Theorem 3expd 1085

Description: Exportation deduction for triple conjunction.

Hypothesis

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

Assertion

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

Proof of Theorem 3expd

Step	Hyp	Ref	Expression
1		3expd.1	. . . 4 |- (ph -> ((ps /\ ch /\ th) -> ta))
2	1	com12 14	. . 3 |- ((ps /\ ch /\ th) -> (ph -> ta))
3	2	3exp 1066	. 2 |- (ps -> (ch -> (th -> (ph -> ta))))
4	3	com4r 45	1 |- (ph -> (ps -> (ch -> (th -> ta))))

Syntax hints:   -> wi 3   /\ w3a 858

This theorem is referenced by:  3exp2 1086  3impexpbicom 1287  mulcan 6880  psdmrn 9991  psref 9992  indexfi 10174  findcardOLD 10179  fgid 10289  flimopn 10321  on1el3 10412  eqfnung2 14459  filint2 14923  efilcp2 14926  cnfilca 14927  conttnf 14944  bwt2 14960  altretop 14997  lvsovso2 15039  cmpmon 15164  fgmin 15558  ufileulem 15572  ufileu 15573  filufint 15574  cocanfo 15689  fimax 15746  indexfiOLD 15755  isringd 16097  cvrat4 17076  pmaple 17241  paddasslem14 17294  paddasslem15 17295  osumcllem11 17374

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 164  df-an 242  df-3an 860

Copyright terms: Public domain