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

Theorem 3exp1 1167
Description: Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3exp1.1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ta )
Assertion
Ref Expression
3exp1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem 3exp1
StepHypRef Expression
1 3exp1.1 . . 3  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ta )
21ex 423 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( th  ->  ta ) )
323exp 1150 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:  ltmpi  8544  voliunlem3  18925  strlem3a  22848  hstrlem3a  22856  chirredlem1  22986  zerdivemp1  25539  rngoridfz  25540  cmptdst  25671  limptlimpr2lem1  25677  cmpmon  25918  icmpmon  25919  lemindclsbu  26098  clscnc  26113  lppotos  26247  bsstrs  26249  nbssntrs  26250  nn0prpwlem  26341  zerdivemp1x  26689  jm2.26  27198  athgt  30267  paddasslem14  30644  paddidm  30652  tendospcanN  31835
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