Theorem 3adant3r1 1182

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

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

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

This theorem is referenced by:  dif1en  9111  ccatswrd  14568  plttr  18245  pltletr  18246  latjlej1  18356  latjlej2  18357  latnlej  18359  latnlej2  18362  latmlem2  18373  latledi  18380  latjass  18386  latj32  18388  latj13  18389  ipopos  18439  tsrlemax  18489  imasmnd2  18607  grpsubsub  18850  grpnnncan2  18858  imasgrp2  18876  mulgnn0ass  18926  mulgsubdir  18930  cmn32  19596  ablsubadd  19604  imasring  20059  zntoslem  21000  xmettri3  23743  mettri3  23744  xmetrtri  23745  xmetrtri2  23746  metrtri  23747  cphdivcl  24583  cphassr  24613  relogbmulexp  26165  grpodivdiv  29545  grpomuldivass  29546  ablo32  29554  ablodivdiv4  29559  ablodiv32  29560  nvmdi  29653  dipdi  29848  dipassr  29851  dipsubdir  29853  dipsubdi  29854  dvrcan5  32141  cgr3tr4  34713  cgr3rflx  34715  endofsegid  34746  seglemin  34774  broutsideof2  34783  rngosubdi  36477  rngosubdir  36478  isdrngo2  36490  crngm23  36534  dmncan2  36609  latmassOLD  37764  latm32  37766  cvrnbtwn4  37814  cvrcmp2  37819  ltcvrntr  37960  atcvrj0  37964  3dim3  38005  paddasslem17  38372  paddass  38374  lautlt  38627  lautcvr  38628  lautj  38629  lautm  38630  erngdvlem3  39526  dvalveclem  39561  isdomn4  40697  mendlmod  41578