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 396   ∧ 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 397  df-3an 1088

This theorem is referenced by:  infsupprpr  9339  ressress  17032  plttr  18134  plelttr  18136  latledi  18269  latmlej11  18270  latmlej21  18272  latmlej22  18273  latjass  18275  latj12  18276  latj31  18279  latdisdlem  18288  ipopos  18328  imasmnd2  18496  imasmnd  18497  grpaddsubass  18738  grpsubsub4  18741  grpnpncan  18743  imasgrp2  18763  imasgrp  18764  frgp0  19438  cmn12  19479  abladdsub  19488  imasring  19930  dvrass  20004  lss1  20280  islmhm2  20380  zntoslem  20844  ipdir  20924  psrgrp  21247  psrlmod  21250  t1sep  22601  mettri2  23574  xmetrtri  23588  xmetrtri2  23589  pi1grplem  24292  dchrabl  26482  motgrp  27037  xmstrkgc  27386  ax5seglem4  27433  grpomuldivass  29035  ablomuldiv  29046  ablodivdiv4  29048  nvmdi  29142  dipdi  29337  dipsubdir  29342  dipsubdi  29343  cgr3tr4  34424  cgr3rflx  34426  seglemin  34485  linerflx1  34521  elicc3  34576  rngosubdi  36180  rngosubdir  36181  igenval2  36301  dmncan1  36311  latmassOLD  37468  omlfh1N  37497  omlfh3N  37498  cvrnbtwn  37510  cvrnbtwn2  37514  cvrnbtwn4  37518  hlatj12  37610  cvrntr  37665  islpln2a  37788  3atnelvolN  37826  elpadd2at2  38047  paddasslem17  38076  paddass  38078  paddssw2  38084  pmapjlln1  38095  ltrn2ateq  38420  cdlemc3  38433  cdleme1b  38466  cdleme3b  38469  cdleme3c  38470  cdleme9b  38492  erngdvlem3  39230  erngdvlem3-rN  39238  dvalveclem  39265  isdomn4  40401  mendlmod  41240  lincsumscmcl  46044