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

Theorem 3imp1 1204
Description: Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3imp1.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
3imp1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ta )

Proof of Theorem 3imp1
StepHypRef Expression
1 3imp1.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
213imp 1185 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( th  ->  ta ) )
32imp 429 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ 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:  reupick2  3777  indcardi  8411  expcan  12173  ltexp2  12174  leexp1a  12179  expnbnd  12250  xrsdsreclblem  18225  matecl  18687  scmateALT  18774  riinopn  19177  neindisj2  19383  filufint  20149  tsmsxp  20385  spthonepeq  24251  usg2wlkeq  24370  rusgraprop4  24606  vdn0frgrav2  24686  vdn1frgrav2  24688  usgreghash2spot  24732  zerdivemp1  25098  homco1  26382  homulass  26383  hoadddir  26385  relexpindlem  28523  rtrclreclem.min  28531  mblfinlem3  29617  zerdivemp1x  29948  eluzge0nn0  31753  athgt  34127  psubspi  34418  paddasslem14  34504
  Copyright terms: Public domain W3C validator