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

Theorem 3impd 1168
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 81 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
323imp 1148 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ( ph  ->  ta ) )
43com12 30 1  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  3imp2  1169  3impexp  1376  oprabid  6106  riotasv2dOLD  6596  isinf  7323  axdc3lem4  8334  iccid  10962  difreicc  11029  joinle  14451  meetle  14458  issubg4  14962  bwth  17474  reconn  18860  bcthlem2  19279  dvfsumrlim3  19918  3v3e3cycl1  21632  4cycl4v4e  21654  4cycl4dv4e  21656  eupai  21690  cvmlift3lem4  25010  wfrlem12  25550  frrlem11  25595  ax5seg  25878  axcontlem4  25907  fscgr  26015  idinside  26019  brsegle  26043  seglecgr12im  26045  areacirclem1  26293  areacirclem2  26294  areacirclem4  26296  areacirc  26298  imp5q  26316  elicc3  26321  filbcmb  26443  fzmul  26445  2spontn0vne  28355  iunconlem2  29048  islshpcv  29852  cvrat3  30240  4atexlem7  30873
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator