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

Theorem 3exp1 1203
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 1186 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  ltmpi  9072  symgfvne  15892  voliunlem3  21032  zerdivemp1  23920  rngoridfz  23921  strlem3a  25655  hstrlem3a  25663  chirredlem1  25793  nn0prpwlem  28515  zerdivemp1x  28759  jm2.26  29349  frgraregord013  30709  athgt  33098  paddasslem14  33475  paddidm  33483  tendospcanN  34666
  Copyright terms: Public domain W3C validator