Theorem 3adant3r 1200

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 488	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an3 1183	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mapfien2  9379  cfeq0  10258  ltmul2  12090  lemul1  12091  lemul2  12092  lemuldiv  12119  lediv2  12129  ltdiv23  12130  lediv23  12131  dvdscmulr  16374  dvdsmulcr  16375  modremain  16498  ndvdsadd  16500  rpexp12i  16815  isdrngd  20931  isdrngdOLD  20933  cramerimp  22911  tsmsxp  24381  xblcntrps  24636  xblcntr  24637  rrxmet  25636  nvaddsub4  31138  hvmulcan2  31554  adjlnop  32567  rrnmet  38579  lfladd  39939  lflsub  39940  lshpset2N  39992  atcvrj1  40304  athgt  40329  ltrncnvel  41015  trlcnv  41038  trljat2  41040  cdlemc5  41068  trlcoabs  41594  trlcolem  41599  dicvaddcl  42063  limsupre3uzlem  46563  fourierdlem42  46977  ovnhoilem2  47430  lincext3  49386