Theorem 3adant3r3 1184

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 1171	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  9573  ressress  17307  plttr  18412  plelttr  18414  latledi  18547  latmlej11  18548  latmlej21  18550  latmlej22  18551  latjass  18553  latj12  18554  latj31  18557  latdisdlem  18566  ipopos  18606  imasmnd2  18809  imasmnd  18810  grpaddsubass  19070  grpsubsub4  19073  grpnpncan  19075  imasgrp2  19095  imasgrp  19096  frgp0  19802  cmn12  19844  abladdsub  19854  imasrng  20204  imasring  20353  dvrass  20434  isdomn4  20738  lss1  20959  islmhm2  21060  zntoslem  21598  ipdir  21680  psrgrpOLD  22000  psrlmod  22003  t1sep  23399  mettri2  24372  xmetrtri  24386  xmetrtri2  24387  pi1grplem  25101  dchrabl  27316  motgrp  28569  xmstrkgc  28918  ax5seglem4  28965  grpomuldivass  30573  ablomuldiv  30584  ablodivdiv4  30586  nvmdi  30680  dipdi  30875  dipsubdir  30880  dipsubdi  30881  cgr3tr4  36016  cgr3rflx  36018  seglemin  36077  linerflx1  36113  elicc3  36283  rngosubdi  37905  rngosubdir  37906  igenval2  38026  dmncan1  38036  latmassOLD  39185  omlfh1N  39214  omlfh3N  39215  cvrnbtwn  39227  cvrnbtwn2  39231  cvrnbtwn4  39235  hlatj12  39327  cvrntr  39382  islpln2a  39505  3atnelvolN  39543  elpadd2at2  39764  paddasslem17  39793  paddass  39795  paddssw2  39801  pmapjlln1  39812  ltrn2ateq  40137  cdlemc3  40150  cdleme1b  40183  cdleme3b  40186  cdleme3c  40187  cdleme9b  40209  erngdvlem3  40947  erngdvlem3-rN  40955  dvalveclem  40982  mendlmod  43150  lincsumscmcl  48162