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  969  3ad2antr1  1189  xordidc  1444  po2nr  4435  sotricim  4449  fmptco  5848  fvtp1g  5897  dff13  5947  fcof1o  5968  isocnv  5990  isores2  5992  isoini  5997  f1oiso2  6006  acexmidlemab  6052  ovmpodf  6193  offval  6283  xp1st  6372  1stconst  6430  cnvf1olem  6433  f1od2  6444  mpoxopoveq  6484  nnaordi  6754  nnmordi  6762  erinxp  6856  dom2lem  7024  fundmen  7060  pw2f1odclem  7100  mapen  7112  ssenen  7118  fidifsnen  7138  difinfsnlem  7403  fodjum  7450  cc2lem  7596  ltsonq  7729  lt2addnq  7735  lt2mulnq  7736  ltexnqq  7739  prarloclemarch2  7750  enq0sym  7763  genprndl  7852  genprndu  7853  prmuloc  7897  distrlem1prl  7913  distrlem1pru  7914  ltsopr  7927  ltexprlemdisj  7937  ltexprlemfl  7940  ltexprlemfu  7942  addcanprlemu  7946  ltaprg  7950  mulcmpblnrlemg  8071  recexgt0sr  8104  mul4  8421  2addsub  8503  muladd  8674  ltleadd  8737  eqord1  8774  eqord2  8775  divmulap3  8968  divcanap7  9012  divadddivap  9018  lemul2a  9150  lemul12b  9152  ltmuldiv2  9166  ltdivmul  9167  ltdivmul2  9169  ledivmul2  9171  lemuldiv2  9173  lt2msq  9177  cju  9252  zextlt  9688  xrlttr  10147  xrre3  10174  ixxdisj  10255  iooshf  10304  icodisj  10344  iccf1o  10357  zssinfcl  10614  seqf1og  10907  expsubap  10973  bcval5  11150  hashmap  11217  hashfacen  11233  seq3coll  11239  swrdswrdlem  11421  swrdccatin2  11446  sqrt0rlem  11713  lenegsq  11805  zsumdc  12095  fisum0diag2  12158  prodmodclem2  12288  zproddc  12290  ndvdsadd  12642  lcmdvds  12801  oddpwdclemdc  12895  hashdvds  12943  phisum  12963  pcqmul  13026  pcmpt  13066  4sqlemffi  13119  4sqlem11  13124  ballotfilemfc0  13176  ballotfilemfcc  13177  ennnfonelemex  13249  grpinvid1  13807  grpinvid2  13808  grplcan  13817  grpnpncan0  13851  dfgrp3mlem  13853  dfgrp3m  13854  grplactcnv  13857  0nsg  13967  eqger  13977  resghm  14013  conjghm  14029  znunit  14933  psrbagconf1o  14954  psrgrp  14966  eltg2  15044  ssnei2  15148  restopnb  15172  txdis1cn  15269  txlm  15270  elbl2ps  15383  elbl2  15384  blininf  15415  xmeter  15427  xmetresbl  15431  bdxmet  15492  metrest  15497  dedekindicc  15624  limcimo  15656  dvmptfsum  15716  plycolemc  15749  dvdsppwf1o  15983  fsumdvdsmul  15985  sgmmul  15990  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem2  16081  upgriswlkdc  16481