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  3615  indcardi  7960  expcan  11470  ltexp2  11471  leexp1a  11476  expnbnd  11546  xrsdsreclblem  16782  riinopn  17019  neindisj2  17225  filufint  17990  tsmsxp  18222  spthonepeq  21625  zerdivemp1  22060  homco1  23342  homulass  23343  hoadddir  23345  relexpindlem  25174  rtrclreclem.min  25182  mblfinlem3  26285  zerdivemp1x  26613  2cshw2lem3  28386  usg2wlkeq  28440  vdn0frgrav2  28586  vdn1frgrav2  28588  usgreghash2spot  28630  athgt  30427  psubspi  30718  paddasslem14  30804
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