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  9156  ccatswrd  14738  plttr  18428  pltletr  18429  latjlej1  18541  latjlej2  18542  latnlej  18544  latnlej2  18547  latmlem2  18558  latledi  18565  latjass  18571  latj32  18573  latj13  18574  ipopos  18624  tsrlemax  18674  imasmnd2  18881  grpsubsub  19152  grpnnncan2  19160  imasgrp2  19178  mulgnn0ass  19233  mulgsubdir  19237  cmn32  19927  ablsubadd  19936  imasrng  20312  imasring  20471  isdomn4  20877  zntoslem  21769  xmettri3  24579  mettri3  24580  xmetrtri  24581  xmetrtri2  24582  metrtri  24583  cphdivcl  25410  cphassr  25440  relogbmulexp  27015  grpodivdiv  31021  grpomuldivass  31022  ablo32  31030  ablodivdiv4  31035  ablodiv32  31036  nvmdi  31129  dipdi  31324  dipassr  31327  dipsubdir  31329  dipsubdi  31330  dvrcan5  33675  cgr3tr4  36632  cgr3rflx  36634  endofsegid  36665  seglemin  36693  broutsideof2  36702  rngosubdi  38695  rngosubdir  38696  isdrngo2  38708  crngm23  38752  dmncan2  38827  latmassOLD  40102  latm32  40104  cvrnbtwn4  40152  cvrcmp2  40157  ltcvrntr  40297  atcvrj0  40301  3dim3  40342  paddasslem17  40709  paddass  40711  lautlt  40964  lautcvr  40965  lautj  40966  lautm  40967  erngdvlem3  41863  dvalveclem  41898  mendlmod  44030  idomcanr  49263