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  9172  ccatswrd  14684  plttr  18350  pltletr  18351  latjlej1  18461  latjlej2  18462  latnlej  18464  latnlej2  18467  latmlem2  18478  latledi  18485  latjass  18491  latj32  18493  latj13  18494  ipopos  18544  tsrlemax  18594  imasmnd2  18750  grpsubsub  19010  grpnnncan2  19018  imasgrp2  19036  mulgnn0ass  19091  mulgsubdir  19095  cmn32  19779  ablsubadd  19788  imasrng  20135  imasring  20288  isdomn4  20674  zntoslem  21515  xmettri3  24290  mettri3  24291  xmetrtri  24292  xmetrtri2  24293  metrtri  24294  cphdivcl  25132  cphassr  25162  relogbmulexp  26738  grpodivdiv  30467  grpomuldivass  30468  ablo32  30476  ablodivdiv4  30481  ablodiv32  30482  nvmdi  30575  dipdi  30770  dipassr  30773  dipsubdir  30775  dipsubdi  30776  dvrcan5  33177  cgr3tr4  36016  cgr3rflx  36018  endofsegid  36049  seglemin  36077  broutsideof2  36086  rngosubdi  37915  rngosubdir  37916  isdrngo2  37928  crngm23  37972  dmncan2  38047  latmassOLD  39193  latm32  39195  cvrnbtwn4  39243  cvrcmp2  39248  ltcvrntr  39389  atcvrj0  39393  3dim3  39434  paddasslem17  39801  paddass  39803  lautlt  40056  lautcvr  40057  lautj  40058  lautm  40059  erngdvlem3  40955  dvalveclem  40990  mendlmod  43160