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

Theorem 3anim123d 1261
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 547 . . 3  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
4 3anim123d.3 . . 3  |-  ( ph  ->  ( et  ->  ze )
)
53, 4anim12d 547 . 2  |-  ( ph  ->  ( ( ( ps 
/\  th )  /\  et )  ->  ( ( ch 
/\  ta )  /\  ze ) ) )
6 df-3an 938 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
7 df-3an 938 . 2  |-  ( ( ch  /\  ta  /\  ze )  <->  ( ( ch 
/\  ta )  /\  ze ) )
85, 6, 73imtr4g 262 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  -> 
( ch  /\  ta  /\ 
ze ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  pofun  4487  isopolem  6032  issmo2  6578  smores  6581  inawina  8529  gchina  8538  issubmnd  14687  issubg2  14922  issubrg2  15851  ocv2ss  16863  sslm  17325  cmetcaulem  19202  redwlk  21567  3cycl3dv  21590  3v3e3cycl1  21592  constr3trllem5  21602  grponnncan2  21803  dipsubdir  22310  axcontlem4  25818  axcontlem8  25822  cgr3tr4  25898  idinside  25930  fzmul  26342  fdc1  26348  rngosubdi  26467  rngosubdir  26468  el2wlkonotot0  28077  cdlemg33a  31200
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