Theorem 3adant3r3 1185

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 1172	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  infsupprpr  9409  ressress  17174  plttr  18263  plelttr  18265  latledi  18400  latmlej11  18401  latmlej21  18403  latmlej22  18404  latjass  18406  latj12  18407  latj31  18410  latdisdlem  18419  ipopos  18459  imasmnd2  18699  imasmnd  18700  grpaddsubass  18960  grpsubsub4  18963  grpnpncan  18965  imasgrp2  18985  imasgrp  18986  frgp0  19689  cmn12  19731  abladdsub  19741  imasrng  20112  imasring  20266  dvrass  20344  isdomn4  20649  lss1  20889  islmhm2  20990  zntoslem  21511  ipdir  21594  psrlmod  21915  t1sep  23314  mettri2  24285  xmetrtri  24299  xmetrtri2  24300  pi1grplem  25005  dchrabl  27221  motgrp  28615  xmstrkgc  28958  ax5seglem4  29005  grpomuldivass  30616  ablomuldiv  30627  ablodivdiv4  30629  nvmdi  30723  dipdi  30918  dipsubdir  30923  dipsubdi  30924  cgr3tr4  36246  cgr3rflx  36248  seglemin  36307  linerflx1  36343  elicc3  36511  rngosubdi  38142  rngosubdir  38143  igenval2  38263  dmncan1  38273  latmassOLD  39485  omlfh1N  39514  omlfh3N  39515  cvrnbtwn  39527  cvrnbtwn2  39531  cvrnbtwn4  39535  hlatj12  39627  cvrntr  39681  islpln2a  39804  3atnelvolN  39842  elpadd2at2  40063  paddasslem17  40092  paddass  40094  paddssw2  40100  pmapjlln1  40111  ltrn2ateq  40436  cdlemc3  40449  cdleme1b  40482  cdleme3b  40485  cdleme3c  40486  cdleme9b  40508  erngdvlem3  41246  erngdvlem3-rN  41254  dvalveclem  41281  mendlmod  43427  lincsumscmcl  48675