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

Theorem 3impd 1165
Description: Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3imp1.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
3impd  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )

Proof of Theorem 3impd
StepHypRef Expression
1 3imp1.1 . . . 4  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
21com4l 78 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
323imp 1145 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ( ph  ->  ta ) )
43com12 27 1  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  3imp2  1166  3impexp  1356  oprabid  5882  riotasv2dOLD  6350  isinf  7076  axdc3lem4  8079  iccid  10701  difreicc  10767  joinle  14127  meetle  14134  issubg4  14638  reconn  18333  bcthlem2  18747  dvfsumrlim3  19380  cvmlift3lem4  23853  eupai  23883  wfrlem12  24267  frrlem11  24293  ax5seg  24566  axcontlem4  24595  fscgr  24703  idinside  24707  brsegle  24731  seglecgr12im  24733  areacirclem2  24925  areacirclem3  24926  areacirclem4  24927  areacirclem5  24929  areacirc  24931  elioo1t3  25502  islimrs4  25582  bwt2  25592  hdrmp  25706  homgrf  25802  cmpmon  25815  icmpmon  25816  imp5q  26221  elicc3  26228  filbcmb  26432  fzmul  26443  islshpcv  29243  cvrat3  29631  4atexlem7  30264
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