Theorem 3adant3r3 1186

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  infsupprpr  9098  ressress  16746  plttr  17802  plelttr  17804  latledi  17937  latmlej11  17938  latmlej21  17940  latmlej22  17941  latjass  17943  latj12  17944  latj31  17947  latdisdlem  17956  ipopos  17996  imasmnd2  18164  imasmnd  18165  grpaddsubass  18407  grpsubsub4  18410  grpnpncan  18412  imasgrp2  18432  imasgrp  18433  frgp0  19104  cmn12  19145  abladdsub  19154  imasring  19591  dvrass  19662  lss1  19929  islmhm2  20029  zntoslem  20475  ipdir  20555  psrgrp  20877  psrlmod  20880  t1sep  22221  mettri2  23193  xmetrtri  23207  xmetrtri2  23208  pi1grplem  23900  dchrabl  26089  motgrp  26588  xmstrkgc  26931  ax5seglem4  26977  grpomuldivass  28576  ablomuldiv  28587  ablodivdiv4  28589  nvmdi  28683  dipdi  28878  dipsubdir  28883  dipsubdi  28884  cgr3tr4  34040  cgr3rflx  34042  seglemin  34101  linerflx1  34137  elicc3  34192  rngosubdi  35789  rngosubdir  35790  igenval2  35910  dmncan1  35920  latmassOLD  36929  omlfh1N  36958  omlfh3N  36959  cvrnbtwn  36971  cvrnbtwn2  36975  cvrnbtwn4  36979  hlatj12  37071  cvrntr  37125  islpln2a  37248  3atnelvolN  37286  elpadd2at2  37507  paddasslem17  37536  paddass  37538  paddssw2  37544  pmapjlln1  37555  ltrn2ateq  37880  cdlemc3  37893  cdleme1b  37926  cdleme3b  37929  cdleme3c  37930  cdleme9b  37952  erngdvlem3  38690  erngdvlem3-rN  38698  dvalveclem  38725  isdomn4  39835  mendlmod  40662  lincsumscmcl  45390