Theorem 3adant3r3 1182

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 1087

This theorem is referenced by:  infsupprpr  9224  ressress  16939  plttr  18041  plelttr  18043  latledi  18176  latmlej11  18177  latmlej21  18179  latmlej22  18180  latjass  18182  latj12  18183  latj31  18186  latdisdlem  18195  ipopos  18235  imasmnd2  18403  imasmnd  18404  grpaddsubass  18646  grpsubsub4  18649  grpnpncan  18651  imasgrp2  18671  imasgrp  18672  frgp0  19347  cmn12  19388  abladdsub  19397  imasring  19839  dvrass  19913  lss1  20181  islmhm2  20281  zntoslem  20745  ipdir  20825  psrgrp  21148  psrlmod  21151  t1sep  22502  mettri2  23475  xmetrtri  23489  xmetrtri2  23490  pi1grplem  24193  dchrabl  26383  motgrp  26885  xmstrkgc  27234  ax5seglem4  27281  grpomuldivass  28882  ablomuldiv  28893  ablodivdiv4  28895  nvmdi  28989  dipdi  29184  dipsubdir  29189  dipsubdi  29190  cgr3tr4  34333  cgr3rflx  34335  seglemin  34394  linerflx1  34430  elicc3  34485  rngosubdi  36082  rngosubdir  36083  igenval2  36203  dmncan1  36213  latmassOLD  37222  omlfh1N  37251  omlfh3N  37252  cvrnbtwn  37264  cvrnbtwn2  37268  cvrnbtwn4  37272  hlatj12  37364  cvrntr  37418  islpln2a  37541  3atnelvolN  37579  elpadd2at2  37800  paddasslem17  37829  paddass  37831  paddssw2  37837  pmapjlln1  37848  ltrn2ateq  38173  cdlemc3  38186  cdleme1b  38219  cdleme3b  38222  cdleme3c  38223  cdleme9b  38245  erngdvlem3  38983  erngdvlem3-rN  38991  dvalveclem  39018  isdomn4  40152  mendlmod  40998  lincsumscmcl  45726