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

Assertion

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

Proof of Theorem adantrr

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

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  4345  sotricim  4359  fmptco  5731  fvtp1g  5773  dff13  5818  fcof1o  5839  isocnv  5861  isores2  5863  isoini  5868  f1oiso2  5877  acexmidlemab  5919  ovmpodf  6058  offval  6147  xp1st  6232  1stconst  6288  cnvf1olem  6291  f1od2  6302  mpoxopoveq  6307  nnaordi  6575  nnmordi  6583  erinxp  6677  dom2lem  6840  fundmen  6874  pw2f1odclem  6904  mapen  6916  ssenen  6921  fidifsnen  6940  difinfsnlem  7174  fodjum  7221  cc2lem  7349  ltsonq  7482  lt2addnq  7488  lt2mulnq  7489  ltexnqq  7492  prarloclemarch2  7503  enq0sym  7516  genprndl  7605  genprndu  7606  prmuloc  7650  distrlem1prl  7666  distrlem1pru  7667  ltsopr  7680  ltexprlemdisj  7690  ltexprlemfl  7693  ltexprlemfu  7695  addcanprlemu  7699  ltaprg  7703  mulcmpblnrlemg  7824  recexgt0sr  7857  mul4  8175  2addsub  8257  muladd  8427  ltleadd  8490  eqord1  8527  eqord2  8528  divmulap3  8721  divcanap7  8765  divadddivap  8771  lemul2a  8903  lemul12b  8905  ltmuldiv2  8919  ltdivmul  8920  ltdivmul2  8922  ledivmul2  8924  lemuldiv2  8926  lt2msq  8930  cju  9005  zextlt  9435  xrlttr  9887  xrre3  9914  ixxdisj  9995  iooshf  10044  icodisj  10084  iccf1o  10096  zssinfcl  10339  seqf1og  10630  expsubap  10696  bcval5  10872  hashfacen  10945  seq3coll  10951  sqrt0rlem  11185  lenegsq  11277  zsumdc  11566  fisum0diag2  11629  prodmodclem2  11759  zproddc  11761  ndvdsadd  12113  lcmdvds  12272  oddpwdclemdc  12366  hashdvds  12414  phisum  12434  pcqmul  12497  pcmpt  12537  4sqlemffi  12590  4sqlem11  12595  ennnfonelemex  12656  grpinvid1  13254  grpinvid2  13255  grplcan  13264  grpnpncan0  13298  dfgrp3mlem  13300  dfgrp3m  13301  grplactcnv  13304  0nsg  13420  eqger  13430  resghm  13466  conjghm  13482  znunit  14291  psrgrp  14313  eltg2  14373  ssnei2  14477  restopnb  14501  txdis1cn  14598  txlm  14599  elbl2ps  14712  elbl2  14713  blininf  14744  xmeter  14756  xmetresbl  14760  bdxmet  14821  metrest  14826  dedekindicc  14953  limcimo  14985  dvmptfsum  15045  plycolemc  15078  dvdsppwf1o  15309  fsumdvdsmul  15311  sgmmul  15316  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem2  15407