Theorem 3adant3r 1178

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)

Hypothesis

Ref	Expression
ad4ant3.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant3r	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3adant3r

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an3 1162	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084

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 396  df-3an 1086

This theorem is referenced by:  wfrlem12OLD  8315  mapfien2  9400  cfeq0  10247  ltmul2  12062  lemul1  12063  lemul2  12064  lemuldiv  12091  lediv2  12101  ltdiv23  12102  lediv23  12103  dvdscmulr  16225  dvdsmulcr  16226  modremain  16348  ndvdsadd  16350  rpexp12i  16659  isdrngd  20610  isdrngdOLD  20612  cramerimp  22510  tsmsxp  23981  xblcntrps  24238  xblcntr  24239  rrxmet  25258  nvaddsub4  30379  hvmulcan2  30795  adjlnop  31808  rrnmet  37187  lfladd  38426  lflsub  38427  lshpset2N  38479  atcvrj1  38792  athgt  38817  ltrncnvel  39503  trlcnv  39526  trljat2  39528  cdlemc5  39556  trlcoabs  40082  trlcolem  40087  dicvaddcl  40551  limsupre3uzlem  44936  fourierdlem42  45350  ovnhoilem2  45803  lincext3  47325