Theorem 3adant3r3 1183

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 1119	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1170	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 206  df-an 396  df-3an 1088

This theorem is referenced by:  infsupprpr  9503  ressress  17198  plttr  18300  plelttr  18302  latledi  18435  latmlej11  18436  latmlej21  18438  latmlej22  18439  latjass  18441  latj12  18442  latj31  18445  latdisdlem  18454  ipopos  18494  imasmnd2  18697  imasmnd  18698  grpaddsubass  18950  grpsubsub4  18953  grpnpncan  18955  imasgrp2  18975  imasgrp  18976  frgp0  19670  cmn12  19712  abladdsub  19722  imasrng  20072  imasring  20219  dvrass  20300  lss1  20694  islmhm2  20794  isdomn4  21119  zntoslem  21332  ipdir  21412  psrgrpOLD  21738  psrlmod  21741  t1sep  23095  mettri2  24068  xmetrtri  24082  xmetrtri2  24083  pi1grplem  24797  dchrabl  26994  motgrp  28062  xmstrkgc  28411  ax5seglem4  28458  grpomuldivass  30062  ablomuldiv  30073  ablodivdiv4  30075  nvmdi  30169  dipdi  30364  dipsubdir  30369  dipsubdi  30370  cgr3tr4  35329  cgr3rflx  35331  seglemin  35390  linerflx1  35426  elicc3  35506  rngosubdi  37117  rngosubdir  37118  igenval2  37238  dmncan1  37248  latmassOLD  38403  omlfh1N  38432  omlfh3N  38433  cvrnbtwn  38445  cvrnbtwn2  38449  cvrnbtwn4  38453  hlatj12  38545  cvrntr  38600  islpln2a  38723  3atnelvolN  38761  elpadd2at2  38982  paddasslem17  39011  paddass  39013  paddssw2  39019  pmapjlln1  39030  ltrn2ateq  39355  cdlemc3  39368  cdleme1b  39401  cdleme3b  39404  cdleme3c  39405  cdleme9b  39427  erngdvlem3  40165  erngdvlem3-rN  40173  dvalveclem  40200  mendlmod  42238  lincsumscmcl  47202