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

Theorem 3expd 1213
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 31 . . 3  |-  ( ( ps  /\  ch  /\  th )  ->  ( ph  ->  ta ) )
323exp 1195 . 2  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
43com4r 86 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  3exp2  1214  exp516  1216  smogt  7039  axdc3lem4  8834  axcclem  8838  caubnd  13157  catidd  14938  mulgnnass  15984  bwthOLD  19717  mclsind  28681  fscgr  29583  3impexp  32516  3impexpbicom  32517  cvrat4  34456  3dim1  34480  3dim2  34481  llnle  34531  lplnle  34553  llncvrlpln2  34570  lplncvrlvol2  34628  pmaple  34774  paddasslem14  34846  paddasslem15  34847  osumcllem11N  34979  cdlemeg46gfre  35545  cdlemk33N  35922  dia2dimlem6  36083  lclkrlem2y  36545
  Copyright terms: Public domain W3C validator