Theorem 3adant3r1 1181

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)

Hypothesis

Ref	Expression
ad4ant3.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant3r1	⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3adant3r1

Step	Hyp	Ref	Expression
1		ad4ant3.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1119	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1168	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:  ccatswrd  14390  plttr  18069  pltletr  18070  latjlej1  18180  latjlej2  18181  latnlej  18183  latnlej2  18186  latmlem2  18197  latledi  18204  latjass  18210  latj32  18212  latj13  18213  ipopos  18263  tsrlemax  18313  imasmnd2  18431  grpsubsub  18673  grpnnncan2  18681  imasgrp2  18699  mulgnn0ass  18748  mulgsubdir  18752  cmn32  19414  ablsubadd  19422  imasring  19867  zntoslem  20773  xmettri3  23515  mettri3  23516  xmetrtri  23517  xmetrtri2  23518  metrtri  23519  cphdivcl  24355  cphassr  24385  relogbmulexp  25937  grpodivdiv  28911  grpomuldivass  28912  ablo32  28920  ablodivdiv4  28925  ablodiv32  28926  nvmdi  29019  dipdi  29214  dipassr  29217  dipsubdir  29219  dipsubdi  29220  dvrcan5  31499  cgr3tr4  34363  cgr3rflx  34365  endofsegid  34396  seglemin  34424  broutsideof2  34433  rngosubdi  36112  rngosubdir  36113  isdrngo2  36125  crngm23  36169  dmncan2  36244  latmassOLD  37250  latm32  37252  cvrnbtwn4  37300  cvrcmp2  37305  ltcvrntr  37445  atcvrj0  37449  3dim3  37490  paddasslem17  37857  paddass  37859  lautlt  38112  lautcvr  38113  lautj  38114  lautm  38115  erngdvlem3  39011  dvalveclem  39046  isdomn4  40179  mendlmod  41025