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  968  3ad2antr1  1188  xordidc  1443  po2nr  4408  sotricim  4422  fmptco  5816  fvtp1g  5865  dff13  5914  fcof1o  5935  isocnv  5957  isores2  5959  isoini  5964  f1oiso2  5973  acexmidlemab  6017  ovmpodf  6158  offval  6248  xp1st  6333  1stconst  6391  cnvf1olem  6394  f1od2  6405  mpoxopoveq  6411  nnaordi  6681  nnmordi  6689  erinxp  6783  dom2lem  6950  fundmen  6986  pw2f1odclem  7025  mapen  7037  ssenen  7042  fidifsnen  7062  difinfsnlem  7303  fodjum  7350  cc2lem  7490  ltsonq  7623  lt2addnq  7629  lt2mulnq  7630  ltexnqq  7633  prarloclemarch2  7644  enq0sym  7657  genprndl  7746  genprndu  7747  prmuloc  7791  distrlem1prl  7807  distrlem1pru  7808  ltsopr  7821  ltexprlemdisj  7831  ltexprlemfl  7834  ltexprlemfu  7836  addcanprlemu  7840  ltaprg  7844  mulcmpblnrlemg  7965  recexgt0sr  7998  mul4  8316  2addsub  8398  muladd  8568  ltleadd  8631  eqord1  8668  eqord2  8669  divmulap3  8862  divcanap7  8906  divadddivap  8912  lemul2a  9044  lemul12b  9046  ltmuldiv2  9060  ltdivmul  9061  ltdivmul2  9063  ledivmul2  9065  lemuldiv2  9067  lt2msq  9071  cju  9146  zextlt  9577  xrlttr  10035  xrre3  10062  ixxdisj  10143  iooshf  10192  icodisj  10232  iccf1o  10244  zssinfcl  10498  seqf1og  10789  expsubap  10855  bcval5  11031  hashfacen  11106  seq3coll  11112  swrdswrdlem  11294  swrdccatin2  11319  sqrt0rlem  11586  lenegsq  11678  zsumdc  11968  fisum0diag2  12031  prodmodclem2  12161  zproddc  12163  ndvdsadd  12515  lcmdvds  12674  oddpwdclemdc  12768  hashdvds  12816  phisum  12836  pcqmul  12899  pcmpt  12939  4sqlemffi  12992  4sqlem11  12997  ennnfonelemex  13058  grpinvid1  13658  grpinvid2  13659  grplcan  13668  grpnpncan0  13702  dfgrp3mlem  13704  dfgrp3m  13705  grplactcnv  13708  0nsg  13824  eqger  13834  resghm  13870  conjghm  13886  znunit  14697  psrbagconf1o  14716  psrgrp  14728  eltg2  14806  ssnei2  14910  restopnb  14934  txdis1cn  15031  txlm  15032  elbl2ps  15145  elbl2  15146  blininf  15177  xmeter  15189  xmetresbl  15193  bdxmet  15254  metrest  15259  dedekindicc  15386  limcimo  15418  dvmptfsum  15478  plycolemc  15511  dvdsppwf1o  15742  fsumdvdsmul  15744  sgmmul  15749  lgsquadlem1  15835  lgsquadlem2  15836  lgsquad2lem2  15840  upgriswlkdc  16240