Theorem exp4b 379

Description: An exportation inference.

Hypothesis

Ref	Expression
exp4b.1	|- ((ph /\ ps) -> ((ch /\ th) -> ta))

Assertion

Ref	Expression
exp4b	|- (ph -> (ps -> (ch -> (th -> ta))))

Proof of Theorem exp4b

Step	Hyp	Ref	Expression
1		exp4b.1	. . 3 |- ((ph /\ ps) -> ((ch /\ th) -> ta))
2	1	exp3a 375	. 2 |- ((ph /\ ps) -> (ch -> (th -> ta)))
3	2	ex 373	1 |- (ph -> (ps -> (ch -> (th -> ta))))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  exp43 384  reuss2 2265  wereu 2935  tz7.7 2963  fvco 3759  f1oweALT 3891  omcl 4155  oecl 4156  odi 4194  oeordi 4198  nnmcl 4214  nnecl 4215  inf3lem2 4586  genpnmax 5082  mulclprlem 5093  prlem934 5111  prlem936 5127  reclem3pr 5130  reclem4pr 5131  mulcmpblnr 5155  lemul12it 5800  nnmulclt 5889  sup2 5998  uzind 6153  zbtwnre 6169  qbtwnre 6216  expgt0t 6520  expgt1t 6523  le2sqit 6563  expnbndt 6585  cau4i 6855  cau5 6856  caubnd 6863  iserzmulc1 7072  unbenlem 7447  infpnlem1 7449  lmle 7895  ubthlem5 8464  occl 9097  projlem26 9127  projlem28 9129  spansneleq 9409  spansneleqOLD 9410  elspansn4t 9413  cvmd 10159  atcvat3 10231  mdsymlem3 10240  icmpmon 10587

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain