Theorem exp4b 296

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 292	. 2 |- ((ph /\ ps) -> (ch -> (th -> ta )))
3	2	exp 291	1 |- (ph -> (ps -> (ch -> (th -> ta ))))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  exp43 301  wereu 2197  tz7.7 2224  limsuc 2361  fvco 2865  f1oweOLD 2944  tfrlem8 2956  omcl 3139  oecl 3140  nnmcl 3173  nndi 3180  nnmordi 3188  inf3lem2 3465  genpnmax 3904  mulclprlem 3915  prlem934 3933  prlem936 3949  reclem3pr 3952  reclem4pr 3953  mulcmpblnr 3977  nnmulclt 4437  sup2 4510  zbtwnre 4619  qbtwnre 4650  occl 5188  projlem26 5218  projlem28 5220  spansneleq 5475  elspansn4t 5478  atcvat3 5774  mdsymlem3 5778

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org