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  5898  riotasv2dOLD  6366  isinf  7092  axdc3lem4  8095  iccid  10717  difreicc  10783  joinle  14143  meetle  14150  issubg4  14654  reconn  18349  bcthlem2  18763  dvfsumrlim3  19396  cvmlift3lem4  23868  eupai  23898  wfrlem12  24338  frrlem11  24364  ax5seg  24638  axcontlem4  24667  fscgr  24775  idinside  24779  brsegle  24803  seglecgr12im  24805  areacirclem2  25028  areacirclem3  25029  areacirclem4  25030  areacirclem5  25032  areacirc  25034  elioo1t3  25605  islimrs4  25685  bwt2  25695  hdrmp  25809  homgrf  25905  cmpmon  25918  icmpmon  25919  imp5q  26324  elicc3  26331  filbcmb  26535  fzmul  26546  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv4e  28414  islshpcv  29865  cvrat3  30253  4atexlem7  30886
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