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

Theorem 3imp1 1167
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 1148 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( th  ->  ta ) )
32imp 420 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  reupick2  3629  indcardi  7927  expcan  11437  ltexp2  11438  leexp1a  11443  expnbnd  11513  xrsdsreclblem  16749  riinopn  16986  neindisj2  17192  filufint  17957  tsmsxp  18189  spthonepeq  21592  zerdivemp1  22027  homco1  23309  homulass  23310  hoadddir  23312  relexpindlem  25144  rtrclreclem.min  25152  mblfinlem3  26257  zerdivemp1x  26585  2cshw2lem3  28288  usg2wlkeq  28342  vdn0frgrav2  28488  vdn1frgrav2  28490  usgreghash2spot  28532  athgt  30327  psubspi  30618  paddasslem14  30704
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator