Theorem 3adant3r1 1196

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1070

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 197  df-an 383  df-3an 1072

This theorem is referenced by:  plttr  17177  pltletr  17178  latjlej1  17272  latjlej2  17273  latnlej  17275  latnlej2  17278  latmlem2  17289  latledi  17296  latjass  17302  latj32  17304  latj13  17305  ipopos  17367  tsrlemax  17427  imasmnd2  17534  grpsubsub  17711  grpnnncan2  17719  imasgrp2  17737  mulgnn0ass  17785  mulgsubdir  17789  cmn32  18417  ablsubadd  18423  imasring  18826  zntoslem  20119  xmettri3  22377  mettri3  22378  xmetrtri  22379  xmetrtri2  22380  metrtri  22381  cphdivcl  23200  cphassr  23230  relogbmulexp  24736  grpodivdiv  27728  grpomuldivass  27729  ablo32  27737  ablodivdiv4  27742  ablodiv32  27743  ablonnncan  27744  nvmdi  27837  dipdi  28032  dipassr  28035  dipsubdir  28037  dipsubdi  28038  dvrcan5  30127  cgr3tr4  32490  cgr3rflx  32492  endofsegid  32523  seglemin  32551  broutsideof2  32560  rngosubdi  34069  rngosubdir  34070  isdrngo2  34082  crngm23  34126  dmncan2  34201  latmassOLD  35031  latm32  35033  cvrnbtwn4  35081  cvrcmp2  35086  ltcvrntr  35225  atcvrj0  35229  3dim3  35270  paddasslem17  35637  paddass  35639  lautlt  35892  lautcvr  35893  lautj  35894  lautm  35895  erngdvlem3  36792  dvalveclem  36828  mendlmod  38282