Theorem 3adant3r3 1185

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 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1172	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  infsupprpr  9464  ressress  17224  plttr  18308  plelttr  18310  latledi  18443  latmlej11  18444  latmlej21  18446  latmlej22  18447  latjass  18449  latj12  18450  latj31  18453  latdisdlem  18462  ipopos  18502  imasmnd2  18708  imasmnd  18709  grpaddsubass  18969  grpsubsub4  18972  grpnpncan  18974  imasgrp2  18994  imasgrp  18995  frgp0  19697  cmn12  19739  abladdsub  19749  imasrng  20093  imasring  20246  dvrass  20324  isdomn4  20632  lss1  20851  islmhm2  20952  zntoslem  21473  ipdir  21555  psrgrpOLD  21873  psrlmod  21876  t1sep  23264  mettri2  24236  xmetrtri  24250  xmetrtri2  24251  pi1grplem  24956  dchrabl  27172  motgrp  28477  xmstrkgc  28820  ax5seglem4  28866  grpomuldivass  30477  ablomuldiv  30488  ablodivdiv4  30490  nvmdi  30584  dipdi  30779  dipsubdir  30784  dipsubdi  30785  cgr3tr4  36047  cgr3rflx  36049  seglemin  36108  linerflx1  36144  elicc3  36312  rngosubdi  37946  rngosubdir  37947  igenval2  38067  dmncan1  38077  latmassOLD  39229  omlfh1N  39258  omlfh3N  39259  cvrnbtwn  39271  cvrnbtwn2  39275  cvrnbtwn4  39279  hlatj12  39371  cvrntr  39426  islpln2a  39549  3atnelvolN  39587  elpadd2at2  39808  paddasslem17  39837  paddass  39839  paddssw2  39845  pmapjlln1  39856  ltrn2ateq  40181  cdlemc3  40194  cdleme1b  40227  cdleme3b  40230  cdleme3c  40231  cdleme9b  40253  erngdvlem3  40991  erngdvlem3-rN  40999  dvalveclem  41026  mendlmod  43185  lincsumscmcl  48426