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  4400  sotricim  4414  fmptco  5803  fvtp1g  5851  dff13  5898  fcof1o  5919  isocnv  5941  isores2  5943  isoini  5948  f1oiso2  5957  acexmidlemab  6001  ovmpodf  6142  offval  6232  xp1st  6317  1stconst  6373  cnvf1olem  6376  f1od2  6387  mpoxopoveq  6392  nnaordi  6662  nnmordi  6670  erinxp  6764  dom2lem  6931  fundmen  6967  pw2f1odclem  7003  mapen  7015  ssenen  7020  fidifsnen  7040  difinfsnlem  7277  fodjum  7324  cc2lem  7463  ltsonq  7596  lt2addnq  7602  lt2mulnq  7603  ltexnqq  7606  prarloclemarch2  7617  enq0sym  7630  genprndl  7719  genprndu  7720  prmuloc  7764  distrlem1prl  7780  distrlem1pru  7781  ltsopr  7794  ltexprlemdisj  7804  ltexprlemfl  7807  ltexprlemfu  7809  addcanprlemu  7813  ltaprg  7817  mulcmpblnrlemg  7938  recexgt0sr  7971  mul4  8289  2addsub  8371  muladd  8541  ltleadd  8604  eqord1  8641  eqord2  8642  divmulap3  8835  divcanap7  8879  divadddivap  8885  lemul2a  9017  lemul12b  9019  ltmuldiv2  9033  ltdivmul  9034  ltdivmul2  9036  ledivmul2  9038  lemuldiv2  9040  lt2msq  9044  cju  9119  zextlt  9550  xrlttr  10003  xrre3  10030  ixxdisj  10111  iooshf  10160  icodisj  10200  iccf1o  10212  zssinfcl  10464  seqf1og  10755  expsubap  10821  bcval5  10997  hashfacen  11071  seq3coll  11077  swrdswrdlem  11251  swrdccatin2  11276  sqrt0rlem  11529  lenegsq  11621  zsumdc  11910  fisum0diag2  11973  prodmodclem2  12103  zproddc  12105  ndvdsadd  12457  lcmdvds  12616  oddpwdclemdc  12710  hashdvds  12758  phisum  12778  pcqmul  12841  pcmpt  12881  4sqlemffi  12934  4sqlem11  12939  ennnfonelemex  13000  grpinvid1  13600  grpinvid2  13601  grplcan  13610  grpnpncan0  13644  dfgrp3mlem  13646  dfgrp3m  13647  grplactcnv  13650  0nsg  13766  eqger  13776  resghm  13812  conjghm  13828  znunit  14638  psrgrp  14664  eltg2  14742  ssnei2  14846  restopnb  14870  txdis1cn  14967  txlm  14968  elbl2ps  15081  elbl2  15082  blininf  15113  xmeter  15125  xmetresbl  15129  bdxmet  15190  metrest  15195  dedekindicc  15322  limcimo  15354  dvmptfsum  15414  plycolemc  15447  dvdsppwf1o  15678  fsumdvdsmul  15680  sgmmul  15685  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem2  15776  upgriswlkdc  16101