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  11256  lenegsq  11348  zsumdc  11637  fisum0diag2  11700  prodmodclem2  11830  zproddc  11832  ndvdsadd  12184  lcmdvds  12343  oddpwdclemdc  12437  hashdvds  12485  phisum  12505  pcqmul  12568  pcmpt  12608  4sqlemffi  12661  4sqlem11  12666  ennnfonelemex  12727  grpinvid1  13326  grpinvid2  13327  grplcan  13336  grpnpncan0  13370  dfgrp3mlem  13372  dfgrp3m  13373  grplactcnv  13376  0nsg  13492  eqger  13502  resghm  13538  conjghm  13554  znunit  14363  psrgrp  14389  eltg2  14467  ssnei2  14571  restopnb  14595  txdis1cn  14692  txlm  14693  elbl2ps  14806  elbl2  14807  blininf  14838  xmeter  14850  xmetresbl  14854  bdxmet  14915  metrest  14920  dedekindicc  15047  limcimo  15079  dvmptfsum  15139  plycolemc  15172  dvdsppwf1o  15403  fsumdvdsmul  15405  sgmmul  15410  lgsquadlem1  15496  lgsquadlem2  15497  lgsquad2lem2  15501