Theorem anim12i 549

Description: Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)

Hypotheses

Ref	Expression
anim12i.1	|- (ph -> ps)
anim12i.2	|- (ch -> th)

Assertion

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

Proof of Theorem anim12i

Step	Hyp	Ref	Expression
1		anim12i.1	. 2 |- (ph -> ps)
2		anim12i.2	. 2 |- (ch -> th)
3		id 19	. 2 |- ((ps /\ th) -> (ps /\ th))
4	1, 2, 3	syl2an 463	1 |- ((ph /\ ch) -> (ps /\ th))

Syntax hints:   -> wi 4   /\ wa 358

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 177  df-an 360

This theorem is referenced by:  anim12ci  550  anim1i  551  anim2i  552  sbimi  1652  2mo  2282  cgsex2g  2891  cgsex4g  2892  spc2egv  2941  sseq2  3293  uneqin  3506  undif3  3515  ssunieq  3924  iuneq1  3982  iuneq2  3985  tfin11  4493  sfinltfin  4535  copsex2t  4608  vtoclr  4816  coeq1  4874  coeq2  4875  brco  4883  cnveq  4886  dmeq  4907  dfco2a  5081  funeq  5127  funun  5146  2elresin  5194  funssxp  5233  fssres  5238  f1co  5264  f1ores  5300  resdif  5306  f1oco  5308  fvun  5378  fvreseq  5398  brswap  5509  fununiq  5517  ndmovdistr  5619  ndmovord  5620  trtxp  5781  fntxp  5804  qrpprod  5836  fnpprod  5843  f1opprod  5844  enprmaplem3  6078  peano4nc  6150  cecl  6186