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  965  3ad2antr1  1167  xordidc  1421  po2nr  4377  sotricim  4391  fmptco  5774  fvtp1g  5820  dff13  5865  fcof1o  5886  isocnv  5908  isores2  5910  isoini  5915  f1oiso2  5924  acexmidlemab  5968  ovmpodf  6107  offval  6196  xp1st  6281  1stconst  6337  cnvf1olem  6340  f1od2  6351  mpoxopoveq  6356  nnaordi  6624  nnmordi  6632  erinxp  6726  dom2lem  6893  fundmen  6929  pw2f1odclem  6963  mapen  6975  ssenen  6980  fidifsnen  7000  difinfsnlem  7234  fodjum  7281  cc2lem  7420  ltsonq  7553  lt2addnq  7559  lt2mulnq  7560  ltexnqq  7563  prarloclemarch2  7574  enq0sym  7587  genprndl  7676  genprndu  7677  prmuloc  7721  distrlem1prl  7737  distrlem1pru  7738  ltsopr  7751  ltexprlemdisj  7761  ltexprlemfl  7764  ltexprlemfu  7766  addcanprlemu  7770  ltaprg  7774  mulcmpblnrlemg  7895  recexgt0sr  7928  mul4  8246  2addsub  8328  muladd  8498  ltleadd  8561  eqord1  8598  eqord2  8599  divmulap3  8792  divcanap7  8836  divadddivap  8842  lemul2a  8974  lemul12b  8976  ltmuldiv2  8990  ltdivmul  8991  ltdivmul2  8993  ledivmul2  8995  lemuldiv2  8997  lt2msq  9001  cju  9076  zextlt  9507  xrlttr  9959  xrre3  9986  ixxdisj  10067  iooshf  10116  icodisj  10156  iccf1o  10168  zssinfcl  10419  seqf1og  10710  expsubap  10776  bcval5  10952  hashfacen  11025  seq3coll  11031  swrdswrdlem  11202  swrdccatin2  11227  sqrt0rlem  11480  lenegsq  11572  zsumdc  11861  fisum0diag2  11924  prodmodclem2  12054  zproddc  12056  ndvdsadd  12408  lcmdvds  12567  oddpwdclemdc  12661  hashdvds  12709  phisum  12729  pcqmul  12792  pcmpt  12832  4sqlemffi  12885  4sqlem11  12890  ennnfonelemex  12951  grpinvid1  13551  grpinvid2  13552  grplcan  13561  grpnpncan0  13595  dfgrp3mlem  13597  dfgrp3m  13598  grplactcnv  13601  0nsg  13717  eqger  13727  resghm  13763  conjghm  13779  znunit  14588  psrgrp  14614  eltg2  14692  ssnei2  14796  restopnb  14820  txdis1cn  14917  txlm  14918  elbl2ps  15031  elbl2  15032  blininf  15063  xmeter  15075  xmetresbl  15079  bdxmet  15140  metrest  15145  dedekindicc  15272  limcimo  15304  dvmptfsum  15364  plycolemc  15397  dvdsppwf1o  15628  fsumdvdsmul  15630  sgmmul  15635  lgsquadlem1  15721  lgsquadlem2  15722  lgsquad2lem2  15726