Theorem 3adant3r3 1203

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 1138	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1190	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  infsupprpr  9480  ressress  17345  plttr  18434  plelttr  18436  latledi  18571  latmlej11  18572  latmlej21  18574  latmlej22  18575  latjass  18577  latj12  18578  latj31  18581  latdisdlem  18590  ipopos  18630  imasmnd2  18887  imasmnd  18888  grpaddsubass  19159  grpsubsub4  19162  grpnpncan  19164  imasgrp2  19184  imasgrp  19185  frgp0  19893  cmn12  19935  abladdsub  19945  imasrng  20318  imasring  20477  dvrass  20555  isdomn4  20883  lss1  21128  islmhm2  21228  unichnlidl  21431  rspprop  21439  zntoslem  21775  ipdir  21858  psrlmod  22180  t1sep  23601  mettri2  24573  xmetrtri  24587  xmetrtri2  24588  pi1grplem  25283  dchrabl  27498  motgrp  28893  xmstrkgc  29350  ax5seglem4  29397  grpomuldivass  31030  ablomuldiv  31041  ablodivdiv4  31043  nvmdi  31137  dipdi  31332  dipsubdir  31337  dipsubdi  31338  cgr3tr4  36640  cgr3rflx  36642  seglemin  36701  linerflx1  36737  elicc3  36944  rngosubdi  38703  rngosubdir  38704  igenval2  38824  dmncan1  38834  latmassOLD  40110  omlfh1N  40139  omlfh3N  40140  cvrnbtwn  40152  cvrnbtwn2  40156  cvrnbtwn4  40160  hlatj12  40252  cvrntr  40306  islpln2a  40429  3atnelvolN  40467  elpadd2at2  40688  paddasslem17  40717  paddass  40719  paddssw2  40725  pmapjlln1  40736  ltrn2ateq  41061  cdlemc3  41074  cdleme1b  41107  cdleme3b  41110  cdleme3c  41111  cdleme9b  41133  erngdvlem3  41871  erngdvlem3-rN  41879  dvalveclem  41906  mendlmod  44038  lincsumscmcl  49371