Theorem 3adant3r1 1200

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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

This theorem is used by:  dif1en  9144  ccatswrd  14713  plttr  18402  pltletr  18403  latjlej1  18515  latjlej2  18516  latnlej  18518  latnlej2  18521  latmlem2  18532  latledi  18539  latjass  18545  latj32  18547  latj13  18548  ipopos  18598  tsrlemax  18648  imasmnd2  18838  grpsubsub  19101  grpnnncan2  19109  imasgrp2  19127  mulgnn0ass  19182  mulgsubdir  19186  cmn32  19876  ablsubadd  19885  imasrng  20261  imasring  20419  isdomn4  20825  zntoslem  21717  xmettri3  24521  mettri3  24522  xmetrtri  24523  xmetrtri2  24524  metrtri  24525  cphdivcl  25352  cphassr  25382  relogbmulexp  26954  grpodivdiv  30903  grpomuldivass  30904  ablo32  30912  ablodivdiv4  30917  ablodiv32  30918  nvmdi  31011  dipdi  31206  dipassr  31209  dipsubdir  31211  dipsubdi  31212  dvrcan5  33564  cgr3tr4  36552  cgr3rflx  36554  endofsegid  36585  seglemin  36613  broutsideof2  36622  rngosubdi  38624  rngosubdir  38625  isdrngo2  38637  crngm23  38681  dmncan2  38756  latmassOLD  40031  latm32  40033  cvrnbtwn4  40081  cvrcmp2  40086  ltcvrntr  40226  atcvrj0  40230  3dim3  40271  paddasslem17  40638  paddass  40640  lautlt  40893  lautcvr  40894  lautj  40895  lautm  40896  erngdvlem3  41792  dvalveclem  41827  mendlmod  43944  idomcanr  49141