Theorem adantrr 483

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  513  ad2ant2lr  514  dn1dc  973  3ad2antr1  1193  xordidc  1448  po2nr  4452  sotricim  4466  fmptco  5868  fvtp1g  5917  dff13  5968  fcof1o  5989  isocnv  6011  isores2  6013  isoini  6018  f1oiso2  6027  acexmidlemab  6073  ovmpodf  6214  offval  6304  xp1st  6393  1stconst  6451  cnvf1olem  6454  f1od2  6465  mpoxopoveq  6505  nnaordi  6775  nnmordi  6783  erinxp  6877  dom2lem  7052  fundmen  7088  pw2f1odclem  7128  mapen  7140  ssenen  7146  fidifsnen  7166  difinfsnlem  7433  fodjum  7480  cc2lem  7626  ltsonq  7759  lt2addnq  7765  lt2mulnq  7766  ltexnqq  7769  prarloclemarch2  7780  enq0sym  7793  genprndl  7882  genprndu  7883  prmuloc  7927  distrlem1prl  7943  distrlem1pru  7944  ltsopr  7957  ltexprlemdisj  7967  ltexprlemfl  7970  ltexprlemfu  7972  addcanprlemu  7976  ltaprg  7980  mulcmpblnrlemg  8101  recexgt0sr  8134  mul4  8452  2addsub  8534  muladd  8705  ltleadd  8768  eqord1  8805  eqord2  8806  divmulap3  9001  divcanap7  9045  divadddivap  9051  lemul2a  9183  lemul12b  9185  ltmuldiv2  9199  ltdivmul  9200  ltdivmul2  9202  ledivmul2  9204  lemuldiv2  9206  lt2msq  9210  cju  9285  zextlt  9721  xrlttr  10180  xrre3  10207  ixxdisj  10288  iooshf  10337  icodisj  10377  iccf1o  10390  zssinfcl  10648  seqf1og  10941  expsubap  11007  bcval5  11184  hashmap  11251  hashfacen  11267  seq3coll  11277  swrdswrdlem  11459  swrdccatin2  11484  sqrt0rlem  11752  lenegsq  11844  zsumdc  12134  fisum0diag2  12197  prodmodclem2  12327  zproddc  12329  ndvdsadd  12681  lcmdvds  12840  oddpwdclemdc  12934  hashdvds  12982  phisum  13002  pcqmul  13065  pcmpt  13105  4sqlemffi  13158  4sqlem11  13163  ballotfilemfc0  13215  ballotfilemfcc  13216  ennnfonelemex  13288  grpinvid1  13840  grpinvid2  13841  grplcan  13850  grpnpncan0  13884  dfgrp3mlem  13886  dfgrp3m  13887  grplactcnv  13890  0nsg  14000  eqger  14010  resghm  14046  conjghm  14062  znunit  14977  issubassa3  14995  issubassa2  15018  psrbagconf1o  15047  psrgrp  15059  eltg2  15137  ssnei2  15241  restopnb  15265  txdis1cn  15362  txlm  15363  elbl2ps  15476  elbl2  15477  blininf  15508  xmeter  15520  xmetresbl  15524  bdxmet  15585  metrest  15590  dedekindicc  15717  limcimo  15749  dvmptfsum  15809  plycolemc  15842  dvdsppwf1o  16086  fsumdvdsmul  16088  sgmmul  16093  lgsquadlem1  16179  lgsquadlem2  16180  lgsquad2lem2  16184  upgriswlkdc  16584