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  9385  ressress  17153  plttr  18241  plelttr  18243  latledi  18378  latmlej11  18379  latmlej21  18381  latmlej22  18382  latjass  18384  latj12  18385  latj31  18388  latdisdlem  18397  ipopos  18437  imasmnd2  18677  imasmnd  18678  grpaddsubass  18938  grpsubsub4  18941  grpnpncan  18943  imasgrp2  18963  imasgrp  18964  frgp0  19667  cmn12  19709  abladdsub  19719  imasrng  20090  imasring  20243  dvrass  20321  isdomn4  20626  lss1  20866  islmhm2  20967  zntoslem  21488  ipdir  21571  psrgrpOLD  21889  psrlmod  21892  t1sep  23280  mettri2  24251  xmetrtri  24265  xmetrtri2  24266  pi1grplem  24971  dchrabl  27187  motgrp  28516  xmstrkgc  28859  ax5seglem4  28905  grpomuldivass  30513  ablomuldiv  30524  ablodivdiv4  30526  nvmdi  30620  dipdi  30815  dipsubdir  30820  dipsubdi  30821  cgr3tr4  36086  cgr3rflx  36088  seglemin  36147  linerflx1  36183  elicc3  36351  rngosubdi  37985  rngosubdir  37986  igenval2  38106  dmncan1  38116  latmassOLD  39268  omlfh1N  39297  omlfh3N  39298  cvrnbtwn  39310  cvrnbtwn2  39314  cvrnbtwn4  39318  hlatj12  39410  cvrntr  39464  islpln2a  39587  3atnelvolN  39625  elpadd2at2  39846  paddasslem17  39875  paddass  39877  paddssw2  39883  pmapjlln1  39894  ltrn2ateq  40219  cdlemc3  40232  cdleme1b  40265  cdleme3b  40268  cdleme3c  40269  cdleme9b  40291  erngdvlem3  41029  erngdvlem3-rN  41037  dvalveclem  41064  mendlmod  43222  lincsumscmcl  48465