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  9421  ressress  17186  plttr  18275  plelttr  18277  latledi  18412  latmlej11  18413  latmlej21  18415  latmlej22  18416  latjass  18418  latj12  18419  latj31  18422  latdisdlem  18431  ipopos  18471  imasmnd2  18711  imasmnd  18712  grpaddsubass  18972  grpsubsub4  18975  grpnpncan  18977  imasgrp2  18997  imasgrp  18998  frgp0  19701  cmn12  19743  abladdsub  19753  imasrng  20124  imasring  20278  dvrass  20356  isdomn4  20661  lss1  20901  islmhm2  21002  zntoslem  21523  ipdir  21606  psrlmod  21927  t1sep  23326  mettri2  24297  xmetrtri  24311  xmetrtri2  24312  pi1grplem  25017  dchrabl  27233  motgrp  28627  xmstrkgc  28970  ax5seglem4  29017  grpomuldivass  30628  ablomuldiv  30639  ablodivdiv4  30641  nvmdi  30735  dipdi  30930  dipsubdir  30935  dipsubdi  30936  cgr3tr4  36265  cgr3rflx  36267  seglemin  36326  linerflx1  36362  elicc3  36530  rngosubdi  38193  rngosubdir  38194  igenval2  38314  dmncan1  38324  latmassOLD  39602  omlfh1N  39631  omlfh3N  39632  cvrnbtwn  39644  cvrnbtwn2  39648  cvrnbtwn4  39652  hlatj12  39744  cvrntr  39798  islpln2a  39921  3atnelvolN  39959  elpadd2at2  40180  paddasslem17  40209  paddass  40211  paddssw2  40217  pmapjlln1  40228  ltrn2ateq  40553  cdlemc3  40566  cdleme1b  40599  cdleme3b  40602  cdleme3c  40603  cdleme9b  40625  erngdvlem3  41363  erngdvlem3-rN  41371  dvalveclem  41398  mendlmod  43543  lincsumscmcl  48790