Theorem 3adant3r1 1175

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  plttr  17414  pltletr  17415  latjlej1  17509  latjlej2  17510  latnlej  17512  latnlej2  17515  latmlem2  17526  latledi  17533  latjass  17539  latj32  17541  latj13  17542  ipopos  17604  tsrlemax  17664  imasmnd2  17771  grpsubsub  17950  grpnnncan2  17958  imasgrp2  17976  mulgnn0ass  18022  mulgsubdir  18026  cmn32  18656  ablsubadd  18662  imasring  19064  zntoslem  20390  xmettri3  22651  mettri3  22652  xmetrtri  22653  xmetrtri2  22654  metrtri  22655  cphdivcl  23474  cphassr  23504  relogbmulexp  25042  grpodivdiv  28013  grpomuldivass  28014  ablo32  28022  ablodivdiv4  28027  ablodiv32  28028  nvmdi  28121  dipdi  28316  dipassr  28319  dipsubdir  28321  dipsubdi  28322  dvrcan5  30523  cgr3tr4  33128  cgr3rflx  33130  endofsegid  33161  seglemin  33189  broutsideof2  33198  rngosubdi  34780  rngosubdir  34781  isdrngo2  34793  crngm23  34837  dmncan2  34912  latmassOLD  35921  latm32  35923  cvrnbtwn4  35971  cvrcmp2  35976  ltcvrntr  36116  atcvrj0  36120  3dim3  36161  paddasslem17  36528  paddass  36530  lautlt  36783  lautcvr  36784  lautj  36785  lautm  36786  erngdvlem3  37682  dvalveclem  37717  mendlmod  39303