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 1166	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  8360  mapfien2  9449  cfeq0  10296  ltmul2  12118  lemul1  12119  lemul2  12120  lemuldiv  12148  lediv2  12158  ltdiv23  12159  lediv23  12160  dvdscmulr  16322  dvdsmulcr  16323  modremain  16445  ndvdsadd  16447  rpexp12i  16761  isdrngd  20765  isdrngdOLD  20767  cramerimp  22692  tsmsxp  24163  xblcntrps  24420  xblcntr  24421  rrxmet  25442  nvaddsub4  30676  hvmulcan2  31092  adjlnop  32105  rrnmet  37836  lfladd  39067  lflsub  39068  lshpset2N  39120  atcvrj1  39433  athgt  39458  ltrncnvel  40144  trlcnv  40167  trljat2  40169  cdlemc5  40197  trlcoabs  40723  trlcolem  40728  dicvaddcl  41192  limsupre3uzlem  45750  fourierdlem42  46164  ovnhoilem2  46617  lincext3  48373