Theorem 3adant3r3 1197

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

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

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  infsupprpr  9446  ressress  17274  plttr  18363  plelttr  18365  latledi  18500  latmlej11  18501  latmlej21  18503  latmlej22  18504  latjass  18506  latj12  18507  latj31  18510  latdisdlem  18519  ipopos  18559  imasmnd2  18799  imasmnd  18800  grpaddsubass  19063  grpsubsub4  19066  grpnpncan  19068  imasgrp2  19088  imasgrp  19089  frgp0  19791  cmn12  19833  abladdsub  19843  imasrng  20214  imasring  20366  dvrass  20444  isdomn4  20753  lss1  20993  islmhm2  21093  zntoslem  21596  ipdir  21679  psrlmod  21999  t1sep  23418  mettri2  24389  xmetrtri  24403  xmetrtri2  24404  pi1grplem  25099  dchrabl  27306  motgrp  28700  xmstrkgc  29043  ax5seglem4  29090  grpomuldivass  30701  ablomuldiv  30712  ablodivdiv4  30714  nvmdi  30808  dipdi  31003  dipsubdir  31008  dipsubdi  31009  cgr3tr4  36363  cgr3rflx  36365  seglemin  36424  linerflx1  36460  elicc3  36638  rngosubdi  38405  rngosubdir  38406  igenval2  38526  dmncan1  38536  latmassOLD  39814  omlfh1N  39843  omlfh3N  39844  cvrnbtwn  39856  cvrnbtwn2  39860  cvrnbtwn4  39864  hlatj12  39956  cvrntr  40010  islpln2a  40133  3atnelvolN  40171  elpadd2at2  40392  paddasslem17  40421  paddass  40423  paddssw2  40429  pmapjlln1  40440  ltrn2ateq  40765  cdlemc3  40778  cdleme1b  40811  cdleme3b  40814  cdleme3c  40815  cdleme9b  40837  erngdvlem3  41575  erngdvlem3-rN  41583  dvalveclem  41610  mendlmod  43727  lincsumscmcl  49016