Theorem adantrrr 724

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis

Ref	Expression
adantr2.1

Assertion

Ref	Expression
adantrrr

Proof of Theorem adantrrr

Step	Hyp	Ref	Expression
1		simpl 457	. 2
2		adantr2.1	. 2
3	1, 2	sylanr2 653	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  2ndconst  6889  zorn2lem6  8902  addsrmo  9471  mulsrmo  9472  lemul12b  10424  lt2mul2div  10446  lediv12a  10463  tgcl  19471  neissex  19628  alexsublem  20544  alexsubALTlem4  20550  iscmet3  21732  ablo4  25289  shscli  26235  mdslmd3i  27251  cvmliftmolem2  28727  mblfinlem4  30054  heibor  30317  ablo4pnp  30342  crngm4  30400  mzpcompact2lem  30684  cvratlem  35145  ps-2  35202  cdlemftr3  36291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371