Theorem 3anim1i 1248

Description: Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)

Hypothesis

Ref	Expression
3animi.1	|- ( ph -> ps )

Assertion

Ref	Expression
3anim1i	|- ( ( ph /\ ch /\ th ) -> ( ps /\ ch /\ th ) )

Proof of Theorem 3anim1i

Step	Hyp	Ref	Expression
1		3animi.1	. 2 |- ( ph -> ps )
2		id 22	. 2 |- ( ch -> ch )
3		id 22	. 2 |- ( th -> th )
4	1, 2, 3	3anim123i 1247	1 |- ( ( ph /\ ch /\ th ) -> ( ps /\ ch /\ th ) )

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl3an1  1359  syl3anl1  1374  syl3anr1  1378  fnsuppres  7322  elfiun  8336  elioc2  12236  elico2  12237  elicc2  12238  dvdsleabs2  15034  mulgnndir  17569  mulgnnass  17576  cphipval  23042  spthonpthon  26647  uhgrwkspth  26651  usgr2wlkspth  26655  upgriseupth  27067  cm2j  28479  bnj544  30964  btwnconn1lem4  32197  relowlssretop  33211  dalem53  35011  dalem54  35012  paddasslem14  35119  mzpcong  37539