Theorem exp4a 378

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 347	. 2 |- (((ch /\ th) -> ta) <-> (ch -> (th -> ta)))
3	1, 2	syl6ib 212	1 |- (ph -> (ps -> (ch -> (th -> ta))))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  exp4d 381  exp45 386  uniiunlem 2130  tz7.7 2970  tfr3 3923  oaass 4192  omordi 4194  unifi 4545  fiint 4547  inf3lem2 4601  zorn2lem6 4780  zorn2lem7 4781  unxpdomlem 4830  prlem936b 5141  divasst 5718  climaddlem3 7085  climmullem8 7096  cvgratlem2 7222  lmnn 7918  occllem6 9166  spansn 9469  elspansn4t 9486  hoadddirt 9721  homco2t 9892  atcvatlem 10303  sumdmdi 10333  sumdmdlem 10336  and4as 10425

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