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  3454  indcardi  7668  expcan  11154  ltexp2  11155  leexp1a  11160  expnbnd  11230  xrsdsreclblem  16417  riinopn  16654  neindisj2  16860  filufint  17615  tsmsxp  17837  homco1  22381  homulass  22382  hoadddir  22384  relexpindlem  24036  rtrclreclem.min  24044  and4as  24939  11st22nd  25045  eqfnung2  25118  cmpltr2  25407  cmperltr  25409  zerdivemp1  25436  distmlva  25688  distsava  25689  tartarmap  25888  lemindclsbu  25995  clscnc  26010  lppotos  26144  pdiveql  26168  zerdivemp1x  26586  athgt  29645  psubspi  29936  paddasslem14  30022
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