Theorem adantrr 448

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	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantrr	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		simpl 102	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 270	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  ad2ant2r  478  ad2ant2lr  479  dn1dc  867  3ad2antr1  1069  xordidc  1290  po2nr  4046  sotricim  4060  fmptco  5330  fvtp1g  5369  dff13  5407  fcof1o  5429  isocnv  5451  isores2  5453  isoini  5457  f1oiso2  5466  acexmidlemab  5506  ovmpt2df  5632  offval  5719  xp1st  5792  1stconst  5842  cnvf1olem  5845  mpt2xopoveq  5855  nnaordi  6081  nnmordi  6089  erinxp  6180  dom2lem  6252  fundmen  6286  fidifsnen  6331  ltsonq  6496  lt2addnq  6502  lt2mulnq  6503  ltexnqq  6506  prarloclemarch2  6517  enq0sym  6530  genprndl  6619  genprndu  6620  prmuloc  6664  distrlem1prl  6680  distrlem1pru  6681  ltsopr  6694  ltexprlemdisj  6704  ltexprlemfl  6707  ltexprlemfu  6709  addcanprlemu  6713  ltaprg  6717  mulcmpblnrlemg  6825  recexgt0sr  6858  mul4  7145  2addsub  7225  muladd  7381  ltleadd  7441  divmulap3  7656  divcanap7  7697  divadddivap  7703  lemul2a  7825  lemul12b  7827  ltmuldiv2  7841  ltdivmul  7842  ltdivmul2  7844  ledivmul2  7846  lemuldiv2  7848  lt2msq  7852  cju  7913  zextlt  8332  xrlttr  8716  xrre3  8735  ixxdisj  8772  iooshf  8821  icodisj  8860  iccf1o  8872  expsubap  9302  sqrt0rlem  9601  lenegsq  9691