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

Theorem 3imp1 1164
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 1145 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( th  ->  ta ) )
32imp 418 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  reupick2  3467  indcardi  7684  expcan  11170  ltexp2  11171  leexp1a  11176  expnbnd  11246  xrsdsreclblem  16433  riinopn  16670  neindisj2  16876  filufint  17631  tsmsxp  17853  homco1  22397  homulass  22398  hoadddir  22400  relexpindlem  24051  rtrclreclem.min  24059  and4as  25042  11st22nd  25148  eqfnung2  25221  cmpltr2  25510  cmperltr  25512  zerdivemp1  25539  distmlva  25791  distsava  25792  tartarmap  25991  lemindclsbu  26098  clscnc  26113  lppotos  26247  pdiveql  26271  zerdivemp1x  26689  athgt  30267  psubspi  30558  paddasslem14  30644
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator