Theorem anim12i 336

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  anim12ci  337  anim1i  338  anim2i  340  hban  1540  sbimi  1757  spsbbi  1837  2exeu  2111  cgsex2g  2766  cgsex4g  2767  spc2egv  2820  spc2gv  2821  sseq2  3171  unssin  3366  uneqin  3378  undif3ss  3388  prneimg  3761  ssunieq  3829  iuneq1  3886  iuneq2  3889  copsex2t  4230  soeq2  4301  tpexg  4429  eldifpw  4462  iunpw  4465  peano5  4582  opbrop  4690  xpsspw  4723  coeq1  4768  coeq2  4769  cnveq  4785  dmeq  4811  sotri  5006  elxp4  5098  elxp5  5099  funun  5242  funtp  5251  imain  5280  2elresin  5309  funssxp  5367  fssres  5373  f1co  5415  foun  5461  resdif  5464  f1oco  5465  fvun1  5562  elfvmptrab1  5590  fvreseq  5599  ftpg  5680  f1o2ndf1  6207  spc2ed  6212  smores  6271  nnaord  6488  nnm00  6509  brecop  6603  eroveu  6604  ecopovtrn  6610  ecopovtrng  6613  th3qlem1  6615  th3q  6618  ixpeq2  6690  djuexb  7021  addcmpblnq  7329  mulcmpblnq  7330  mulclnq  7338  dmaddpq  7341  dmmulpq  7342  mulcanenq  7347  distrnqg  7349  ltdcnq  7359  ltexnqq  7370  enq0breq  7398  mulcmpblnq0  7406  mulcanenq0ec  7407  addnnnq0  7411  mulnnnq0  7412  mulclnq0  7414  nqpnq0nq  7415  nqnq0a  7416  nqnq0m  7417  distrnq0  7421  elinp  7436  genpml  7479  genpmu  7480  genprndl  7483  genprndu  7484  addnqprl  7491  addnqpru  7492  distrlem1prl  7544  distrlem1pru  7545  ltsopr  7558  cauappcvgprlemdisj  7613  caucvgprlemdisj  7636  caucvgprprlemdisj  7664  addcmpblnr  7701  addsrpr  7707  mulsrpr  7708  addclsr  7715  addasssrg  7718  0idsr  7729  1idsr  7730  00sr  7731  mulgt0sr  7740  axaddcl  7826  axmulcl  7828  axaddass  7834  axdistr  7836  cnegexlem3  8096  cnegex  8097  apirr  8524  recexaplem2  8570  zletric  9256  zlelttric  9257  difgtsumgt  9281  qaddcl  9594  qmulcl  9596  qreccl  9601  iccss  9898  fzsubel  10016  elfz0add  10076  difelfznle  10091  2ffzeq  10097  fzonmapblen  10143  ubmelfzo  10156  ubmelm1fzo  10182  subfzo0  10198  qletric  10200  qlelttric  10201  adddivflid  10248  mulexp  10515  mulexpzap  10516  leexp1a  10531  faclbnd  10675  rexanuz  10952  sqabsadd  11019  sqabssub  11020  abs2dif  11070  rpmincl  11201  xrminrpcl  11237  fsum2dlemstep  11397  fprodeq0  11580  fprod2dlemstep  11585  summodnegmod  11784  dvds2ln  11786  dvdsflip  11811  gcdsupex  11912  gcdsupcl  11913  gcdabs  11943  sqgcd  11984  nnwosdc  11994  lcmabs  12030  lcmgcdlem  12031  lcmgcd  12032  lcmgcdeq  12037  qredeq  12050  cncongr1  12057  cncongr2  12058  hashgcdlem  12192  dvdsprmpweqle  12290  difsqpwdvds  12291  mndissubm  12697  tgcl  12858  uncld  12907  innei  12957  cnco  13015  txbas  13052  txbasval  13061  blin2  13226  qtopbasss  13315  lgsmulsqcoprm  13741  bj-charfunbi  13846  bj-indind  13967