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  4404  sotricim  4418  fmptco  5809  fvtp1g  5857  dff13  5904  fcof1o  5925  isocnv  5947  isores2  5949  isoini  5954  f1oiso2  5963  acexmidlemab  6007  ovmpodf  6148  offval  6238  xp1st  6323  1stconst  6381  cnvf1olem  6384  f1od2  6395  mpoxopoveq  6401  nnaordi  6671  nnmordi  6679  erinxp  6773  dom2lem  6940  fundmen  6976  pw2f1odclem  7015  mapen  7027  ssenen  7032  fidifsnen  7052  difinfsnlem  7289  fodjum  7336  cc2lem  7475  ltsonq  7608  lt2addnq  7614  lt2mulnq  7615  ltexnqq  7618  prarloclemarch2  7629  enq0sym  7642  genprndl  7731  genprndu  7732  prmuloc  7776  distrlem1prl  7792  distrlem1pru  7793  ltsopr  7806  ltexprlemdisj  7816  ltexprlemfl  7819  ltexprlemfu  7821  addcanprlemu  7825  ltaprg  7829  mulcmpblnrlemg  7950  recexgt0sr  7983  mul4  8301  2addsub  8383  muladd  8553  ltleadd  8616  eqord1  8653  eqord2  8654  divmulap3  8847  divcanap7  8891  divadddivap  8897  lemul2a  9029  lemul12b  9031  ltmuldiv2  9045  ltdivmul  9046  ltdivmul2  9048  ledivmul2  9050  lemuldiv2  9052  lt2msq  9056  cju  9131  zextlt  9562  xrlttr  10020  xrre3  10047  ixxdisj  10128  iooshf  10177  icodisj  10217  iccf1o  10229  zssinfcl  10482  seqf1og  10773  expsubap  10839  bcval5  11015  hashfacen  11090  seq3coll  11096  swrdswrdlem  11275  swrdccatin2  11300  sqrt0rlem  11554  lenegsq  11646  zsumdc  11935  fisum0diag2  11998  prodmodclem2  12128  zproddc  12130  ndvdsadd  12482  lcmdvds  12641  oddpwdclemdc  12735  hashdvds  12783  phisum  12803  pcqmul  12866  pcmpt  12906  4sqlemffi  12959  4sqlem11  12964  ennnfonelemex  13025  grpinvid1  13625  grpinvid2  13626  grplcan  13635  grpnpncan0  13669  dfgrp3mlem  13671  dfgrp3m  13672  grplactcnv  13675  0nsg  13791  eqger  13801  resghm  13837  conjghm  13853  znunit  14663  psrgrp  14689  eltg2  14767  ssnei2  14871  restopnb  14895  txdis1cn  14992  txlm  14993  elbl2ps  15106  elbl2  15107  blininf  15138  xmeter  15150  xmetresbl  15154  bdxmet  15215  metrest  15220  dedekindicc  15347  limcimo  15379  dvmptfsum  15439  plycolemc  15472  dvdsppwf1o  15703  fsumdvdsmul  15705  sgmmul  15710  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem2  15801  upgriswlkdc  16157