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  966  3ad2antr1  1186  xordidc  1441  po2nr  4399  sotricim  4413  fmptco  5800  fvtp1g  5846  dff13  5891  fcof1o  5912  isocnv  5934  isores2  5936  isoini  5941  f1oiso2  5950  acexmidlemab  5994  ovmpodf  6135  offval  6224  xp1st  6309  1stconst  6365  cnvf1olem  6368  f1od2  6379  mpoxopoveq  6384  nnaordi  6652  nnmordi  6660  erinxp  6754  dom2lem  6921  fundmen  6957  pw2f1odclem  6991  mapen  7003  ssenen  7008  fidifsnen  7028  difinfsnlem  7262  fodjum  7309  cc2lem  7448  ltsonq  7581  lt2addnq  7587  lt2mulnq  7588  ltexnqq  7591  prarloclemarch2  7602  enq0sym  7615  genprndl  7704  genprndu  7705  prmuloc  7749  distrlem1prl  7765  distrlem1pru  7766  ltsopr  7779  ltexprlemdisj  7789  ltexprlemfl  7792  ltexprlemfu  7794  addcanprlemu  7798  ltaprg  7802  mulcmpblnrlemg  7923  recexgt0sr  7956  mul4  8274  2addsub  8356  muladd  8526  ltleadd  8589  eqord1  8626  eqord2  8627  divmulap3  8820  divcanap7  8864  divadddivap  8870  lemul2a  9002  lemul12b  9004  ltmuldiv2  9018  ltdivmul  9019  ltdivmul2  9021  ledivmul2  9023  lemuldiv2  9025  lt2msq  9029  cju  9104  zextlt  9535  xrlttr  9987  xrre3  10014  ixxdisj  10095  iooshf  10144  icodisj  10184  iccf1o  10196  zssinfcl  10447  seqf1og  10738  expsubap  10804  bcval5  10980  hashfacen  11053  seq3coll  11059  swrdswrdlem  11231  swrdccatin2  11256  sqrt0rlem  11509  lenegsq  11601  zsumdc  11890  fisum0diag2  11953  prodmodclem2  12083  zproddc  12085  ndvdsadd  12437  lcmdvds  12596  oddpwdclemdc  12690  hashdvds  12738  phisum  12758  pcqmul  12821  pcmpt  12861  4sqlemffi  12914  4sqlem11  12919  ennnfonelemex  12980  grpinvid1  13580  grpinvid2  13581  grplcan  13590  grpnpncan0  13624  dfgrp3mlem  13626  dfgrp3m  13627  grplactcnv  13630  0nsg  13746  eqger  13756  resghm  13792  conjghm  13808  znunit  14617  psrgrp  14643  eltg2  14721  ssnei2  14825  restopnb  14849  txdis1cn  14946  txlm  14947  elbl2ps  15060  elbl2  15061  blininf  15092  xmeter  15104  xmetresbl  15108  bdxmet  15169  metrest  15174  dedekindicc  15301  limcimo  15333  dvmptfsum  15393  plycolemc  15426  dvdsppwf1o  15657  fsumdvdsmul  15659  sgmmul  15664  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem2  15755