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  966  3ad2antr1  1186  xordidc  1441  po2nr  4404  sotricim  4418  fmptco  5809  fvtp1g  5857  dff13  5904  fcof1o  5925  isocnv  5947  isores2  5949  isoini  5954  f1oiso2  5963  acexmidlemab  6007  ovmpodf  6148  offval  6238  xp1st  6323  1stconst  6381  cnvf1olem  6384  f1od2  6395  mpoxopoveq  6401  nnaordi  6671  nnmordi  6679  erinxp  6773  dom2lem  6940  fundmen  6976  pw2f1odclem  7015  mapen  7027  ssenen  7032  fidifsnen  7052  difinfsnlem  7292  fodjum  7339  cc2lem  7478  ltsonq  7611  lt2addnq  7617  lt2mulnq  7618  ltexnqq  7621  prarloclemarch2  7632  enq0sym  7645  genprndl  7734  genprndu  7735  prmuloc  7779  distrlem1prl  7795  distrlem1pru  7796  ltsopr  7809  ltexprlemdisj  7819  ltexprlemfl  7822  ltexprlemfu  7824  addcanprlemu  7828  ltaprg  7832  mulcmpblnrlemg  7953  recexgt0sr  7986  mul4  8304  2addsub  8386  muladd  8556  ltleadd  8619  eqord1  8656  eqord2  8657  divmulap3  8850  divcanap7  8894  divadddivap  8900  lemul2a  9032  lemul12b  9034  ltmuldiv2  9048  ltdivmul  9049  ltdivmul2  9051  ledivmul2  9053  lemuldiv2  9055  lt2msq  9059  cju  9134  zextlt  9565  xrlttr  10023  xrre3  10050  ixxdisj  10131  iooshf  10180  icodisj  10220  iccf1o  10232  zssinfcl  10485  seqf1og  10776  expsubap  10842  bcval5  11018  hashfacen  11093  seq3coll  11099  swrdswrdlem  11278  swrdccatin2  11303  sqrt0rlem  11557  lenegsq  11649  zsumdc  11938  fisum0diag2  12001  prodmodclem2  12131  zproddc  12133  ndvdsadd  12485  lcmdvds  12644  oddpwdclemdc  12738  hashdvds  12786  phisum  12806  pcqmul  12869  pcmpt  12909  4sqlemffi  12962  4sqlem11  12967  ennnfonelemex  13028  grpinvid1  13628  grpinvid2  13629  grplcan  13638  grpnpncan0  13672  dfgrp3mlem  13674  dfgrp3m  13675  grplactcnv  13678  0nsg  13794  eqger  13804  resghm  13840  conjghm  13856  znunit  14666  psrgrp  14692  eltg2  14770  ssnei2  14874  restopnb  14898  txdis1cn  14995  txlm  14996  elbl2ps  15109  elbl2  15110  blininf  15141  xmeter  15153  xmetresbl  15157  bdxmet  15218  metrest  15223  dedekindicc  15350  limcimo  15382  dvmptfsum  15442  plycolemc  15475  dvdsppwf1o  15706  fsumdvdsmul  15708  sgmmul  15713  lgsquadlem1  15799  lgsquadlem2  15800  lgsquad2lem2  15804  upgriswlkdc  16171