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

Theorem 3imp1 1200
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 1181 . 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 965
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 967
This theorem is referenced by:  reupick2  3634  indcardi  8209  expcan  11914  ltexp2  11915  leexp1a  11920  expnbnd  11991  xrsdsreclblem  17857  matecl  18324  riinopn  18519  neindisj2  18725  filufint  19491  tsmsxp  19727  spthonepeq  23484  zerdivemp1  23919  homco1  25203  homulass  25204  hoadddir  25206  relexpindlem  27339  rtrclreclem.min  27347  mblfinlem3  28427  zerdivemp1x  28758  eluzge0nn0  30186  usg2wlkeq  30286  rusgraprop4  30553  vdn0frgrav2  30613  vdn1frgrav2  30615  usgreghash2spot  30659  athgt  33097  psubspi  33388  paddasslem14  33474
  Copyright terms: Public domain W3C validator