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 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  dif1en  9153  ccatswrd  14728  plttr  18418  pltletr  18419  latjlej1  18531  latjlej2  18532  latnlej  18534  latnlej2  18537  latmlem2  18548  latledi  18555  latjass  18561  latj32  18563  latj13  18564  ipopos  18614  tsrlemax  18664  imasmnd2  18869  grpsubsub  19139  grpnnncan2  19147  imasgrp2  19165  mulgnn0ass  19220  mulgsubdir  19224  cmn32  19914  ablsubadd  19923  imasrng  20299  imasring  20458  isdomn4  20864  zntoslem  21756  xmettri3  24561  mettri3  24562  xmetrtri  24563  xmetrtri2  24564  metrtri  24565  cphdivcl  25392  cphassr  25422  relogbmulexp  26994  grpodivdiv  30963  grpomuldivass  30964  ablo32  30972  ablodivdiv4  30977  ablodiv32  30978  nvmdi  31071  dipdi  31266  dipassr  31269  dipsubdir  31271  dipsubdi  31272  dvrcan5  33619  cgr3tr4  36581  cgr3rflx  36583  endofsegid  36614  seglemin  36642  broutsideof2  36651  rngosubdi  38654  rngosubdir  38655  isdrngo2  38667  crngm23  38711  dmncan2  38786  latmassOLD  40061  latm32  40063  cvrnbtwn4  40111  cvrcmp2  40116  ltcvrntr  40256  atcvrj0  40260  3dim3  40301  paddasslem17  40668  paddass  40670  lautlt  40923  lautcvr  40924  lautj  40925  lautm  40926  erngdvlem3  41822  dvalveclem  41857  mendlmod  43974  idomcanr  49170