Theorem adantrr 479

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  ad2ant2r  509  ad2ant2lr  510  dn1dc  960  3ad2antr1  1162  xordidc  1399  po2nr  4310  sotricim  4324  fmptco  5683  fvtp1g  5725  dff13  5769  fcof1o  5790  isocnv  5812  isores2  5814  isoini  5819  f1oiso2  5828  acexmidlemab  5869  ovmpodf  6006  offval  6090  xp1st  6166  1stconst  6222  cnvf1olem  6225  f1od2  6236  mpoxopoveq  6241  nnaordi  6509  nnmordi  6517  erinxp  6609  dom2lem  6772  fundmen  6806  mapen  6846  ssenen  6851  fidifsnen  6870  difinfsnlem  7098  fodjum  7144  cc2lem  7265  ltsonq  7397  lt2addnq  7403  lt2mulnq  7404  ltexnqq  7407  prarloclemarch2  7418  enq0sym  7431  genprndl  7520  genprndu  7521  prmuloc  7565  distrlem1prl  7581  distrlem1pru  7582  ltsopr  7595  ltexprlemdisj  7605  ltexprlemfl  7608  ltexprlemfu  7610  addcanprlemu  7614  ltaprg  7618  mulcmpblnrlemg  7739  recexgt0sr  7772  mul4  8089  2addsub  8171  muladd  8341  ltleadd  8403  eqord1  8440  eqord2  8441  divmulap3  8634  divcanap7  8678  divadddivap  8684  lemul2a  8816  lemul12b  8818  ltmuldiv2  8832  ltdivmul  8833  ltdivmul2  8835  ledivmul2  8837  lemuldiv2  8839  lt2msq  8843  cju  8918  zextlt  9345  xrlttr  9795  xrre3  9822  ixxdisj  9903  iooshf  9952  icodisj  9992  iccf1o  10004  expsubap  10568  bcval5  10743  hashfacen  10816  seq3coll  10822  sqrt0rlem  11012  lenegsq  11104  zsumdc  11392  fisum0diag2  11455  prodmodclem2  11585  zproddc  11587  ndvdsadd  11936  zssinfcl  11949  lcmdvds  12079  oddpwdclemdc  12173  hashdvds  12221  phisum  12240  pcqmul  12303  pcmpt  12341  ennnfonelemex  12415  grpinvid1  12924  grpinvid2  12925  grplcan  12932  grpnpncan0  12966  dfgrp3mlem  12968  dfgrp3m  12969  grplactcnv  12972  0nsg  13074  eqger  13083  eltg2  13556  ssnei2  13660  restopnb  13684  txdis1cn  13781  txlm  13782  elbl2ps  13895  elbl2  13896  blininf  13927  xmeter  13939  xmetresbl  13943  bdxmet  14004  metrest  14009  dedekindicc  14114  limcimo  14137