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

Theorem 3impd 1205
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 1185 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ( ph  ->  ta ) )
43com12 31 1  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 968
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 371  df-3an 970
This theorem is referenced by:  3imp2  1206  oprabid  6301  isinf  7725  axdc3lem4  8824  iccid  11565  difreicc  11643  issubg4  16010  bwthOLD  19672  reconn  21063  bcthlem2  21494  dvfsumrlim3  22164  ax5seg  23912  axcontlem4  23941  3v3e3cycl1  24308  4cycl4v4e  24330  4cycl4dv4e  24332  2spontn0vne  24551  eupai  24631  cvmlift3lem4  28395  wfrlem12  28919  frrlem11  28964  fscgr  29295  idinside  29299  brsegle  29323  seglecgr12im  29325  dvtanlem  29630  areacirclem1  29673  areacirclem2  29674  areacirclem4  29676  areacirc  29678  imp5q  29696  elicc3  29701  filbcmb  29823  fzmul  29825  3impexp  32176  iunconlem2  32692  islshpcv  33727  cvrat3  34115  4atexlem7  34748
  Copyright terms: Public domain W3C validator