Theorem 3adant3r1 1184

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  dif1en  9096  ccatswrd  14631  plttr  18306  pltletr  18307  latjlej1  18419  latjlej2  18420  latnlej  18422  latnlej2  18425  latmlem2  18436  latledi  18443  latjass  18449  latj32  18451  latj13  18452  ipopos  18502  tsrlemax  18552  imasmnd2  18742  grpsubsub  19005  grpnnncan2  19013  imasgrp2  19031  mulgnn0ass  19086  mulgsubdir  19090  cmn32  19775  ablsubadd  19784  imasrng  20158  imasring  20310  isdomn4  20693  zntoslem  21536  xmettri3  24318  mettri3  24319  xmetrtri  24320  xmetrtri2  24321  metrtri  24322  cphdivcl  25149  cphassr  25179  relogbmulexp  26742  grpodivdiv  30611  grpomuldivass  30612  ablo32  30620  ablodivdiv4  30625  ablodiv32  30626  nvmdi  30719  dipdi  30914  dipassr  30917  dipsubdir  30919  dipsubdi  30920  dvrcan5  33297  cgr3tr4  36234  cgr3rflx  36236  endofsegid  36267  seglemin  36295  broutsideof2  36304  rngosubdi  38266  rngosubdir  38267  isdrngo2  38279  crngm23  38323  dmncan2  38398  latmassOLD  39675  latm32  39677  cvrnbtwn4  39725  cvrcmp2  39730  ltcvrntr  39870  atcvrj0  39874  3dim3  39915  paddasslem17  40282  paddass  40284  lautlt  40537  lautcvr  40538  lautj  40539  lautm  40540  erngdvlem3  41436  dvalveclem  41471  mendlmod  43617