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

Theorem 3imp1 1210
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 1191 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( th  ->  ta ) )
32imp 427 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ 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:  reupick2  3736  indcardi  8454  expcan  12263  ltexp2  12264  leexp1a  12269  expnbnd  12339  rtrclreclem4  13043  relexpindlem  13045  xrsdsreclblem  18784  matecl  19219  scmateALT  19306  riinopn  19709  neindisj2  19917  filufint  20713  tsmsxp  20949  spthonepeq  25006  usg2wlkeq  25125  rusgraprop4  25361  vdn0frgrav2  25440  vdn1frgrav2  25442  usgreghash2spot  25486  zerdivemp1  25850  homco1  27133  homulass  27134  hoadddir  27136  mblfinlem3  31425  zerdivemp1x  31640  athgt  32473  psubspi  32764  paddasslem14  32850  iccpartigtl  37690  eluzge0nn0  37961
  Copyright terms: Public domain W3C validator