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

Theorem 3impd 1211
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 84 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
323imp 1191 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ( ph  ->  ta ) )
43com12 29 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 369  df-3an 976
This theorem is referenced by:  3imp2  1212  3impexp  1219  oprabid  6305  wfrlem12  7032  isinf  7768  axdc3lem4  8865  iccid  11627  difreicc  11706  relexpaddg  13035  issubg4  16544  reconn  21625  bcthlem2  22056  dvfsumrlim3  22726  ax5seg  24658  axcontlem4  24687  3v3e3cycl1  25061  4cycl4v4e  25083  4cycl4dv4e  25085  2spontn0vne  25304  eupai  25384  cvmlift3lem4  29619  frrlem11  30099  fscgr  30418  idinside  30422  brsegle  30446  seglecgr12im  30448  imp5q  30540  elicc3  30545  dvtanlemOLD  31437  areacirclem1  31478  areacirclem2  31479  areacirclem4  31481  areacirc  31483  filbcmb  31513  fzmul  31515  islshpcv  32071  cvrat3  32459  4atexlem7  33092  relexpmulg  35689  iunconlem2  36766
  Copyright terms: Public domain W3C validator