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 2273  wereu 2942  tz7.7 2970  fvco 3771  f1oweALT 3903  omcl 4168  oecl 4169  odi 4207  oeordi 4211  nnmcl 4227  nnecl 4228  inf3lem2 4601  genpnmax 5097  mulclprlem 5108  prlem934 5126  prlem936 5142  reclem3pr 5145  reclem4pr 5146  mulcmpblnr 5170  lemul12it 5814  nnmulclt 5903  sup2 6012  uzind 6167  zbtwnre 6183  qbtwnre 6233  expgt0t 6539  expgt1t 6542  le2sqit 6582  expnbndt 6604  cau4i 6884  cau5 6885  caubnd 6892  iserzmulc1 7105  unbenlem 7483  infpnlem1 7485  lmle 7943  ubthlem5 8517  occl 9169  projlem26 9199  projlem28 9201  spansneleq 9482  spansneleqOLD 9483  elspansn4t 9486  cvmd 10242  atcvat3 10314  mdsymlem3 10323  icmpmon 10694

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