Theorem 3adant3r1 1182

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 1169	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  9226  ccatswrd  14716  plttr  18412  pltletr  18413  latjlej1  18523  latjlej2  18524  latnlej  18526  latnlej2  18529  latmlem2  18540  latledi  18547  latjass  18553  latj32  18555  latj13  18556  ipopos  18606  tsrlemax  18656  imasmnd2  18809  grpsubsub  19069  grpnnncan2  19077  imasgrp2  19095  mulgnn0ass  19150  mulgsubdir  19154  cmn32  19842  ablsubadd  19851  imasrng  20204  imasring  20353  isdomn4  20738  zntoslem  21598  xmettri3  24384  mettri3  24385  xmetrtri  24386  xmetrtri2  24387  metrtri  24388  cphdivcl  25235  cphassr  25265  relogbmulexp  26839  grpodivdiv  30572  grpomuldivass  30573  ablo32  30581  ablodivdiv4  30586  ablodiv32  30587  nvmdi  30680  dipdi  30875  dipassr  30878  dipsubdir  30880  dipsubdi  30881  dvrcan5  33216  cgr3tr4  36016  cgr3rflx  36018  endofsegid  36049  seglemin  36077  broutsideof2  36086  rngosubdi  37905  rngosubdir  37906  isdrngo2  37918  crngm23  37962  dmncan2  38037  latmassOLD  39185  latm32  39187  cvrnbtwn4  39235  cvrcmp2  39240  ltcvrntr  39381  atcvrj0  39385  3dim3  39426  paddasslem17  39793  paddass  39795  lautlt  40048  lautcvr  40049  lautj  40050  lautm  40051  erngdvlem3  40947  dvalveclem  40982  mendlmod  43150