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  339  hban  1526  sbimi  1737  spsbbi  1816  2exeu  2089  cgsex2g  2717  cgsex4g  2718  spc2egv  2770  spc2gv  2771  sseq2  3116  unssin  3310  uneqin  3322  undif3ss  3332  prneimg  3696  ssunieq  3764  iuneq1  3821  iuneq2  3824  copsex2t  4162  soeq2  4233  tpexg  4360  eldifpw  4393  iunpw  4396  peano5  4507  opbrop  4613  xpsspw  4646  coeq1  4691  coeq2  4692  cnveq  4708  dmeq  4734  sotri  4929  elxp4  5021  elxp5  5022  funun  5162  funtp  5171  imain  5200  2elresin  5229  funssxp  5287  fssres  5293  f1co  5335  foun  5379  resdif  5382  f1oco  5383  fvun1  5480  elfvmptrab1  5508  fvreseq  5517  ftpg  5597  f1o2ndf1  6118  spc2ed  6123  smores  6182  nnaord  6398  nnm00  6418  brecop  6512  eroveu  6513  ecopovtrn  6519  ecopovtrng  6522  th3qlem1  6524  th3q  6527  ixpeq2  6599  djuexb  6922  addcmpblnq  7168  mulcmpblnq  7169  mulclnq  7177  dmaddpq  7180  dmmulpq  7181  mulcanenq  7186  distrnqg  7188  ltdcnq  7198  ltexnqq  7209  enq0breq  7237  mulcmpblnq0  7245  mulcanenq0ec  7246  addnnnq0  7250  mulnnnq0  7251  mulclnq0  7253  nqpnq0nq  7254  nqnq0a  7255  nqnq0m  7256  distrnq0  7260  elinp  7275  genpml  7318  genpmu  7319  genprndl  7322  genprndu  7323  addnqprl  7330  addnqpru  7331  distrlem1prl  7383  distrlem1pru  7384  ltsopr  7397  cauappcvgprlemdisj  7452  caucvgprlemdisj  7475  caucvgprprlemdisj  7503  addcmpblnr  7540  addsrpr  7546  mulsrpr  7547  addclsr  7554  addasssrg  7557  0idsr  7568  1idsr  7569  00sr  7570  mulgt0sr  7579  axaddcl  7665  axmulcl  7667  axaddass  7673  axdistr  7675  cnegexlem3  7932  cnegex  7933  apirr  8360  recexaplem2  8406  zletric  9091  zlelttric  9092  qaddcl  9420  qmulcl  9422  qreccl  9427  iccss  9717  fzsubel  9833  elfz0add  9893  difelfznle  9905  2ffzeq  9911  fzonmapblen  9957  ubmelfzo  9970  ubmelm1fzo  9996  subfzo0  10012  qletric  10014  qlelttric  10015  adddivflid  10058  mulexp  10325  mulexpzap  10326  leexp1a  10341  faclbnd  10480  rexanuz  10753  sqabsadd  10820  sqabssub  10821  abs2dif  10871  rpmincl  11002  xrminrpcl  11036  fsum2dlemstep  11196  summodnegmod  11513  dvds2ln  11515  dvdsflip  11538  gcdsupex  11635  gcdsupcl  11636  gcdabs  11665  sqgcd  11706  lcmabs  11746  lcmgcdlem  11747  lcmgcd  11748  lcmgcdeq  11753  qredeq  11766  cncongr1  11773  cncongr2  11774  hashgcdlem  11892  tgcl  12222  uncld  12271  innei  12321  cnco  12379  txbas  12416  txbasval  12425  blin2  12590  qtopbasss  12679  bj-indind  13119