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  945  3ad2antr1  1147  xordidc  1378  po2nr  4239  sotricim  4253  fmptco  5594  fvtp1g  5636  dff13  5677  fcof1o  5698  isocnv  5720  isores2  5722  isoini  5727  f1oiso2  5736  acexmidlemab  5776  ovmpodf  5910  offval  5997  xp1st  6071  1stconst  6126  cnvf1olem  6129  f1od2  6140  mpoxopoveq  6145  nnaordi  6412  nnmordi  6420  erinxp  6511  dom2lem  6674  fundmen  6708  mapen  6748  ssenen  6753  fidifsnen  6772  difinfsnlem  6992  fodjum  7026  cc2lem  7098  ltsonq  7230  lt2addnq  7236  lt2mulnq  7237  ltexnqq  7240  prarloclemarch2  7251  enq0sym  7264  genprndl  7353  genprndu  7354  prmuloc  7398  distrlem1prl  7414  distrlem1pru  7415  ltsopr  7428  ltexprlemdisj  7438  ltexprlemfl  7441  ltexprlemfu  7443  addcanprlemu  7447  ltaprg  7451  mulcmpblnrlemg  7572  recexgt0sr  7605  mul4  7918  2addsub  8000  muladd  8170  ltleadd  8232  eqord1  8269  eqord2  8270  divmulap3  8461  divcanap7  8505  divadddivap  8511  lemul2a  8641  lemul12b  8643  ltmuldiv2  8657  ltdivmul  8658  ltdivmul2  8660  ledivmul2  8662  lemuldiv2  8664  lt2msq  8668  cju  8743  zextlt  9167  xrlttr  9611  xrre3  9635  ixxdisj  9716  iooshf  9765  icodisj  9805  iccf1o  9817  expsubap  10372  bcval5  10541  hashfacen  10611  seq3coll  10617  sqrt0rlem  10807  lenegsq  10899  zsumdc  11185  fisum0diag2  11248  prodmodclem2  11378  zproddc  11380  ndvdsadd  11664  zssinfcl  11677  lcmdvds  11796  oddpwdclemdc  11887  hashdvds  11933  ennnfonelemex  11963  eltg2  12261  ssnei2  12365  restopnb  12389  txdis1cn  12486  txlm  12487  elbl2ps  12600  elbl2  12601  blininf  12632  xmeter  12644  xmetresbl  12648  bdxmet  12709  metrest  12714  dedekindicc  12819  limcimo  12842