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

Theorem 3exp1 1169
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 424 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( th  ->  ta ) )
323exp 1152 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ltmpi  8781  voliunlem3  19446  zerdivemp1  22022  rngoridfz  22023  strlem3a  23755  hstrlem3a  23763  chirredlem1  23893  nn0prpwlem  26325  zerdivemp1x  26571  jm2.26  27073  athgt  30253  paddasslem14  30630  paddidm  30638  tendospcanN  31821
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator