Theorem adantrr 470

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  500  ad2ant2lr  501  dn1dc  944  3ad2antr1  1146  xordidc  1377  po2nr  4226  sotricim  4240  fmptco  5579  fvtp1g  5621  dff13  5662  fcof1o  5683  isocnv  5705  isores2  5707  isoini  5712  f1oiso2  5721  acexmidlemab  5761  ovmpodf  5895  offval  5982  xp1st  6056  1stconst  6111  cnvf1olem  6114  f1od2  6125  mpoxopoveq  6130  nnaordi  6397  nnmordi  6405  erinxp  6496  dom2lem  6659  fundmen  6693  mapen  6733  ssenen  6738  fidifsnen  6757  difinfsnlem  6977  fodjum  7011  ltsonq  7199  lt2addnq  7205  lt2mulnq  7206  ltexnqq  7209  prarloclemarch2  7220  enq0sym  7233  genprndl  7322  genprndu  7323  prmuloc  7367  distrlem1prl  7383  distrlem1pru  7384  ltsopr  7397  ltexprlemdisj  7407  ltexprlemfl  7410  ltexprlemfu  7412  addcanprlemu  7416  ltaprg  7420  mulcmpblnrlemg  7541  recexgt0sr  7574  mul4  7887  2addsub  7969  muladd  8139  ltleadd  8201  eqord1  8238  eqord2  8239  divmulap3  8430  divcanap7  8474  divadddivap  8480  lemul2a  8610  lemul12b  8612  ltmuldiv2  8626  ltdivmul  8627  ltdivmul2  8629  ledivmul2  8631  lemuldiv2  8633  lt2msq  8637  cju  8712  zextlt  9136  xrlttr  9574  xrre3  9598  ixxdisj  9679  iooshf  9728  icodisj  9768  iccf1o  9780  expsubap  10334  bcval5  10502  hashfacen  10572  seq3coll  10578  sqrt0rlem  10768  lenegsq  10860  zsumdc  11146  fisum0diag2  11209  ndvdsadd  11617  zssinfcl  11630  lcmdvds  11749  oddpwdclemdc  11840  hashdvds  11886  ennnfonelemex  11916  eltg2  12211  ssnei2  12315  restopnb  12339  txdis1cn  12436  txlm  12437  elbl2ps  12550  elbl2  12551  blininf  12582  xmeter  12594  xmetresbl  12598  bdxmet  12659  metrest  12664  dedekindicc  12769  limcimo  12792