Theorem adantrr 471

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 108	. 2 |- ( ( ps /\ th ) -> ps )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan2 284	1 |- ( ( ph /\ ( ps /\ th ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad2ant2r  501  ad2ant2lr  502  dn1dc  950  3ad2antr1  1152  xordidc  1389  po2nr  4286  sotricim  4300  fmptco  5650  fvtp1g  5692  dff13  5735  fcof1o  5756  isocnv  5778  isores2  5780  isoini  5785  f1oiso2  5794  acexmidlemab  5835  ovmpodf  5969  offval  6056  xp1st  6130  1stconst  6185  cnvf1olem  6188  f1od2  6199  mpoxopoveq  6204  nnaordi  6472  nnmordi  6480  erinxp  6571  dom2lem  6734  fundmen  6768  mapen  6808  ssenen  6813  fidifsnen  6832  difinfsnlem  7060  fodjum  7106  cc2lem  7203  ltsonq  7335  lt2addnq  7341  lt2mulnq  7342  ltexnqq  7345  prarloclemarch2  7356  enq0sym  7369  genprndl  7458  genprndu  7459  prmuloc  7503  distrlem1prl  7519  distrlem1pru  7520  ltsopr  7533  ltexprlemdisj  7543  ltexprlemfl  7546  ltexprlemfu  7548  addcanprlemu  7552  ltaprg  7556  mulcmpblnrlemg  7677  recexgt0sr  7710  mul4  8026  2addsub  8108  muladd  8278  ltleadd  8340  eqord1  8377  eqord2  8378  divmulap3  8569  divcanap7  8613  divadddivap  8619  lemul2a  8750  lemul12b  8752  ltmuldiv2  8766  ltdivmul  8767  ltdivmul2  8769  ledivmul2  8771  lemuldiv2  8773  lt2msq  8777  cju  8852  zextlt  9279  xrlttr  9727  xrre3  9754  ixxdisj  9835  iooshf  9884  icodisj  9924  iccf1o  9936  expsubap  10499  bcval5  10672  hashfacen  10745  seq3coll  10751  sqrt0rlem  10941  lenegsq  11033  zsumdc  11321  fisum0diag2  11384  prodmodclem2  11514  zproddc  11516  ndvdsadd  11864  zssinfcl  11877  lcmdvds  12007  oddpwdclemdc  12101  hashdvds  12149  phisum  12168  pcqmul  12231  pcmpt  12269  ennnfonelemex  12343  eltg2  12653  ssnei2  12757  restopnb  12781  txdis1cn  12878  txlm  12879  elbl2ps  12992  elbl2  12993  blininf  13024  xmeter  13036  xmetresbl  13040  bdxmet  13101  metrest  13106  dedekindicc  13211  limcimo  13234