Theorem 3adant3r1 1183

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  dif1en  9156  ccatswrd  14614  plttr  18291  pltletr  18292  latjlej1  18402  latjlej2  18403  latnlej  18405  latnlej2  18408  latmlem2  18419  latledi  18426  latjass  18432  latj32  18434  latj13  18435  ipopos  18485  tsrlemax  18535  imasmnd2  18658  grpsubsub  18908  grpnnncan2  18916  imasgrp2  18934  mulgnn0ass  18984  mulgsubdir  18988  cmn32  19661  ablsubadd  19669  imasring  20133  zntoslem  21096  xmettri3  23841  mettri3  23842  xmetrtri  23843  xmetrtri2  23844  metrtri  23845  cphdivcl  24681  cphassr  24711  relogbmulexp  26263  grpodivdiv  29771  grpomuldivass  29772  ablo32  29780  ablodivdiv4  29785  ablodiv32  29786  nvmdi  29879  dipdi  30074  dipassr  30077  dipsubdir  30079  dipsubdi  30080  dvrcan5  32360  cgr3tr4  34962  cgr3rflx  34964  endofsegid  34995  seglemin  35023  broutsideof2  35032  rngosubdi  36751  rngosubdir  36752  isdrngo2  36764  crngm23  36808  dmncan2  36883  latmassOLD  38037  latm32  38039  cvrnbtwn4  38087  cvrcmp2  38092  ltcvrntr  38233  atcvrj0  38237  3dim3  38278  paddasslem17  38645  paddass  38647  lautlt  38900  lautcvr  38901  lautj  38902  lautm  38903  erngdvlem3  39799  dvalveclem  39834  isdomn4  40970  mendlmod  41868  imasrng  46613