Theorem 3adant3r3 1201

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  infsupprpr  9462  ressress  17303  plttr  18392  plelttr  18394  latledi  18529  latmlej11  18530  latmlej21  18532  latmlej22  18533  latjass  18535  latj12  18536  latj31  18539  latdisdlem  18548  ipopos  18588  imasmnd2  18828  imasmnd  18829  grpaddsubass  19092  grpsubsub4  19095  grpnpncan  19097  imasgrp2  19117  imasgrp  19118  frgp0  19826  cmn12  19868  abladdsub  19878  imasrng  20251  imasring  20408  dvrass  20486  isdomn4  20796  lss1  21033  islmhm2  21133  unichnlidl  21336  zntoslem  21671  ipdir  21754  psrlmod  22074  t1sep  23492  mettri2  24463  xmetrtri  24477  xmetrtri2  24478  pi1grplem  25173  dchrabl  27380  motgrp  28774  xmstrkgc  29172  ax5seglem4  29219  grpomuldivass  30830  ablomuldiv  30841  ablodivdiv4  30843  nvmdi  30937  dipdi  31132  dipsubdir  31137  dipsubdi  31138  cgr3tr4  36439  cgr3rflx  36441  seglemin  36500  linerflx1  36536  elicc3  36713  rngosubdi  38479  rngosubdir  38480  igenval2  38600  dmncan1  38610  latmassOLD  39888  omlfh1N  39917  omlfh3N  39918  cvrnbtwn  39930  cvrnbtwn2  39934  cvrnbtwn4  39938  hlatj12  40030  cvrntr  40084  islpln2a  40207  3atnelvolN  40245  elpadd2at2  40466  paddasslem17  40495  paddass  40497  paddssw2  40503  pmapjlln1  40514  ltrn2ateq  40839  cdlemc3  40852  cdleme1b  40885  cdleme3b  40888  cdleme3c  40889  cdleme9b  40911  erngdvlem3  41649  erngdvlem3-rN  41657  dvalveclem  41684  mendlmod  43801  lincsumscmcl  49091