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

Theorem 3imp1 1166
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 1147 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( th  ->  ta ) )
32imp 419 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  reupick2  3619  indcardi  7914  expcan  11424  ltexp2  11425  leexp1a  11430  expnbnd  11500  xrsdsreclblem  16736  riinopn  16973  neindisj2  17179  filufint  17944  tsmsxp  18176  spthonepeq  21579  zerdivemp1  22014  homco1  23296  homulass  23297  hoadddir  23299  relexpindlem  25131  rtrclreclem.min  25139  mblfinlem2  26235  zerdivemp1x  26562  2cshw2lem3  28220  vdn0frgrav2  28351  vdn1frgrav2  28353  usgreghash2spot  28395  athgt  30190  psubspi  30481  paddasslem14  30567
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator