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

Theorem 3anim123d 1310
Description: Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)
Hypotheses
Ref Expression
3anim123d.1  |-  ( ph  ->  ( ps  ->  ch ) )
3anim123d.2  |-  ( ph  ->  ( th  ->  ta ) )
3anim123d.3  |-  ( ph  ->  ( et  ->  ze )
)
Assertion
Ref Expression
3anim123d  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  -> 
( ch  /\  ta  /\ 
ze ) ) )

Proof of Theorem 3anim123d
StepHypRef Expression
1 3anim123d.1 . . . 4  |-  ( ph  ->  ( ps  ->  ch ) )
2 3anim123d.2 . . . 4  |-  ( ph  ->  ( th  ->  ta ) )
31, 2anim12d 563 . . 3  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
4 3anim123d.3 . . 3  |-  ( ph  ->  ( et  ->  ze )
)
53, 4anim12d 563 . 2  |-  ( ph  ->  ( ( ( ps 
/\  th )  /\  et )  ->  ( ( ch 
/\  ta )  /\  ze ) ) )
6 df-3an 978 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
7 df-3an 978 . 2  |-  ( ( ch  /\  ta  /\  ze )  <->  ( ( ch 
/\  ta )  /\  ze ) )
85, 6, 73imtr4g 272 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  -> 
( ch  /\  ta  /\ 
ze ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 976
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 187  df-an 371  df-3an 978
This theorem is referenced by:  pofun  4762  isopolem  6226  issmo2  7055  smores  7058  inawina  9100  gchina  9109  repswcshw  12838  issubmnd  16274  issubg2  16542  issubrg2  17771  ocv2ss  19004  sslm  20095  cmetcaulem  22021  axcontlem4  24699  axcontlem8  24703  redwlk  25037  3cycl3dv  25071  3v3e3cycl1  25073  constr3trllem5  25083  el2wlkonotot0  25301  grponnncan2  25683  dipsubdir  26190  cgr3tr4  30403  idinside  30435  ftc1anclem7  31482  fzmul  31528  fdc1  31534  rngosubdi  31651  rngosubdir  31652  cdlemg33a  33738  lidlmsgrp  38256  lidlrng  38257
  Copyright terms: Public domain W3C validator