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

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

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 1089

This theorem is referenced by:  infsupprpr  9419  ressress  17217  plttr  18306  plelttr  18308  latledi  18443  latmlej11  18444  latmlej21  18446  latmlej22  18447  latjass  18449  latj12  18450  latj31  18453  latdisdlem  18462  ipopos  18502  imasmnd2  18742  imasmnd  18743  grpaddsubass  19006  grpsubsub4  19009  grpnpncan  19011  imasgrp2  19031  imasgrp  19032  frgp0  19735  cmn12  19777  abladdsub  19787  imasrng  20158  imasring  20310  dvrass  20388  isdomn4  20693  lss1  20933  islmhm2  21033  zntoslem  21536  ipdir  21619  psrlmod  21938  t1sep  23335  mettri2  24306  xmetrtri  24320  xmetrtri2  24321  pi1grplem  25016  dchrabl  27217  motgrp  28611  xmstrkgc  28954  ax5seglem4  29001  grpomuldivass  30612  ablomuldiv  30623  ablodivdiv4  30625  nvmdi  30719  dipdi  30914  dipsubdir  30919  dipsubdi  30920  cgr3tr4  36234  cgr3rflx  36236  seglemin  36295  linerflx1  36331  elicc3  36499  rngosubdi  38266  rngosubdir  38267  igenval2  38387  dmncan1  38397  latmassOLD  39675  omlfh1N  39704  omlfh3N  39705  cvrnbtwn  39717  cvrnbtwn2  39721  cvrnbtwn4  39725  hlatj12  39817  cvrntr  39871  islpln2a  39994  3atnelvolN  40032  elpadd2at2  40253  paddasslem17  40282  paddass  40284  paddssw2  40290  pmapjlln1  40301  ltrn2ateq  40626  cdlemc3  40639  cdleme1b  40672  cdleme3b  40675  cdleme3c  40676  cdleme9b  40698  erngdvlem3  41436  erngdvlem3-rN  41444  dvalveclem  41471  mendlmod  43617  lincsumscmcl  48909