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  4430  sotricim  4444  fmptco  5843  fvtp1g  5892  dff13  5941  fcof1o  5962  isocnv  5984  isores2  5986  isoini  5991  f1oiso2  6000  acexmidlemab  6044  ovmpodf  6185  offval  6274  xp1st  6359  1stconst  6417  cnvf1olem  6420  f1od2  6431  mpoxopoveq  6471  nnaordi  6741  nnmordi  6749  erinxp  6843  dom2lem  7011  fundmen  7047  pw2f1odclem  7087  mapen  7099  ssenen  7105  fidifsnen  7125  difinfsnlem  7390  fodjum  7437  cc2lem  7580  ltsonq  7713  lt2addnq  7719  lt2mulnq  7720  ltexnqq  7723  prarloclemarch2  7734  enq0sym  7747  genprndl  7836  genprndu  7837  prmuloc  7881  distrlem1prl  7897  distrlem1pru  7898  ltsopr  7911  ltexprlemdisj  7921  ltexprlemfl  7924  ltexprlemfu  7926  addcanprlemu  7930  ltaprg  7934  mulcmpblnrlemg  8055  recexgt0sr  8088  mul4  8405  2addsub  8487  muladd  8657  ltleadd  8720  eqord1  8757  eqord2  8758  divmulap3  8951  divcanap7  8995  divadddivap  9001  lemul2a  9133  lemul12b  9135  ltmuldiv2  9149  ltdivmul  9150  ltdivmul2  9152  ledivmul2  9154  lemuldiv2  9156  lt2msq  9160  cju  9235  zextlt  9670  xrlttr  10128  xrre3  10155  ixxdisj  10236  iooshf  10285  icodisj  10325  iccf1o  10338  zssinfcl  10592  seqf1og  10883  expsubap  10949  bcval5  11125  hashmap  11192  hashfacen  11208  seq3coll  11214  swrdswrdlem  11396  swrdccatin2  11421  sqrt0rlem  11688  lenegsq  11780  zsumdc  12070  fisum0diag2  12133  prodmodclem2  12263  zproddc  12265  ndvdsadd  12617  lcmdvds  12776  oddpwdclemdc  12870  hashdvds  12918  phisum  12938  pcqmul  13001  pcmpt  13041  4sqlemffi  13094  4sqlem11  13099  ennnfonelemex  13165  grpinvid1  13765  grpinvid2  13766  grplcan  13775  grpnpncan0  13809  dfgrp3mlem  13811  dfgrp3m  13812  grplactcnv  13815  0nsg  13931  eqger  13941  resghm  13977  conjghm  13993  znunit  14807  psrbagconf1o  14828  psrgrp  14840  eltg2  14918  ssnei2  15022  restopnb  15046  txdis1cn  15143  txlm  15144  elbl2ps  15257  elbl2  15258  blininf  15289  xmeter  15301  xmetresbl  15305  bdxmet  15366  metrest  15371  dedekindicc  15498  limcimo  15530  dvmptfsum  15590  plycolemc  15623  dvdsppwf1o  15857  fsumdvdsmul  15859  sgmmul  15864  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem2  15955  upgriswlkdc  16355