Theorem adantrr 479

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

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ps /\ th ) -> ps )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan2 286	1 |- ( ( ph /\ ( ps /\ th ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  ad2ant2r  509  ad2ant2lr  510  dn1dc  962  3ad2antr1  1164  xordidc  1410  po2nr  4327  sotricim  4341  fmptco  5703  fvtp1g  5745  dff13  5790  fcof1o  5811  isocnv  5833  isores2  5835  isoini  5840  f1oiso2  5849  acexmidlemab  5890  ovmpodf  6028  offval  6114  xp1st  6190  1stconst  6246  cnvf1olem  6249  f1od2  6260  mpoxopoveq  6265  nnaordi  6533  nnmordi  6541  erinxp  6635  dom2lem  6798  fundmen  6832  pw2f1odclem  6862  mapen  6874  ssenen  6879  fidifsnen  6898  difinfsnlem  7128  fodjum  7174  cc2lem  7295  ltsonq  7427  lt2addnq  7433  lt2mulnq  7434  ltexnqq  7437  prarloclemarch2  7448  enq0sym  7461  genprndl  7550  genprndu  7551  prmuloc  7595  distrlem1prl  7611  distrlem1pru  7612  ltsopr  7625  ltexprlemdisj  7635  ltexprlemfl  7638  ltexprlemfu  7640  addcanprlemu  7644  ltaprg  7648  mulcmpblnrlemg  7769  recexgt0sr  7802  mul4  8119  2addsub  8201  muladd  8371  ltleadd  8433  eqord1  8470  eqord2  8471  divmulap3  8664  divcanap7  8708  divadddivap  8714  lemul2a  8846  lemul12b  8848  ltmuldiv2  8862  ltdivmul  8863  ltdivmul2  8865  ledivmul2  8867  lemuldiv2  8869  lt2msq  8873  cju  8948  zextlt  9375  xrlttr  9825  xrre3  9852  ixxdisj  9933  iooshf  9982  icodisj  10022  iccf1o  10034  expsubap  10599  bcval5  10775  hashfacen  10848  seq3coll  10854  sqrt0rlem  11044  lenegsq  11136  zsumdc  11424  fisum0diag2  11487  prodmodclem2  11617  zproddc  11619  ndvdsadd  11968  zssinfcl  11981  lcmdvds  12111  oddpwdclemdc  12205  hashdvds  12253  phisum  12272  pcqmul  12335  pcmpt  12375  4sqlemffi  12428  4sqlem11  12433  ennnfonelemex  12465  grpinvid1  12996  grpinvid2  12997  grplcan  13006  grpnpncan0  13040  dfgrp3mlem  13042  dfgrp3m  13043  grplactcnv  13046  0nsg  13153  eqger  13163  resghm  13199  conjghm  13215  eltg2  14010  ssnei2  14114  restopnb  14138  txdis1cn  14235  txlm  14236  elbl2ps  14349  elbl2  14350  blininf  14381  xmeter  14393  xmetresbl  14397  bdxmet  14458  metrest  14463  dedekindicc  14568  limcimo  14591