Theorem adantrr 463

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 107	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 280	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  ad2ant2r  493  ad2ant2lr  494  dn1dc  904  3ad2antr1  1106  xordidc  1333  po2nr  4110  sotricim  4124  fmptco  5427  fvtp1g  5466  dff13  5508  fcof1o  5529  isocnv  5551  isores2  5553  isoini  5558  f1oiso2  5567  acexmidlemab  5607  ovmpt2df  5733  offval  5820  xp1st  5893  1stconst  5943  cnvf1olem  5946  f1od2  5957  mpt2xopoveq  5959  nnaordi  6219  nnmordi  6227  erinxp  6318  dom2lem  6441  fundmen  6475  mapen  6514  ssenen  6519  fidifsnen  6538  fodjuomnilemm  6745  ltsonq  6901  lt2addnq  6907  lt2mulnq  6908  ltexnqq  6911  prarloclemarch2  6922  enq0sym  6935  genprndl  7024  genprndu  7025  prmuloc  7069  distrlem1prl  7085  distrlem1pru  7086  ltsopr  7099  ltexprlemdisj  7109  ltexprlemfl  7112  ltexprlemfu  7114  addcanprlemu  7118  ltaprg  7122  mulcmpblnrlemg  7230  recexgt0sr  7263  mul4  7558  2addsub  7640  muladd  7806  ltleadd  7868  divmulap3  8083  divcanap7  8127  divadddivap  8133  lemul2a  8255  lemul12b  8257  ltmuldiv2  8271  ltdivmul  8272  ltdivmul2  8274  ledivmul2  8276  lemuldiv2  8278  lt2msq  8282  cju  8356  zextlt  8771  xrlttr  9197  xrre3  9216  ixxdisj  9253  iooshf  9302  icodisj  9341  iccf1o  9353  expsubap  9902  ibcval5  10068  hashfacen  10138  iseqcoll  10144  sqrt0rlem  10332  lenegsq  10424  zisum  10665  ndvdsadd  10813  zssinfcl  10826  lcmdvds  10943  oddpwdclemdc  11033  hashdvds  11079