Theorem exp4a 295

Description: An exportation inference.

Hypothesis

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

Assertion

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

Proof of Theorem exp4a

Step	Hyp	Ref	Expression
1		exp4a.1	. 2 |- (ph -> (ps -> ((ch /\ th) -> ta )))
2		impexp 276	. 2 |- (((ch /\ th) -> ta ) <-> (ch -> (th -> ta )))
3	1, 2	syl6ib 185	1 |- (ph -> (ps -> (ch -> (th -> ta ))))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  exp4d 298  exp45 303  tz7.7 2224  tfr3 2964  tz7.49 2997  oaass 3163  omordi 3164  fiint 3445  inf3lem2 3465  zornlem6 3608  zornlem7 3609  prlem936b 3948  divasst 4239  occllem6 5185  spansn 5462  elspansn4t 5478  atcvatlem 5770  sumdmdi 5785  sumdmdlem 5786

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