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

Theorem 3exp1 1221
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 435 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( th  ->  ta ) )
323exp 1204 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  ltmpi  9328  lcmfunsnlem  14585  symgfvne  16980  voliunlem3  22382  frgraregord013  25691  zerdivemp1  26007  rngoridfz  26008  strlem3a  27740  hstrlem3a  27748  chirredlem1  27878  nn0prpwlem  30763  zerdivemp1x  31898  athgt  32730  paddasslem14  33107  paddidm  33115  tendospcanN  34300  jm2.26  35563  relexpxpmin  35948  0ellimcdiv  37302
  Copyright terms: Public domain W3C validator