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

Theorem 3anim123d 1262
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 548 . . 3  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
4 3anim123d.3 . . 3  |-  ( ph  ->  ( et  ->  ze )
)
53, 4anim12d 548 . 2  |-  ( ph  ->  ( ( ( ps 
/\  th )  /\  et )  ->  ( ( ch 
/\  ta )  /\  ze ) ) )
6 df-3an 939 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
7 df-3an 939 . 2  |-  ( ( ch  /\  ta  /\  ze )  <->  ( ( ch 
/\  ta )  /\  ze ) )
85, 6, 73imtr4g 263 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  -> 
( ch  /\  ta  /\ 
ze ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  pofun  4521  isopolem  6067  issmo2  6613  smores  6616  inawina  8567  gchina  8576  issubmnd  14726  issubg2  14961  issubrg2  15890  ocv2ss  16902  sslm  17365  cmetcaulem  19243  redwlk  21608  3cycl3dv  21631  3v3e3cycl1  21633  constr3trllem5  21643  grponnncan2  21844  dipsubdir  22351  axcontlem4  25908  axcontlem8  25912  cgr3tr4  25988  idinside  26020  ftc1anclem7  26288  fzmul  26446  fdc1  26452  rngosubdi  26571  rngosubdir  26572  el2wlkonotot0  28341  cdlemg33a  31505
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator