Theorem adantrr 466

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 282	1 |- ( ( ph /\ ( ps /\ th ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ad2ant2r  496  ad2ant2lr  497  dn1dc  912  3ad2antr1  1114  xordidc  1345  po2nr  4169  sotricim  4183  fmptco  5518  fvtp1g  5560  dff13  5601  fcof1o  5622  isocnv  5644  isores2  5646  isoini  5651  f1oiso2  5660  acexmidlemab  5700  ovmpodf  5834  offval  5921  xp1st  5994  1stconst  6048  cnvf1olem  6051  f1od2  6062  mpoxopoveq  6067  nnaordi  6334  nnmordi  6342  erinxp  6433  dom2lem  6596  fundmen  6630  mapen  6669  ssenen  6674  fidifsnen  6693  difinfsnlem  6899  fodjum  6930  ltsonq  7107  lt2addnq  7113  lt2mulnq  7114  ltexnqq  7117  prarloclemarch2  7128  enq0sym  7141  genprndl  7230  genprndu  7231  prmuloc  7275  distrlem1prl  7291  distrlem1pru  7292  ltsopr  7305  ltexprlemdisj  7315  ltexprlemfl  7318  ltexprlemfu  7320  addcanprlemu  7324  ltaprg  7328  mulcmpblnrlemg  7436  recexgt0sr  7469  mul4  7765  2addsub  7847  muladd  8013  ltleadd  8075  eqord1  8112  eqord2  8113  divmulap3  8298  divcanap7  8342  divadddivap  8348  lemul2a  8475  lemul12b  8477  ltmuldiv2  8491  ltdivmul  8492  ltdivmul2  8494  ledivmul2  8496  lemuldiv2  8498  lt2msq  8502  cju  8577  zextlt  8995  xrlttr  9422  xrre3  9446  ixxdisj  9527  iooshf  9576  icodisj  9616  iccf1o  9628  expsubap  10182  bcval5  10350  hashfacen  10420  seq3coll  10426  sqrt0rlem  10615  lenegsq  10707  zsumdc  10992  fisum0diag2  11055  ndvdsadd  11423  zssinfcl  11436  lcmdvds  11553  oddpwdclemdc  11643  hashdvds  11689  ennnfonelemex  11719  eltg2  12004  ssnei2  12108  restopnb  12132  txdis1cn  12228  txlm  12229  elbl2ps  12320  elbl2  12321  blininf  12352  xmeter  12364  xmetresbl  12368  bdxmet  12429  metrest  12434  limcimo  12514