MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3expd 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  1372  3impexpbicom  1373  riotasv2dOLD  6533  smogt  6567  axdc3lem4  8268  axcclem  8272  caubnd  12091  catidd  13834  mulgnnass  14847  fscgr  25730  cvrat4  29559  3dim1  29583  3dim2  29584  llnle  29634  lplnle  29656  llncvrlpln2  29673  lplncvrlvol2  29731  pmaple  29877  paddasslem14  29949  paddasslem15  29950  osumcllem11N  30082  cdlemeg46gfre  30648  cdlemk33N  31025  dia2dimlem6  31186  lclkrlem2y  31648
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