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

Theorem 3exp1 1212
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 434 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( th  ->  ta ) )
323exp 1195 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  ltmpi  9282  symgfvne  16218  voliunlem3  21725  frgraregord013  24823  zerdivemp1  25140  rngoridfz  25141  strlem3a  26875  hstrlem3a  26883  chirredlem1  27013  nn0prpwlem  29745  zerdivemp1x  29989  jm2.26  30576  athgt  34270  paddasslem14  34647  paddidm  34655  tendospcanN  35838
  Copyright terms: Public domain W3C validator