Theorem 3adant3r1 1201

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  dif1en  9142  ccatswrd  14702  plttr  18391  pltletr  18392  latjlej1  18504  latjlej2  18505  latnlej  18507  latnlej2  18510  latmlem2  18521  latledi  18528  latjass  18534  latj32  18536  latj13  18537  ipopos  18587  tsrlemax  18637  imasmnd2  18827  grpsubsub  19090  grpnnncan2  19098  imasgrp2  19116  mulgnn0ass  19171  mulgsubdir  19175  cmn32  19865  ablsubadd  19874  imasrng  20250  imasring  20408  isdomn4  20814  zntoslem  21706  xmettri3  24510  mettri3  24511  xmetrtri  24512  xmetrtri2  24513  metrtri  24514  cphdivcl  25341  cphassr  25371  relogbmulexp  26943  grpodivdiv  30892  grpomuldivass  30893  ablo32  30901  ablodivdiv4  30906  ablodiv32  30907  nvmdi  31000  dipdi  31195  dipassr  31198  dipsubdir  31200  dipsubdi  31201  dvrcan5  33555  cgr3tr4  36544  cgr3rflx  36546  endofsegid  36577  seglemin  36605  broutsideof2  36614  rngosubdi  38596  rngosubdir  38597  isdrngo2  38609  crngm23  38653  dmncan2  38728  latmassOLD  40003  latm32  40005  cvrnbtwn4  40053  cvrcmp2  40058  ltcvrntr  40198  atcvrj0  40202  3dim3  40243  paddasslem17  40610  paddass  40612  lautlt  40865  lautcvr  40866  lautj  40867  lautm  40868  erngdvlem3  41764  dvalveclem  41799  mendlmod  43916  idomcanr  49113