Theorem 3adant3r3 1164

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  infsupprpr  8763  ressress  16418  plttr  17438  plelttr  17440  latledi  17557  latmlej11  17558  latmlej21  17560  latmlej22  17561  latjass  17563  latj12  17564  latj31  17567  ipopos  17628  latdisdlem  17657  imasmnd2  17795  imasmnd  17796  grpaddsubass  17976  grpsubsub4  17979  grpnpncan  17981  imasgrp2  18001  imasgrp  18002  frgp0  18646  cmn12  18686  abladdsub  18693  imasring  19092  dvrass  19163  lss1  19432  islmhm2  19532  psrgrp  19892  psrlmod  19895  zntoslem  20405  ipdir  20485  t1sep  21682  mettri2  22654  xmetrtri  22668  xmetrtri2  22669  pi1grplem  23356  dchrabl  25532  motgrp  26031  xmstrkgc  26375  ax5seglem4  26421  grpomuldivass  28095  ablomuldiv  28106  ablodivdiv4  28108  nvmdi  28202  dipdi  28397  dipsubdir  28402  dipsubdi  28403  cgr3tr4  33040  cgr3rflx  33042  seglemin  33101  linerflx1  33137  elicc3  33192  rngosubdi  34671  rngosubdir  34672  igenval2  34792  dmncan1  34802  latmassOLD  35816  omlfh1N  35845  omlfh3N  35846  cvrnbtwn  35858  cvrnbtwn2  35862  cvrnbtwn4  35866  hlatj12  35958  cvrntr  36012  islpln2a  36135  3atnelvolN  36173  elpadd2at2  36394  paddasslem17  36423  paddass  36425  paddssw2  36431  pmapjlln1  36442  ltrn2ateq  36767  cdlemc3  36780  cdleme1b  36813  cdleme3b  36816  cdleme3c  36817  cdleme9b  36839  erngdvlem3  37577  erngdvlem3-rN  37585  dvalveclem  37612  mendlmod  39195  lincsumscmcl  43861