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

Theorem 3anim123d 1260
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 546 . . 3  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
4 3anim123d.3 . . 3  |-  ( ph  ->  ( et  ->  ze )
)
53, 4anim12d 546 . 2  |-  ( ph  ->  ( ( ( ps 
/\  th )  /\  et )  ->  ( ( ch 
/\  ta )  /\  ze ) ) )
6 df-3an 937 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
7 df-3an 937 . 2  |-  ( ( ch  /\  ta  /\  ze )  <->  ( ( ch 
/\  ta )  /\  ze ) )
85, 6, 73imtr4g 261 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  -> 
( ch  /\  ta  /\ 
ze ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 935
This theorem is referenced by:  pofun  4433  isopolem  5965  issmo2  6508  smores  6511  inawina  8459  gchina  8468  issubmnd  14611  issubg2  14846  issubrg2  15775  ocv2ss  16790  sslm  17244  cmetcaulem  18929  grponnncan2  21232  dipsubdir  21739  axcontlem4  25337  axcontlem8  25341  cgr3tr4  25417  idinside  25449  fzmul  25950  fdc1  25963  rngosubdi  26090  rngosubdir  26091  redwlk  27744  3cycl3dv  27768  3v3e3cycl1  27770  constr3trllem5  27780  cdlemg33a  30966
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 177  df-an 360  df-3an 937
  Copyright terms: Public domain W3C validator