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

Theorem 3expd 1170
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 29 . . 3  |-  ( ( ps  /\  ch  /\  th )  ->  ( ph  ->  ta ) )
323exp 1152 . 2  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
43com4r 82 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  3exp2  1171  exp516  1173  3impexp  1375  3impexpbicom  1376  riotasv2dOLD  6587  smogt  6621  axdc3lem4  8323  axcclem  8327  caubnd  12152  catidd  13895  mulgnnass  14908  bwth  17463  fscgr  25979  cvrat4  30141  3dim1  30165  3dim2  30166  llnle  30216  lplnle  30238  llncvrlpln2  30255  lplncvrlvol2  30313  pmaple  30459  paddasslem14  30531  paddasslem15  30532  osumcllem11N  30664  cdlemeg46gfre  31230  cdlemk33N  31607  dia2dimlem6  31768  lclkrlem2y  32230
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator