Theorem 3adant3r 1181

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

This theorem is referenced by:  wfrlem12OLD  8376  mapfien2  9478  cfeq0  10325  ltmul2  12145  lemul1  12146  lemul2  12147  lemuldiv  12175  lediv2  12185  ltdiv23  12186  lediv23  12187  dvdscmulr  16333  dvdsmulcr  16334  modremain  16456  ndvdsadd  16458  rpexp12i  16771  isdrngd  20787  isdrngdOLD  20789  cramerimp  22713  tsmsxp  24184  xblcntrps  24441  xblcntr  24442  rrxmet  25461  nvaddsub4  30689  hvmulcan2  31105  adjlnop  32118  rrnmet  37789  lfladd  39022  lflsub  39023  lshpset2N  39075  atcvrj1  39388  athgt  39413  ltrncnvel  40099  trlcnv  40122  trljat2  40124  cdlemc5  40152  trlcoabs  40678  trlcolem  40683  dicvaddcl  41147  limsupre3uzlem  45656  fourierdlem42  46070  ovnhoilem2  46523  lincext3  48185