Theorem 3adant3r1 1178

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ccatswrd  14030  plttr  17580  pltletr  17581  latjlej1  17675  latjlej2  17676  latnlej  17678  latnlej2  17681  latmlem2  17692  latledi  17699  latjass  17705  latj32  17707  latj13  17708  ipopos  17770  tsrlemax  17830  imasmnd2  17948  grpsubsub  18188  grpnnncan2  18196  imasgrp2  18214  mulgnn0ass  18263  mulgsubdir  18267  cmn32  18925  ablsubadd  18932  imasring  19369  zntoslem  20703  xmettri3  22963  mettri3  22964  xmetrtri  22965  xmetrtri2  22966  metrtri  22967  cphdivcl  23786  cphassr  23816  relogbmulexp  25356  grpodivdiv  28317  grpomuldivass  28318  ablo32  28326  ablodivdiv4  28331  ablodiv32  28332  nvmdi  28425  dipdi  28620  dipassr  28623  dipsubdir  28625  dipsubdi  28626  dvrcan5  30864  cgr3tr4  33513  cgr3rflx  33515  endofsegid  33546  seglemin  33574  broutsideof2  33583  rngosubdi  35238  rngosubdir  35239  isdrngo2  35251  crngm23  35295  dmncan2  35370  latmassOLD  36380  latm32  36382  cvrnbtwn4  36430  cvrcmp2  36435  ltcvrntr  36575  atcvrj0  36579  3dim3  36620  paddasslem17  36987  paddass  36989  lautlt  37242  lautcvr  37243  lautj  37244  lautm  37245  erngdvlem3  38141  dvalveclem  38176  mendlmod  39842