Theorem adantrr 476

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  506  ad2ant2lr  507  dn1dc  955  3ad2antr1  1157  xordidc  1394  po2nr  4294  sotricim  4308  fmptco  5662  fvtp1g  5704  dff13  5747  fcof1o  5768  isocnv  5790  isores2  5792  isoini  5797  f1oiso2  5806  acexmidlemab  5847  ovmpodf  5984  offval  6068  xp1st  6144  1stconst  6200  cnvf1olem  6203  f1od2  6214  mpoxopoveq  6219  nnaordi  6487  nnmordi  6495  erinxp  6587  dom2lem  6750  fundmen  6784  mapen  6824  ssenen  6829  fidifsnen  6848  difinfsnlem  7076  fodjum  7122  cc2lem  7228  ltsonq  7360  lt2addnq  7366  lt2mulnq  7367  ltexnqq  7370  prarloclemarch2  7381  enq0sym  7394  genprndl  7483  genprndu  7484  prmuloc  7528  distrlem1prl  7544  distrlem1pru  7545  ltsopr  7558  ltexprlemdisj  7568  ltexprlemfl  7571  ltexprlemfu  7573  addcanprlemu  7577  ltaprg  7581  mulcmpblnrlemg  7702  recexgt0sr  7735  mul4  8051  2addsub  8133  muladd  8303  ltleadd  8365  eqord1  8402  eqord2  8403  divmulap3  8594  divcanap7  8638  divadddivap  8644  lemul2a  8775  lemul12b  8777  ltmuldiv2  8791  ltdivmul  8792  ltdivmul2  8794  ledivmul2  8796  lemuldiv2  8798  lt2msq  8802  cju  8877  zextlt  9304  xrlttr  9752  xrre3  9779  ixxdisj  9860  iooshf  9909  icodisj  9949  iccf1o  9961  expsubap  10524  bcval5  10697  hashfacen  10771  seq3coll  10777  sqrt0rlem  10967  lenegsq  11059  zsumdc  11347  fisum0diag2  11410  prodmodclem2  11540  zproddc  11542  ndvdsadd  11890  zssinfcl  11903  lcmdvds  12033  oddpwdclemdc  12127  hashdvds  12175  phisum  12194  pcqmul  12257  pcmpt  12295  ennnfonelemex  12369  grpinvid1  12754  grpinvid2  12755  grplcan  12761  eltg2  12847  ssnei2  12951  restopnb  12975  txdis1cn  13072  txlm  13073  elbl2ps  13186  elbl2  13187  blininf  13218  xmeter  13230  xmetresbl  13234  bdxmet  13295  metrest  13300  dedekindicc  13405  limcimo  13428