Theorem anim12i 331

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 283	1 |- ( ( ph /\ ch ) -> ( ps /\ th ) )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  anim12ci  332  anim1i  333  anim2i  334  hban  1482  sbimi  1691  spsbbi  1769  2exeu  2037  cgsex2g  2648  cgsex4g  2649  spc2egv  2700  spc2gv  2701  sseq2  3034  unssin  3224  uneqin  3236  undif3ss  3246  prneimg  3595  ssunieq  3663  iuneq1  3720  iuneq2  3723  copsex2t  4039  soeq2  4110  tpexg  4236  eldifpw  4265  iunpw  4268  peano5  4379  opbrop  4478  xpsspw  4511  coeq1  4554  coeq2  4555  cnveq  4571  dmeq  4597  sotri  4785  elxp4  4875  elxp5  4876  funun  5014  funtp  5023  imain  5052  2elresin  5081  funssxp  5132  fssres  5138  f1co  5179  foun  5223  resdif  5226  f1oco  5227  fvun1  5318  fvreseq  5351  ftpg  5426  f1o2ndf1  5931  spc2ed  5936  smores  5992  nnaord  6201  nnm00  6221  brecop  6315  eroveu  6316  ecopovtrn  6322  ecopovtrng  6325  th3qlem1  6327  th3q  6330  addcmpblnq  6847  mulcmpblnq  6848  mulclnq  6856  dmaddpq  6859  dmmulpq  6860  mulcanenq  6865  distrnqg  6867  ltdcnq  6877  ltexnqq  6888  enq0breq  6916  mulcmpblnq0  6924  mulcanenq0ec  6925  addnnnq0  6929  mulnnnq0  6930  mulclnq0  6932  nqpnq0nq  6933  nqnq0a  6934  nqnq0m  6935  distrnq0  6939  elinp  6954  genpml  6997  genpmu  6998  genprndl  7001  genprndu  7002  addnqprl  7009  addnqpru  7010  distrlem1prl  7062  distrlem1pru  7063  ltsopr  7076  cauappcvgprlemdisj  7131  caucvgprlemdisj  7154  caucvgprprlemdisj  7182  addcmpblnr  7206  addsrpr  7212  mulsrpr  7213  addclsr  7220  addasssrg  7223  0idsr  7234  1idsr  7235  00sr  7236  mulgt0sr  7244  axaddcl  7322  axmulcl  7324  axaddass  7328  axdistr  7330  cnegexlem3  7580  cnegex  7581  apirr  8000  recexaplem2  8037  zletric  8704  zlelttric  8705  qaddcl  9029  qmulcl  9031  qreccl  9036  iccss  9268  fzsubel  9382  elfz0add  9439  difelfznle  9451  2ffzeq  9456  fzonmapblen  9501  ubmelfzo  9514  ubmelm1fzo  9540  subfzo0  9556  qletric  9558  qlelttric  9559  adddivflid  9602  mulexp  9845  mulexpzap  9846  leexp1a  9861  faclbnd  9998  rexanuz  10262  sqabsadd  10329  sqabssub  10330  abs2dif  10380  summodnegmod  10621  dvds2ln  10623  dvdsflip  10646  gcdsupex  10743  gcdsupcl  10744  gcdabs  10773  sqgcd  10812  lcmabs  10852  lcmgcdlem  10853  lcmgcd  10854  lcmgcdeq  10859  qredeq  10872  cncongr1  10879  cncongr2  10880  hashgcdlem  10997  bj-indind  11184