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  1479  sbimi  1687  spsbbi  1765  2exeu  2033  cgsex2g  2635  cgsex4g  2636  spc2egv  2687  spc2gv  2688  sseq2  3021  unssin  3203  uneqin  3215  undif3ss  3225  prneimg  3566  ssunieq  3634  iuneq1  3691  iuneq2  3694  copsex2t  4000  soeq2  4071  tpexg  4197  eldifpw  4226  iunpw  4229  peano5  4339  opbrop  4437  xpsspw  4468  coeq1  4511  coeq2  4512  cnveq  4527  dmeq  4553  sotri  4740  elxp4  4828  elxp5  4829  funun  4964  funtp  4972  imain  5001  2elresin  5030  funssxp  5080  fssres  5086  f1co  5121  foun  5165  resdif  5168  f1oco  5169  fvun1  5260  fvreseq  5292  ftpg  5368  f1o2ndf1  5869  spc2ed  5874  smores  5930  nnaord  6105  nnm00  6125  brecop  6219  eroveu  6220  ecopovtrn  6226  ecopovtrng  6229  th3qlem1  6231  th3q  6234  addcmpblnq  6557  mulcmpblnq  6558  mulclnq  6566  dmaddpq  6569  dmmulpq  6570  mulcanenq  6575  distrnqg  6577  ltdcnq  6587  ltexnqq  6598  enq0breq  6626  mulcmpblnq0  6634  mulcanenq0ec  6635  addnnnq0  6639  mulnnnq0  6640  mulclnq0  6642  nqpnq0nq  6643  nqnq0a  6644  nqnq0m  6645  distrnq0  6649  elinp  6664  genpml  6707  genpmu  6708  genprndl  6711  genprndu  6712  addnqprl  6719  addnqpru  6720  distrlem1prl  6772  distrlem1pru  6773  ltsopr  6786  cauappcvgprlemdisj  6841  caucvgprlemdisj  6864  caucvgprprlemdisj  6892  addcmpblnr  6916  addsrpr  6922  mulsrpr  6923  addclsr  6930  addasssrg  6933  0idsr  6944  1idsr  6945  00sr  6946  mulgt0sr  6954  axaddcl  7032  axmulcl  7034  axaddass  7038  axdistr  7040  cnegexlem3  7285  cnegex  7286  apirr  7705  recexaplem2  7742  zletric  8395  zlelttric  8396  qaddcl  8720  qmulcl  8722  qreccl  8727  iccss  8964  fzsubel  9078  elfz0add  9134  difelfznle  9146  2ffzeq  9151  fzonmapblen  9196  ubmelfzo  9209  ubmelm1fzo  9235  subfzo0  9251  qletric  9253  qlelttric  9254  adddivflid  9294  mulexp  9515  mulexpzap  9516  leexp1a  9531  faclbnd  9668  rexanuz  9874  sqabsadd  9941  sqabssub  9942  abs2dif  9992  summodnegmod  10226  dvds2ln  10228  dvdsflip  10251  gcdsupex  10349  gcdsupcl  10350  gcdabs  10379  sqgcd  10418  lcmabs  10458  lcmgcdlem  10459  lcmgcd  10460  lcmgcdeq  10465  qredeq  10478  cncongr1  10485  cncongr2  10486  bj-indind  10727