Theorem 3adant3r1 1183

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  dif1en  9130  ccatswrd  14640  plttr  18308  pltletr  18309  latjlej1  18419  latjlej2  18420  latnlej  18422  latnlej2  18425  latmlem2  18436  latledi  18443  latjass  18449  latj32  18451  latj13  18452  ipopos  18502  tsrlemax  18552  imasmnd2  18708  grpsubsub  18968  grpnnncan2  18976  imasgrp2  18994  mulgnn0ass  19049  mulgsubdir  19053  cmn32  19737  ablsubadd  19746  imasrng  20093  imasring  20246  isdomn4  20632  zntoslem  21473  xmettri3  24248  mettri3  24249  xmetrtri  24250  xmetrtri2  24251  metrtri  24252  cphdivcl  25089  cphassr  25119  relogbmulexp  26695  grpodivdiv  30476  grpomuldivass  30477  ablo32  30485  ablodivdiv4  30490  ablodiv32  30491  nvmdi  30584  dipdi  30779  dipassr  30782  dipsubdir  30784  dipsubdi  30785  dvrcan5  33194  cgr3tr4  36047  cgr3rflx  36049  endofsegid  36080  seglemin  36108  broutsideof2  36117  rngosubdi  37946  rngosubdir  37947  isdrngo2  37959  crngm23  38003  dmncan2  38078  latmassOLD  39229  latm32  39231  cvrnbtwn4  39279  cvrcmp2  39284  ltcvrntr  39425  atcvrj0  39429  3dim3  39470  paddasslem17  39837  paddass  39839  lautlt  40092  lautcvr  40093  lautj  40094  lautm  40095  erngdvlem3  40991  dvalveclem  41026  mendlmod  43185