Theorem 3adant3r 1182

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

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

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

This theorem is referenced by:  wfrlem12OLD  8334  mapfien2  9421  cfeq0  10270  ltmul2  12092  lemul1  12093  lemul2  12094  lemuldiv  12122  lediv2  12132  ltdiv23  12133  lediv23  12134  dvdscmulr  16304  dvdsmulcr  16305  modremain  16427  ndvdsadd  16429  rpexp12i  16743  isdrngd  20725  isdrngdOLD  20727  cramerimp  22624  tsmsxp  24093  xblcntrps  24349  xblcntr  24350  rrxmet  25360  nvaddsub4  30638  hvmulcan2  31054  adjlnop  32067  rrnmet  37853  lfladd  39084  lflsub  39085  lshpset2N  39137  atcvrj1  39450  athgt  39475  ltrncnvel  40161  trlcnv  40184  trljat2  40186  cdlemc5  40214  trlcoabs  40740  trlcolem  40745  dicvaddcl  41209  limsupre3uzlem  45764  fourierdlem42  46178  ovnhoilem2  46631  lincext3  48432