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

Theorem 3expd 1214
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 1196 . 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 974
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 976
This theorem is referenced by:  3exp2  1215  exp516  1217  smogt  7040  axdc3lem4  8836  axcclem  8840  caubnd  13170  catidd  14954  mulgnnass  16044  bwthOLD  19784  mclsind  28803  fscgr  29705  3impexp  32953  3impexpbicom  32954  cvrat4  34907  3dim1  34931  3dim2  34932  llnle  34982  lplnle  35004  llncvrlpln2  35021  lplncvrlvol2  35079  pmaple  35225  paddasslem14  35297  paddasslem15  35298  osumcllem11N  35430  cdlemeg46gfre  35998  cdlemk33N  36375  dia2dimlem6  36536  lclkrlem2y  36998  cotr2g  37479
  Copyright terms: Public domain W3C validator