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  968  3ad2antr1  1188  xordidc  1443  po2nr  4406  sotricim  4420  fmptco  5813  fvtp1g  5861  dff13  5908  fcof1o  5929  isocnv  5951  isores2  5953  isoini  5958  f1oiso2  5967  acexmidlemab  6011  ovmpodf  6152  offval  6242  xp1st  6327  1stconst  6385  cnvf1olem  6388  f1od2  6399  mpoxopoveq  6405  nnaordi  6675  nnmordi  6683  erinxp  6777  dom2lem  6944  fundmen  6980  pw2f1odclem  7019  mapen  7031  ssenen  7036  fidifsnen  7056  difinfsnlem  7297  fodjum  7344  cc2lem  7484  ltsonq  7617  lt2addnq  7623  lt2mulnq  7624  ltexnqq  7627  prarloclemarch2  7638  enq0sym  7651  genprndl  7740  genprndu  7741  prmuloc  7785  distrlem1prl  7801  distrlem1pru  7802  ltsopr  7815  ltexprlemdisj  7825  ltexprlemfl  7828  ltexprlemfu  7830  addcanprlemu  7834  ltaprg  7838  mulcmpblnrlemg  7959  recexgt0sr  7992  mul4  8310  2addsub  8392  muladd  8562  ltleadd  8625  eqord1  8662  eqord2  8663  divmulap3  8856  divcanap7  8900  divadddivap  8906  lemul2a  9038  lemul12b  9040  ltmuldiv2  9054  ltdivmul  9055  ltdivmul2  9057  ledivmul2  9059  lemuldiv2  9061  lt2msq  9065  cju  9140  zextlt  9571  xrlttr  10029  xrre3  10056  ixxdisj  10137  iooshf  10186  icodisj  10226  iccf1o  10238  zssinfcl  10491  seqf1og  10782  expsubap  10848  bcval5  11024  hashfacen  11099  seq3coll  11105  swrdswrdlem  11284  swrdccatin2  11309  sqrt0rlem  11563  lenegsq  11655  zsumdc  11944  fisum0diag2  12007  prodmodclem2  12137  zproddc  12139  ndvdsadd  12491  lcmdvds  12650  oddpwdclemdc  12744  hashdvds  12792  phisum  12812  pcqmul  12875  pcmpt  12915  4sqlemffi  12968  4sqlem11  12973  ennnfonelemex  13034  grpinvid1  13634  grpinvid2  13635  grplcan  13644  grpnpncan0  13678  dfgrp3mlem  13680  dfgrp3m  13681  grplactcnv  13684  0nsg  13800  eqger  13810  resghm  13846  conjghm  13862  znunit  14672  psrgrp  14698  eltg2  14776  ssnei2  14880  restopnb  14904  txdis1cn  15001  txlm  15002  elbl2ps  15115  elbl2  15116  blininf  15147  xmeter  15159  xmetresbl  15163  bdxmet  15224  metrest  15229  dedekindicc  15356  limcimo  15388  dvmptfsum  15448  plycolemc  15481  dvdsppwf1o  15712  fsumdvdsmul  15714  sgmmul  15719  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem2  15810  upgriswlkdc  16210