Theorem adantlr 474

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
adantlr	|- ( ( ( ph /\ th ) /\ ps ) -> ch )

Proof of Theorem adantlr

Step	Hyp	Ref	Expression
1		simpl 108	. 2 |- ( ( ph /\ th ) -> ph )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan 281	1 |- ( ( ( ph /\ th ) /\ ps ) -> ch )

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:  ad2antrr  485  ad2ant2r  506  ad2ant2rl  508  adantl3r  509  ad4ant14  511  ad4ant24  513  ad5ant13  516  ad5ant14  517  ad5ant15  518  3ad2antl1  1154  3ad2antl2  1155  ad4ant124  1211  3adant1r  1226  bilukdc  1391  intab  3860  pofun  4297  ralxfrd  4447  rexxfrd  4448  ordtri2or2exmidlem  4510  wessep  4562  poinxp  4680  relop  4761  fun11iun  5463  ssimaex  5557  fndmdif  5601  fconst2g  5711  foeqcnvco  5769  f1eqcocnv  5770  isocnv  5790  isocnv2  5791  riota2df  5829  f1o2ndf1  6207  tfr1onlembacc  6321  tfr1onlemaccex  6327  tfr1onlemres  6328  tfrcllembacc  6334  tfrcllemaccex  6340  tfrcllemres  6341  tfrcldm  6342  tfrcl  6343  xpdom2  6809  fimax2gtrilemstep  6878  xpfi  6907  eqsupti  6973  ordiso2  7012  enumctlemm  7091  enwomnilem  7145  cc2lem  7228  mulcanpig  7297  prarloclemlt  7455  genpdf  7470  genpdisj  7485  addnqprl  7491  addnqpru  7492  addlocpr  7498  prmuloc  7528  mulnqprl  7530  mulnqpru  7531  mullocpr  7533  ltpopr  7557  ltsopr  7558  ltaddpr  7559  ltexprlemdisj  7568  ltexprlemloc  7569  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  ltaprg  7581  recexprlemopu  7589  recexprlemloc  7593  cauappcvgprlemladdfl  7617  cauappcvgprlemladdru  7618  caucvgsrlemcau  7755  caucvgsrlemgt1  7757  caucvgsrlemoffcau  7760  caucvgsrlemoffres  7762  suplocsrlem  7770  axcaucvglemcau  7860  axpre-suploclemres  7863  axsuploc  7992  cnegexlem1  8094  cnegexlem3  8096  cnegex  8097  addsubeq4  8134  rimul  8504  divcanap6  8636  ltmul12a  8776  lemul12b  8777  lbinf  8864  zrevaddcl  9262  nzadd  9264  zextle  9303  fzind  9327  uz11  9509  infregelbex  9557  qreccl  9601  qrevaddcl  9603  irradd  9605  xrlttr  9752  xrltso  9753  xaddass  9826  xleadd1a  9830  xlt2add  9837  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  divelunit  9959  uzsubsubfz  10003  fzaddel  10015  fzrev  10040  elfzmlbp  10088  frec2uzrdg  10365  frecuzrdgtcl  10368  frecuzrdgsuc  10370  frecuzrdgdomlem  10373  frecuzrdgfunlem  10375  frecuzrdgsuctlem  10379  iseqovex  10412  seq3val  10414  seqf  10417  seq3clss  10423  seq3fveq2  10425  seq3feq2  10426  seq3feq  10428  seq3shft2  10429  ser3mono  10434  seq3split  10435  seq3caopr3  10437  seq3caopr2  10438  iseqf1olemab  10445  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  seq3f1olemstep  10457  seq3f1oleml  10459  seq3id3  10463  seq3id  10464  seq3id2  10465  seq3homo  10466  seq3z  10467  seqfeq3  10468  ser3ge0  10473  expp1  10483  expnegap0  10484  expcllem  10487  mulexp  10515  expadd  10518  expaddzap  10520  expmulzap  10522  expdivap  10527  leexp1a  10531  expnlbnd  10600  bcpasc  10700  bccl  10701  hashfacen  10771  seq3coll  10777  seq3shft  10802  resqrexlemfp1  10973  sqrtdiv  11006  climshftlemg  11265  climcn1  11271  climsqz  11298  climsqz2  11299  clim2ser  11300  clim2ser2  11301  isermulc2  11303  climub  11307  serf0  11315  fsum3cvg  11341  sumrbdc  11342  summodclem3  11343  summodclem2a  11344  zsumdc  11347  fsumf1o  11353  isumss  11354  fisumss  11355  isumss2  11356  fsum3cvg2  11357  fsum3cvg3  11359  fsumcl2lem  11361  fsumcllem  11362  fsumadd  11369  fsumsplit  11370  fsumsplitsn  11373  sumsplitdc  11395  fisumrev2  11409  fsum2mul  11416  fsum00  11425  telfsumo  11429  fsumparts  11433  iserabs  11438  cvgratnnlemabsle  11490  cvgratnn  11494  cvgratz  11495  mertenslemub  11497  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  clim2prod  11502  clim2divap  11503  prodfap0  11508  prodfrecap  11509  prodeq2  11520  fproddccvg  11535  prodrbdclem2  11536  prodmodc  11541  zproddc  11542  fprodf1o  11551  fprodssdc  11553  fprodunsn  11567  fprodcllem  11569  fprodabs  11579  fprodeq0  11580  fprodmodd  11604  eftlcvg  11650  negdvdsb  11769  dvdsnegb  11770  dvdsext  11815  addmodlteqALT  11819  nno  11865  infssuzex  11904  zsupssdc  11909  gcdsupex  11912  gcdsupcl  11913  bezoutlembz  11959  dvdssq  11986  eucalgf  12009  dvdslcm  12023  lcmledvds  12024  lcmeq0  12025  lcmcl  12026  lcmdvds  12033  lcmgcdeq  12037  divgcdcoprmex  12056  isprm5lem  12095  phibndlem  12170  phiprmpw  12176  pc2dvds  12283  pcmpt  12295  prmpwdvds  12307  1arith  12319  ctiunctlemf  12393  ctiunct  12395  grprinvd  12640  grpridd  12641  mndpropd  12676  mhmpropd  12689  0mhm  12704  grplcan  12761  opnssneib  12950  neissex  12959  tgrest  12963  iscnp3  12997  cnpnei  13013  cnrest  13029  tx1cn  13063  txcnp  13065  elbl3ps  13188  elbl3  13189  blininf  13218  blssexps  13223  blssex  13224  blpnfctr  13233  mopni2  13277  blsscls2  13287  metss  13288  bdmet  13296  metrest  13300  metcn  13308  txmetcn  13313  bl2ioo  13336  ivthinclemlr  13409  ivthinclemur  13411  dvcj  13467  dvfre  13468  coseq0q4123  13549  abssinper  13561  lgsval2lem  13705  lgsval4lem  13706  lgsneg  13719  lgsmod  13721  lgsdir2  13728  lgsdir  13730  lgsne0  13733  lgssq  13735  subctctexmid  14034  cvgcmp2n  14065  iswomninnlem  14081  nconstwlpo  14097