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  969  3ad2antr1  1189  xordidc  1444  po2nr  4412  sotricim  4426  fmptco  5821  fvtp1g  5870  dff13  5919  fcof1o  5940  isocnv  5962  isores2  5964  isoini  5969  f1oiso2  5978  acexmidlemab  6022  ovmpodf  6163  offval  6252  xp1st  6337  1stconst  6395  cnvf1olem  6398  f1od2  6409  mpoxopoveq  6449  nnaordi  6719  nnmordi  6727  erinxp  6821  dom2lem  6988  fundmen  7024  pw2f1odclem  7063  mapen  7075  ssenen  7080  fidifsnen  7100  difinfsnlem  7341  fodjum  7388  cc2lem  7528  ltsonq  7661  lt2addnq  7667  lt2mulnq  7668  ltexnqq  7671  prarloclemarch2  7682  enq0sym  7695  genprndl  7784  genprndu  7785  prmuloc  7829  distrlem1prl  7845  distrlem1pru  7846  ltsopr  7859  ltexprlemdisj  7869  ltexprlemfl  7872  ltexprlemfu  7874  addcanprlemu  7878  ltaprg  7882  mulcmpblnrlemg  8003  recexgt0sr  8036  mul4  8353  2addsub  8435  muladd  8605  ltleadd  8668  eqord1  8705  eqord2  8706  divmulap3  8899  divcanap7  8943  divadddivap  8949  lemul2a  9081  lemul12b  9083  ltmuldiv2  9097  ltdivmul  9098  ltdivmul2  9100  ledivmul2  9102  lemuldiv2  9104  lt2msq  9108  cju  9183  zextlt  9616  xrlttr  10074  xrre3  10101  ixxdisj  10182  iooshf  10231  icodisj  10271  iccf1o  10284  zssinfcl  10538  seqf1og  10829  expsubap  10895  bcval5  11071  hashfacen  11146  seq3coll  11152  swrdswrdlem  11334  swrdccatin2  11359  sqrt0rlem  11626  lenegsq  11718  zsumdc  12008  fisum0diag2  12071  prodmodclem2  12201  zproddc  12203  ndvdsadd  12555  lcmdvds  12714  oddpwdclemdc  12808  hashdvds  12856  phisum  12876  pcqmul  12939  pcmpt  12979  4sqlemffi  13032  4sqlem11  13037  ennnfonelemex  13098  grpinvid1  13698  grpinvid2  13699  grplcan  13708  grpnpncan0  13742  dfgrp3mlem  13744  dfgrp3m  13745  grplactcnv  13748  0nsg  13864  eqger  13874  resghm  13910  conjghm  13926  znunit  14738  psrbagconf1o  14757  psrgrp  14769  eltg2  14847  ssnei2  14951  restopnb  14975  txdis1cn  15072  txlm  15073  elbl2ps  15186  elbl2  15187  blininf  15218  xmeter  15230  xmetresbl  15234  bdxmet  15295  metrest  15300  dedekindicc  15427  limcimo  15459  dvmptfsum  15519  plycolemc  15552  dvdsppwf1o  15786  fsumdvdsmul  15788  sgmmul  15793  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2lem2  15884  upgriswlkdc  16284