Theorem adantrr 470

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ad2ant2r  500  ad2ant2lr  501  dn1dc  944  3ad2antr1  1146  xordidc  1377  po2nr  4231  sotricim  4245  fmptco  5586  fvtp1g  5628  dff13  5669  fcof1o  5690  isocnv  5712  isores2  5714  isoini  5719  f1oiso2  5728  acexmidlemab  5768  ovmpodf  5902  offval  5989  xp1st  6063  1stconst  6118  cnvf1olem  6121  f1od2  6132  mpoxopoveq  6137  nnaordi  6404  nnmordi  6412  erinxp  6503  dom2lem  6666  fundmen  6700  mapen  6740  ssenen  6745  fidifsnen  6764  difinfsnlem  6984  fodjum  7018  ltsonq  7206  lt2addnq  7212  lt2mulnq  7213  ltexnqq  7216  prarloclemarch2  7227  enq0sym  7240  genprndl  7329  genprndu  7330  prmuloc  7374  distrlem1prl  7390  distrlem1pru  7391  ltsopr  7404  ltexprlemdisj  7414  ltexprlemfl  7417  ltexprlemfu  7419  addcanprlemu  7423  ltaprg  7427  mulcmpblnrlemg  7548  recexgt0sr  7581  mul4  7894  2addsub  7976  muladd  8146  ltleadd  8208  eqord1  8245  eqord2  8246  divmulap3  8437  divcanap7  8481  divadddivap  8487  lemul2a  8617  lemul12b  8619  ltmuldiv2  8633  ltdivmul  8634  ltdivmul2  8636  ledivmul2  8638  lemuldiv2  8640  lt2msq  8644  cju  8719  zextlt  9143  xrlttr  9581  xrre3  9605  ixxdisj  9686  iooshf  9735  icodisj  9775  iccf1o  9787  expsubap  10341  bcval5  10509  hashfacen  10579  seq3coll  10585  sqrt0rlem  10775  lenegsq  10867  zsumdc  11153  fisum0diag2  11216  prodmodclem2  11346  ndvdsadd  11628  zssinfcl  11641  lcmdvds  11760  oddpwdclemdc  11851  hashdvds  11897  ennnfonelemex  11927  eltg2  12222  ssnei2  12326  restopnb  12350  txdis1cn  12447  txlm  12448  elbl2ps  12561  elbl2  12562  blininf  12593  xmeter  12605  xmetresbl  12609  bdxmet  12670  metrest  12675  dedekindicc  12780  limcimo  12803