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  962  3ad2antr1  1164  xordidc  1410  po2nr  4344  sotricim  4358  fmptco  5728  fvtp1g  5770  dff13  5815  fcof1o  5836  isocnv  5858  isores2  5860  isoini  5865  f1oiso2  5874  acexmidlemab  5916  ovmpodf  6054  offval  6143  xp1st  6223  1stconst  6279  cnvf1olem  6282  f1od2  6293  mpoxopoveq  6298  nnaordi  6566  nnmordi  6574  erinxp  6668  dom2lem  6831  fundmen  6865  pw2f1odclem  6895  mapen  6907  ssenen  6912  fidifsnen  6931  difinfsnlem  7165  fodjum  7212  cc2lem  7333  ltsonq  7465  lt2addnq  7471  lt2mulnq  7472  ltexnqq  7475  prarloclemarch2  7486  enq0sym  7499  genprndl  7588  genprndu  7589  prmuloc  7633  distrlem1prl  7649  distrlem1pru  7650  ltsopr  7663  ltexprlemdisj  7673  ltexprlemfl  7676  ltexprlemfu  7678  addcanprlemu  7682  ltaprg  7686  mulcmpblnrlemg  7807  recexgt0sr  7840  mul4  8158  2addsub  8240  muladd  8410  ltleadd  8473  eqord1  8510  eqord2  8511  divmulap3  8704  divcanap7  8748  divadddivap  8754  lemul2a  8886  lemul12b  8888  ltmuldiv2  8902  ltdivmul  8903  ltdivmul2  8905  ledivmul2  8907  lemuldiv2  8909  lt2msq  8913  cju  8988  zextlt  9418  xrlttr  9870  xrre3  9897  ixxdisj  9978  iooshf  10027  icodisj  10067  iccf1o  10079  zssinfcl  10322  seqf1og  10613  expsubap  10679  bcval5  10855  hashfacen  10928  seq3coll  10934  sqrt0rlem  11168  lenegsq  11260  zsumdc  11549  fisum0diag2  11612  prodmodclem2  11742  zproddc  11744  ndvdsadd  12096  lcmdvds  12247  oddpwdclemdc  12341  hashdvds  12389  phisum  12409  pcqmul  12472  pcmpt  12512  4sqlemffi  12565  4sqlem11  12570  ennnfonelemex  12631  grpinvid1  13184  grpinvid2  13185  grplcan  13194  grpnpncan0  13228  dfgrp3mlem  13230  dfgrp3m  13231  grplactcnv  13234  0nsg  13344  eqger  13354  resghm  13390  conjghm  13406  znunit  14215  eltg2  14289  ssnei2  14393  restopnb  14417  txdis1cn  14514  txlm  14515  elbl2ps  14628  elbl2  14629  blininf  14660  xmeter  14672  xmetresbl  14676  bdxmet  14737  metrest  14742  dedekindicc  14869  limcimo  14901  dvmptfsum  14961  plycolemc  14994  dvdsppwf1o  15225  fsumdvdsmul  15227  sgmmul  15232  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem2  15323