Theorem 3adant3r3 1203

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)

Hypothesis

Ref	Expression
ad4ant3.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant3r3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3adant3r3

Step	Hyp	Ref	Expression
1		ad4ant3.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1138	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1190	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  infsupprpr  9491  ressress  17418  plttr  18507  plelttr  18509  latledi  18644  latmlej11  18645  latmlej21  18647  latmlej22  18648  latjass  18650  latj12  18651  latj31  18654  latdisdlem  18663  ipopos  18703  imasmnd2  18961  imasmnd  18962  grpaddsubass  19233  grpsubsub4  19236  grpnpncan  19238  imasgrp2  19258  imasgrp  19259  frgp0  19967  cmn12  20009  abladdsub  20019  imasrng  20392  imasring  20553  dvrass  20631  isdomn4  20960  lss1  21206  islmhm2  21306  unichnlidl  21509  rspprop  21517  zntoslem  21855  ipdir  21938  psrlmod  22260  t1sep  23681  mettri2  24653  xmetrtri  24667  xmetrtri2  24668  pi1grplem  25363  dchrabl  27574  motgrp  28999  xmstrkgc  29456  ax5seglem4  29503  grpomuldivass  31136  ablomuldiv  31147  ablodivdiv4  31149  nvmdi  31243  dipdi  31438  dipsubdir  31443  dipsubdi  31444  cgr3tr4  36797  cgr3rflx  36799  seglemin  36858  linerflx1  36894  elicc3  37085  rngosubdi  38859  rngosubdir  38860  igenval2  38980  dmncan1  38990  latmassOLD  40266  omlfh1N  40295  omlfh3N  40296  cvrnbtwn  40308  cvrnbtwn2  40312  cvrnbtwn4  40316  hlatj12  40408  cvrntr  40462  islpln2a  40585  3atnelvolN  40623  elpadd2at2  40844  paddasslem17  40873  paddass  40875  paddssw2  40881  pmapjlln1  40892  ltrn2ateq  41217  cdlemc3  41230  cdleme1b  41263  cdleme3b  41266  cdleme3c  41267  cdleme9b  41289  erngdvlem3  42027  erngdvlem3-rN  42035  dvalveclem  42062  mendlmod  44175  lincsumscmcl  49514