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  966  3ad2antr1  1186  xordidc  1441  po2nr  4400  sotricim  4414  fmptco  5801  fvtp1g  5847  dff13  5892  fcof1o  5913  isocnv  5935  isores2  5937  isoini  5942  f1oiso2  5951  acexmidlemab  5995  ovmpodf  6136  offval  6226  xp1st  6311  1stconst  6367  cnvf1olem  6370  f1od2  6381  mpoxopoveq  6386  nnaordi  6654  nnmordi  6662  erinxp  6756  dom2lem  6923  fundmen  6959  pw2f1odclem  6995  mapen  7007  ssenen  7012  fidifsnen  7032  difinfsnlem  7266  fodjum  7313  cc2lem  7452  ltsonq  7585  lt2addnq  7591  lt2mulnq  7592  ltexnqq  7595  prarloclemarch2  7606  enq0sym  7619  genprndl  7708  genprndu  7709  prmuloc  7753  distrlem1prl  7769  distrlem1pru  7770  ltsopr  7783  ltexprlemdisj  7793  ltexprlemfl  7796  ltexprlemfu  7798  addcanprlemu  7802  ltaprg  7806  mulcmpblnrlemg  7927  recexgt0sr  7960  mul4  8278  2addsub  8360  muladd  8530  ltleadd  8593  eqord1  8630  eqord2  8631  divmulap3  8824  divcanap7  8868  divadddivap  8874  lemul2a  9006  lemul12b  9008  ltmuldiv2  9022  ltdivmul  9023  ltdivmul2  9025  ledivmul2  9027  lemuldiv2  9029  lt2msq  9033  cju  9108  zextlt  9539  xrlttr  9991  xrre3  10018  ixxdisj  10099  iooshf  10148  icodisj  10188  iccf1o  10200  zssinfcl  10452  seqf1og  10743  expsubap  10809  bcval5  10985  hashfacen  11058  seq3coll  11064  swrdswrdlem  11236  swrdccatin2  11261  sqrt0rlem  11514  lenegsq  11606  zsumdc  11895  fisum0diag2  11958  prodmodclem2  12088  zproddc  12090  ndvdsadd  12442  lcmdvds  12601  oddpwdclemdc  12695  hashdvds  12743  phisum  12763  pcqmul  12826  pcmpt  12866  4sqlemffi  12919  4sqlem11  12924  ennnfonelemex  12985  grpinvid1  13585  grpinvid2  13586  grplcan  13595  grpnpncan0  13629  dfgrp3mlem  13631  dfgrp3m  13632  grplactcnv  13635  0nsg  13751  eqger  13761  resghm  13797  conjghm  13813  znunit  14623  psrgrp  14649  eltg2  14727  ssnei2  14831  restopnb  14855  txdis1cn  14952  txlm  14953  elbl2ps  15066  elbl2  15067  blininf  15098  xmeter  15110  xmetresbl  15114  bdxmet  15175  metrest  15180  dedekindicc  15307  limcimo  15339  dvmptfsum  15399  plycolemc  15432  dvdsppwf1o  15663  fsumdvdsmul  15665  sgmmul  15670  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem2  15761  upgriswlkdc  16071