MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3expd Unicode version

Theorem 3expd 1168
Description: Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3expd.1  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
Assertion
Ref Expression
3expd  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem 3expd
StepHypRef Expression
1 3expd.1 . . . 4  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
21com12 27 . . 3  |-  ( ( ps  /\  ch  /\  th )  ->  ( ph  ->  ta ) )
323exp 1150 . 2  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
43com4r 80 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  3exp2  1169  exp516  1171  3impexp  1356  3impexpbicom  1357  riotasv2dOLD  6366  smogt  6400  axdc3lem4  8095  axcclem  8099  caubnd  11858  catidd  13598  mulgnnass  14611  fscgr  24775  eqfnung2  25221  cmptdst  25671  limptlimpr2lem1  25677  limptlimpr2lem2  25678  bwt2  25695  lvsovso2  25730  negveudr  25772  cmpmon  25918  cvrat4  30254  3dim1  30278  3dim2  30279  llnle  30329  lplnle  30351  llncvrlpln2  30368  lplncvrlvol2  30426  pmaple  30572  paddasslem14  30644  paddasslem15  30645  osumcllem11N  30777  cdlemeg46gfre  31343  cdlemk33N  31720  dia2dimlem6  31881  lclkrlem2y  32343
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator