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  4432  sotricim  4446  fmptco  5845  fvtp1g  5894  dff13  5943  fcof1o  5964  isocnv  5986  isores2  5988  isoini  5993  f1oiso2  6002  acexmidlemab  6046  ovmpodf  6187  offval  6276  xp1st  6361  1stconst  6419  cnvf1olem  6422  f1od2  6433  mpoxopoveq  6473  nnaordi  6743  nnmordi  6751  erinxp  6845  dom2lem  7013  fundmen  7049  pw2f1odclem  7089  mapen  7101  ssenen  7107  fidifsnen  7127  difinfsnlem  7392  fodjum  7439  cc2lem  7585  ltsonq  7718  lt2addnq  7724  lt2mulnq  7725  ltexnqq  7728  prarloclemarch2  7739  enq0sym  7752  genprndl  7841  genprndu  7842  prmuloc  7886  distrlem1prl  7902  distrlem1pru  7903  ltsopr  7916  ltexprlemdisj  7926  ltexprlemfl  7929  ltexprlemfu  7931  addcanprlemu  7935  ltaprg  7939  mulcmpblnrlemg  8060  recexgt0sr  8093  mul4  8410  2addsub  8492  muladd  8662  ltleadd  8725  eqord1  8762  eqord2  8763  divmulap3  8956  divcanap7  9000  divadddivap  9006  lemul2a  9138  lemul12b  9140  ltmuldiv2  9154  ltdivmul  9155  ltdivmul2  9157  ledivmul2  9159  lemuldiv2  9161  lt2msq  9165  cju  9240  zextlt  9676  xrlttr  10134  xrre3  10161  ixxdisj  10242  iooshf  10291  icodisj  10331  iccf1o  10344  zssinfcl  10599  seqf1og  10890  expsubap  10956  bcval5  11133  hashmap  11200  hashfacen  11216  seq3coll  11222  swrdswrdlem  11404  swrdccatin2  11429  sqrt0rlem  11696  lenegsq  11788  zsumdc  12078  fisum0diag2  12141  prodmodclem2  12271  zproddc  12273  ndvdsadd  12625  lcmdvds  12784  oddpwdclemdc  12878  hashdvds  12926  phisum  12946  pcqmul  13009  pcmpt  13049  4sqlemffi  13102  4sqlem11  13107  ballotfilemfc0  13157  ballotfilemfcc  13158  ennnfonelemex  13186  grpinvid1  13786  grpinvid2  13787  grplcan  13796  grpnpncan0  13830  dfgrp3mlem  13832  dfgrp3m  13833  grplactcnv  13836  0nsg  13952  eqger  13962  resghm  13998  conjghm  14014  znunit  14856  psrbagconf1o  14877  psrgrp  14889  eltg2  14967  ssnei2  15071  restopnb  15095  txdis1cn  15192  txlm  15193  elbl2ps  15306  elbl2  15307  blininf  15338  xmeter  15350  xmetresbl  15354  bdxmet  15415  metrest  15420  dedekindicc  15547  limcimo  15579  dvmptfsum  15639  plycolemc  15672  dvdsppwf1o  15906  fsumdvdsmul  15908  sgmmul  15913  lgsquadlem1  15999  lgsquadlem2  16000  lgsquad2lem2  16004  upgriswlkdc  16404