Theorem 3adant3r1 1178

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ccatswrd  14032  plttr  17582  pltletr  17583  latjlej1  17677  latjlej2  17678  latnlej  17680  latnlej2  17683  latmlem2  17694  latledi  17701  latjass  17707  latj32  17709  latj13  17710  ipopos  17772  tsrlemax  17832  imasmnd2  17950  grpsubsub  18190  grpnnncan2  18198  imasgrp2  18216  mulgnn0ass  18265  mulgsubdir  18269  cmn32  18927  ablsubadd  18934  imasring  19371  zntoslem  20705  xmettri3  22965  mettri3  22966  xmetrtri  22967  xmetrtri2  22968  metrtri  22969  cphdivcl  23788  cphassr  23818  relogbmulexp  25358  grpodivdiv  28319  grpomuldivass  28320  ablo32  28328  ablodivdiv4  28333  ablodiv32  28334  nvmdi  28427  dipdi  28622  dipassr  28625  dipsubdir  28627  dipsubdi  28628  dvrcan5  30866  cgr3tr4  33515  cgr3rflx  33517  endofsegid  33548  seglemin  33576  broutsideof2  33585  rngosubdi  35225  rngosubdir  35226  isdrngo2  35238  crngm23  35282  dmncan2  35357  latmassOLD  36367  latm32  36369  cvrnbtwn4  36417  cvrcmp2  36422  ltcvrntr  36562  atcvrj0  36566  3dim3  36607  paddasslem17  36974  paddass  36976  lautlt  37229  lautcvr  37230  lautj  37231  lautm  37232  erngdvlem3  38128  dvalveclem  38163  mendlmod  39800