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  4400  sotricim  4414  fmptco  5803  fvtp1g  5851  dff13  5898  fcof1o  5919  isocnv  5941  isores2  5943  isoini  5948  f1oiso2  5957  acexmidlemab  6001  ovmpodf  6142  offval  6232  xp1st  6317  1stconst  6373  cnvf1olem  6376  f1od2  6387  mpoxopoveq  6392  nnaordi  6662  nnmordi  6670  erinxp  6764  dom2lem  6931  fundmen  6967  pw2f1odclem  7003  mapen  7015  ssenen  7020  fidifsnen  7040  difinfsnlem  7274  fodjum  7321  cc2lem  7460  ltsonq  7593  lt2addnq  7599  lt2mulnq  7600  ltexnqq  7603  prarloclemarch2  7614  enq0sym  7627  genprndl  7716  genprndu  7717  prmuloc  7761  distrlem1prl  7777  distrlem1pru  7778  ltsopr  7791  ltexprlemdisj  7801  ltexprlemfl  7804  ltexprlemfu  7806  addcanprlemu  7810  ltaprg  7814  mulcmpblnrlemg  7935  recexgt0sr  7968  mul4  8286  2addsub  8368  muladd  8538  ltleadd  8601  eqord1  8638  eqord2  8639  divmulap3  8832  divcanap7  8876  divadddivap  8882  lemul2a  9014  lemul12b  9016  ltmuldiv2  9030  ltdivmul  9031  ltdivmul2  9033  ledivmul2  9035  lemuldiv2  9037  lt2msq  9041  cju  9116  zextlt  9547  xrlttr  9999  xrre3  10026  ixxdisj  10107  iooshf  10156  icodisj  10196  iccf1o  10208  zssinfcl  10460  seqf1og  10751  expsubap  10817  bcval5  10993  hashfacen  11066  seq3coll  11072  swrdswrdlem  11244  swrdccatin2  11269  sqrt0rlem  11522  lenegsq  11614  zsumdc  11903  fisum0diag2  11966  prodmodclem2  12096  zproddc  12098  ndvdsadd  12450  lcmdvds  12609  oddpwdclemdc  12703  hashdvds  12751  phisum  12771  pcqmul  12834  pcmpt  12874  4sqlemffi  12927  4sqlem11  12932  ennnfonelemex  12993  grpinvid1  13593  grpinvid2  13594  grplcan  13603  grpnpncan0  13637  dfgrp3mlem  13639  dfgrp3m  13640  grplactcnv  13643  0nsg  13759  eqger  13769  resghm  13805  conjghm  13821  znunit  14631  psrgrp  14657  eltg2  14735  ssnei2  14839  restopnb  14863  txdis1cn  14960  txlm  14961  elbl2ps  15074  elbl2  15075  blininf  15106  xmeter  15118  xmetresbl  15122  bdxmet  15183  metrest  15188  dedekindicc  15315  limcimo  15347  dvmptfsum  15407  plycolemc  15440  dvdsppwf1o  15671  fsumdvdsmul  15673  sgmmul  15678  lgsquadlem1  15764  lgsquadlem2  15765  lgsquad2lem2  15769  upgriswlkdc  16081