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  969  3ad2antr1  1189  xordidc  1444  po2nr  4435  sotricim  4449  fmptco  5848  fvtp1g  5897  dff13  5947  fcof1o  5968  isocnv  5990  isores2  5992  isoini  5997  f1oiso2  6006  acexmidlemab  6052  ovmpodf  6193  offval  6283  xp1st  6372  1stconst  6430  cnvf1olem  6433  f1od2  6444  mpoxopoveq  6484  nnaordi  6754  nnmordi  6762  erinxp  6856  dom2lem  7024  fundmen  7060  pw2f1odclem  7100  mapen  7112  ssenen  7118  fidifsnen  7138  difinfsnlem  7403  fodjum  7450  cc2lem  7596  ltsonq  7729  lt2addnq  7735  lt2mulnq  7736  ltexnqq  7739  prarloclemarch2  7750  enq0sym  7763  genprndl  7852  genprndu  7853  prmuloc  7897  distrlem1prl  7913  distrlem1pru  7914  ltsopr  7927  ltexprlemdisj  7937  ltexprlemfl  7940  ltexprlemfu  7942  addcanprlemu  7946  ltaprg  7950  mulcmpblnrlemg  8071  recexgt0sr  8104  mul4  8422  2addsub  8504  muladd  8675  ltleadd  8738  eqord1  8775  eqord2  8776  divmulap3  8971  divcanap7  9015  divadddivap  9021  lemul2a  9153  lemul12b  9155  ltmuldiv2  9169  ltdivmul  9170  ltdivmul2  9172  ledivmul2  9174  lemuldiv2  9176  lt2msq  9180  cju  9255  zextlt  9691  xrlttr  10150  xrre3  10177  ixxdisj  10258  iooshf  10307  icodisj  10347  iccf1o  10360  zssinfcl  10617  seqf1og  10910  expsubap  10976  bcval5  11153  hashmap  11220  hashfacen  11236  seq3coll  11242  swrdswrdlem  11424  swrdccatin2  11449  sqrt0rlem  11716  lenegsq  11808  zsumdc  12098  fisum0diag2  12161  prodmodclem2  12291  zproddc  12293  ndvdsadd  12645  lcmdvds  12804  oddpwdclemdc  12898  hashdvds  12946  phisum  12966  pcqmul  13029  pcmpt  13069  4sqlemffi  13122  4sqlem11  13127  ballotfilemfc0  13179  ballotfilemfcc  13180  ennnfonelemex  13252  grpinvid1  13810  grpinvid2  13811  grplcan  13820  grpnpncan0  13854  dfgrp3mlem  13856  dfgrp3m  13857  grplactcnv  13860  0nsg  13970  eqger  13980  resghm  14016  conjghm  14032  znunit  14936  psrbagconf1o  14957  psrgrp  14969  eltg2  15047  ssnei2  15151  restopnb  15175  txdis1cn  15272  txlm  15273  elbl2ps  15386  elbl2  15387  blininf  15418  xmeter  15430  xmetresbl  15434  bdxmet  15495  metrest  15500  dedekindicc  15627  limcimo  15659  dvmptfsum  15719  plycolemc  15752  dvdsppwf1o  15986  fsumdvdsmul  15988  sgmmul  15993  lgsquadlem1  16079  lgsquadlem2  16080  lgsquad2lem2  16084  upgriswlkdc  16484