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  9523  ressress  17273  plttr  18357  plelttr  18359  latledi  18492  latmlej11  18493  latmlej21  18495  latmlej22  18496  latjass  18498  latj12  18499  latj31  18502  latdisdlem  18511  ipopos  18551  imasmnd2  18757  imasmnd  18758  grpaddsubass  19018  grpsubsub4  19021  grpnpncan  19023  imasgrp2  19043  imasgrp  19044  frgp0  19746  cmn12  19788  abladdsub  19798  imasrng  20142  imasring  20295  dvrass  20373  isdomn4  20681  lss1  20900  islmhm2  21001  zntoslem  21522  ipdir  21604  psrgrpOLD  21922  psrlmod  21925  t1sep  23313  mettri2  24285  xmetrtri  24299  xmetrtri2  24300  pi1grplem  25005  dchrabl  27222  motgrp  28527  xmstrkgc  28870  ax5seglem4  28916  grpomuldivass  30527  ablomuldiv  30538  ablodivdiv4  30540  nvmdi  30634  dipdi  30829  dipsubdir  30834  dipsubdi  30835  cgr3tr4  36075  cgr3rflx  36077  seglemin  36136  linerflx1  36172  elicc3  36340  rngosubdi  37974  rngosubdir  37975  igenval2  38095  dmncan1  38105  latmassOLD  39252  omlfh1N  39281  omlfh3N  39282  cvrnbtwn  39294  cvrnbtwn2  39298  cvrnbtwn4  39302  hlatj12  39394  cvrntr  39449  islpln2a  39572  3atnelvolN  39610  elpadd2at2  39831  paddasslem17  39860  paddass  39862  paddssw2  39868  pmapjlln1  39879  ltrn2ateq  40204  cdlemc3  40217  cdleme1b  40250  cdleme3b  40253  cdleme3c  40254  cdleme9b  40276  erngdvlem3  41014  erngdvlem3-rN  41022  dvalveclem  41049  mendlmod  43180  lincsumscmcl  48376