Theorem 3adant3r3 1180

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  infsupprpr  8968  ressress  16562  plttr  17580  plelttr  17582  latledi  17699  latmlej11  17700  latmlej21  17702  latmlej22  17703  latjass  17705  latj12  17706  latj31  17709  ipopos  17770  latdisdlem  17799  imasmnd2  17948  imasmnd  17949  grpaddsubass  18189  grpsubsub4  18192  grpnpncan  18194  imasgrp2  18214  imasgrp  18215  frgp0  18886  cmn12  18927  abladdsub  18935  imasring  19369  dvrass  19440  lss1  19710  islmhm2  19810  psrgrp  20178  psrlmod  20181  zntoslem  20703  ipdir  20783  t1sep  21978  mettri2  22951  xmetrtri  22965  xmetrtri2  22966  pi1grplem  23653  dchrabl  25830  motgrp  26329  xmstrkgc  26672  ax5seglem4  26718  grpomuldivass  28318  ablomuldiv  28329  ablodivdiv4  28331  nvmdi  28425  dipdi  28620  dipsubdir  28625  dipsubdi  28626  cgr3tr4  33513  cgr3rflx  33515  seglemin  33574  linerflx1  33610  elicc3  33665  rngosubdi  35238  rngosubdir  35239  igenval2  35359  dmncan1  35369  latmassOLD  36380  omlfh1N  36409  omlfh3N  36410  cvrnbtwn  36422  cvrnbtwn2  36426  cvrnbtwn4  36430  hlatj12  36522  cvrntr  36576  islpln2a  36699  3atnelvolN  36737  elpadd2at2  36958  paddasslem17  36987  paddass  36989  paddssw2  36995  pmapjlln1  37006  ltrn2ateq  37331  cdlemc3  37344  cdleme1b  37377  cdleme3b  37380  cdleme3c  37381  cdleme9b  37403  erngdvlem3  38141  erngdvlem3-rN  38149  dvalveclem  38176  mendlmod  39842  lincsumscmcl  44537