Theorem 3adant3r3 1186

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

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

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 1089

This theorem is referenced by:  infsupprpr  9412  ressress  17208  plttr  18297  plelttr  18299  latledi  18434  latmlej11  18435  latmlej21  18437  latmlej22  18438  latjass  18440  latj12  18441  latj31  18444  latdisdlem  18453  ipopos  18493  imasmnd2  18733  imasmnd  18734  grpaddsubass  18997  grpsubsub4  19000  grpnpncan  19002  imasgrp2  19022  imasgrp  19023  frgp0  19726  cmn12  19768  abladdsub  19778  imasrng  20149  imasring  20301  dvrass  20379  isdomn4  20684  lss1  20924  islmhm2  21025  zntoslem  21546  ipdir  21629  psrlmod  21948  t1sep  23345  mettri2  24316  xmetrtri  24330  xmetrtri2  24331  pi1grplem  25026  dchrabl  27231  motgrp  28625  xmstrkgc  28968  ax5seglem4  29015  grpomuldivass  30627  ablomuldiv  30638  ablodivdiv4  30640  nvmdi  30734  dipdi  30929  dipsubdir  30934  dipsubdi  30935  cgr3tr4  36250  cgr3rflx  36252  seglemin  36311  linerflx1  36347  elicc3  36515  rngosubdi  38280  rngosubdir  38281  igenval2  38401  dmncan1  38411  latmassOLD  39689  omlfh1N  39718  omlfh3N  39719  cvrnbtwn  39731  cvrnbtwn2  39735  cvrnbtwn4  39739  hlatj12  39831  cvrntr  39885  islpln2a  40008  3atnelvolN  40046  elpadd2at2  40267  paddasslem17  40296  paddass  40298  paddssw2  40304  pmapjlln1  40315  ltrn2ateq  40640  cdlemc3  40653  cdleme1b  40686  cdleme3b  40689  cdleme3c  40690  cdleme9b  40712  erngdvlem3  41450  erngdvlem3-rN  41458  dvalveclem  41485  mendlmod  43635  lincsumscmcl  48921