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  6350  smogt  6384  axdc3lem4  8079  axcclem  8083  caubnd  11842  catidd  13582  mulgnnass  14595  fscgr  24703  eqfnung2  25118  cmptdst  25568  limptlimpr2lem1  25574  limptlimpr2lem2  25575  bwt2  25592  lvsovso2  25627  negveudr  25669  cmpmon  25815  cvrat4  29632  3dim1  29656  3dim2  29657  llnle  29707  lplnle  29729  llncvrlpln2  29746  lplncvrlvol2  29804  pmaple  29950  paddasslem14  30022  paddasslem15  30023  osumcllem11N  30155  cdlemeg46gfre  30721  cdlemk33N  31098  dia2dimlem6  31259  lclkrlem2y  31721
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