Theorem 3adant3r1 1196

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 1133	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1183	1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  dif1en  9130  ccatswrd  14682  plttr  18372  pltletr  18373  latjlej1  18485  latjlej2  18486  latnlej  18488  latnlej2  18491  latmlem2  18502  latledi  18509  latjass  18515  latj32  18517  latj13  18518  ipopos  18568  tsrlemax  18618  imasmnd2  18808  grpsubsub  19071  grpnnncan2  19079  imasgrp2  19097  mulgnn0ass  19152  mulgsubdir  19156  cmn32  19840  ablsubadd  19849  imasrng  20223  imasring  20375  isdomn4  20762  zntoslem  21605  xmettri3  24410  mettri3  24411  xmetrtri  24412  xmetrtri2  24413  metrtri  24414  cphdivcl  25241  cphassr  25271  relogbmulexp  26840  grpodivdiv  30740  grpomuldivass  30741  ablo32  30749  ablodivdiv4  30754  ablodiv32  30755  nvmdi  30848  dipdi  31043  dipassr  31046  dipsubdir  31048  dipsubdi  31049  dvrcan5  33413  cgr3tr4  36399  cgr3rflx  36401  endofsegid  36432  seglemin  36460  broutsideof2  36469  rngosubdi  38441  rngosubdir  38442  isdrngo2  38454  crngm23  38498  dmncan2  38573  latmassOLD  39850  latm32  39852  cvrnbtwn4  39900  cvrcmp2  39905  ltcvrntr  40045  atcvrj0  40049  3dim3  40090  paddasslem17  40457  paddass  40459  lautlt  40712  lautcvr  40713  lautj  40714  lautm  40715  erngdvlem3  41611  dvalveclem  41646  mendlmod  43763