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  9075  ccatswrd  14575  plttr  18246  pltletr  18247  latjlej1  18359  latjlej2  18360  latnlej  18362  latnlej2  18365  latmlem2  18376  latledi  18383  latjass  18389  latj32  18391  latj13  18392  ipopos  18442  tsrlemax  18492  imasmnd2  18648  grpsubsub  18908  grpnnncan2  18916  imasgrp2  18934  mulgnn0ass  18989  mulgsubdir  18993  cmn32  19679  ablsubadd  19688  imasrng  20062  imasring  20215  isdomn4  20601  zntoslem  21463  xmettri3  24239  mettri3  24240  xmetrtri  24241  xmetrtri2  24242  metrtri  24243  cphdivcl  25080  cphassr  25110  relogbmulexp  26686  grpodivdiv  30484  grpomuldivass  30485  ablo32  30493  ablodivdiv4  30498  ablodiv32  30499  nvmdi  30592  dipdi  30787  dipassr  30790  dipsubdir  30792  dipsubdi  30793  dvrcan5  33176  cgr3tr4  36026  cgr3rflx  36028  endofsegid  36059  seglemin  36087  broutsideof2  36096  rngosubdi  37925  rngosubdir  37926  isdrngo2  37938  crngm23  37982  dmncan2  38057  latmassOLD  39208  latm32  39210  cvrnbtwn4  39258  cvrcmp2  39263  ltcvrntr  39403  atcvrj0  39407  3dim3  39448  paddasslem17  39815  paddass  39817  lautlt  40070  lautcvr  40071  lautj  40072  lautm  40073  erngdvlem3  40969  dvalveclem  41004  mendlmod  43162