Theorem anim12i 334

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  anim12ci  335  anim1i  336  anim2i  337  hban  1494  sbimi  1705  spsbbi  1783  2exeu  2052  cgsex2g  2677  cgsex4g  2678  spc2egv  2730  spc2gv  2731  sseq2  3071  unssin  3262  uneqin  3274  undif3ss  3284  prneimg  3648  ssunieq  3716  iuneq1  3773  iuneq2  3776  copsex2t  4105  soeq2  4176  tpexg  4303  eldifpw  4336  iunpw  4339  peano5  4450  opbrop  4556  xpsspw  4589  coeq1  4634  coeq2  4635  cnveq  4651  dmeq  4677  sotri  4870  elxp4  4962  elxp5  4963  funun  5103  funtp  5112  imain  5141  2elresin  5170  funssxp  5228  fssres  5234  f1co  5276  foun  5320  resdif  5323  f1oco  5324  fvun1  5419  elfvmptrab1  5447  fvreseq  5456  ftpg  5536  f1o2ndf1  6055  spc2ed  6060  smores  6119  nnaord  6335  nnm00  6355  brecop  6449  eroveu  6450  ecopovtrn  6456  ecopovtrng  6459  th3qlem1  6461  th3q  6464  ixpeq2  6536  djuexb  6844  addcmpblnq  7076  mulcmpblnq  7077  mulclnq  7085  dmaddpq  7088  dmmulpq  7089  mulcanenq  7094  distrnqg  7096  ltdcnq  7106  ltexnqq  7117  enq0breq  7145  mulcmpblnq0  7153  mulcanenq0ec  7154  addnnnq0  7158  mulnnnq0  7159  mulclnq0  7161  nqpnq0nq  7162  nqnq0a  7163  nqnq0m  7164  distrnq0  7168  elinp  7183  genpml  7226  genpmu  7227  genprndl  7230  genprndu  7231  addnqprl  7238  addnqpru  7239  distrlem1prl  7291  distrlem1pru  7292  ltsopr  7305  cauappcvgprlemdisj  7360  caucvgprlemdisj  7383  caucvgprprlemdisj  7411  addcmpblnr  7435  addsrpr  7441  mulsrpr  7442  addclsr  7449  addasssrg  7452  0idsr  7463  1idsr  7464  00sr  7465  mulgt0sr  7473  axaddcl  7551  axmulcl  7553  axaddass  7557  axdistr  7559  cnegexlem3  7810  cnegex  7811  apirr  8233  recexaplem2  8274  zletric  8950  zlelttric  8951  qaddcl  9277  qmulcl  9279  qreccl  9284  iccss  9565  fzsubel  9681  elfz0add  9741  difelfznle  9753  2ffzeq  9759  fzonmapblen  9805  ubmelfzo  9818  ubmelm1fzo  9844  subfzo0  9860  qletric  9862  qlelttric  9863  adddivflid  9906  mulexp  10173  mulexpzap  10174  leexp1a  10189  faclbnd  10328  rexanuz  10600  sqabsadd  10667  sqabssub  10668  abs2dif  10718  rpmincl  10848  xrminrpcl  10882  fsum2dlemstep  11042  summodnegmod  11319  dvds2ln  11321  dvdsflip  11344  gcdsupex  11441  gcdsupcl  11442  gcdabs  11471  sqgcd  11510  lcmabs  11550  lcmgcdlem  11551  lcmgcd  11552  lcmgcdeq  11557  qredeq  11570  cncongr1  11577  cncongr2  11578  hashgcdlem  11695  tgcl  12015  uncld  12064  innei  12114  cnco  12171  txbas  12208  txbasval  12217  blin2  12360  qtopbasss  12443  bj-indind  12715