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

Theorem 3anim123d 1259
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 936 . 2  |-  ( ( ps  /\  th  /\  et )  <->  ( ( ps 
/\  th )  /\  et ) )
7 df-3an 936 . 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 934
This theorem is referenced by:  pofun  4346  isopolem  5858  issmo2  6382  smores  6385  inawina  8328  gchina  8337  issubmnd  14417  issubg2  14652  issubrg2  15581  ocv2ss  16589  sslm  17043  cmetcaulem  18730  grponnncan2  20937  dipsubdir  21442  axcontlem4  24667  axcontlem8  24671  cgr3tr4  24747  idinside  24779  cmpassoh  25904  fzmul  26546  fdc1  26559  rngosubdi  26687  rngosubdir  26688  redwlk  28364  3cycl3dv  28388  3v3e3cycl1  28390  constr3trllem5  28400  cdlemg33a  31517
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 936
  Copyright terms: Public domain W3C validator