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  1418  po2nr  4355  sotricim  4369  fmptco  5745  fvtp1g  5791  dff13  5836  fcof1o  5857  isocnv  5879  isores2  5881  isoini  5886  f1oiso2  5895  acexmidlemab  5937  ovmpodf  6076  offval  6165  xp1st  6250  1stconst  6306  cnvf1olem  6309  f1od2  6320  mpoxopoveq  6325  nnaordi  6593  nnmordi  6601  erinxp  6695  dom2lem  6862  fundmen  6897  pw2f1odclem  6930  mapen  6942  ssenen  6947  fidifsnen  6966  difinfsnlem  7200  fodjum  7247  cc2lem  7377  ltsonq  7510  lt2addnq  7516  lt2mulnq  7517  ltexnqq  7520  prarloclemarch2  7531  enq0sym  7544  genprndl  7633  genprndu  7634  prmuloc  7678  distrlem1prl  7694  distrlem1pru  7695  ltsopr  7708  ltexprlemdisj  7718  ltexprlemfl  7721  ltexprlemfu  7723  addcanprlemu  7727  ltaprg  7731  mulcmpblnrlemg  7852  recexgt0sr  7885  mul4  8203  2addsub  8285  muladd  8455  ltleadd  8518  eqord1  8555  eqord2  8556  divmulap3  8749  divcanap7  8793  divadddivap  8799  lemul2a  8931  lemul12b  8933  ltmuldiv2  8947  ltdivmul  8948  ltdivmul2  8950  ledivmul2  8952  lemuldiv2  8954  lt2msq  8958  cju  9033  zextlt  9464  xrlttr  9916  xrre3  9943  ixxdisj  10024  iooshf  10073  icodisj  10113  iccf1o  10125  zssinfcl  10373  seqf1og  10664  expsubap  10730  bcval5  10906  hashfacen  10979  seq3coll  10985  sqrt0rlem  11285  lenegsq  11377  zsumdc  11666  fisum0diag2  11729  prodmodclem2  11859  zproddc  11861  ndvdsadd  12213  lcmdvds  12372  oddpwdclemdc  12466  hashdvds  12514  phisum  12534  pcqmul  12597  pcmpt  12637  4sqlemffi  12690  4sqlem11  12695  ennnfonelemex  12756  grpinvid1  13355  grpinvid2  13356  grplcan  13365  grpnpncan0  13399  dfgrp3mlem  13401  dfgrp3m  13402  grplactcnv  13405  0nsg  13521  eqger  13531  resghm  13567  conjghm  13583  znunit  14392  psrgrp  14418  eltg2  14496  ssnei2  14600  restopnb  14624  txdis1cn  14721  txlm  14722  elbl2ps  14835  elbl2  14836  blininf  14867  xmeter  14879  xmetresbl  14883  bdxmet  14944  metrest  14949  dedekindicc  15076  limcimo  15108  dvmptfsum  15168  plycolemc  15201  dvdsppwf1o  15432  fsumdvdsmul  15434  sgmmul  15439  lgsquadlem1  15525  lgsquadlem2  15526  lgsquad2lem2  15530