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  9438  cfeq0  10373  ltmul2  12208  lemul1  12209  lemul2  12210  lemuldiv  12237  lediv2  12247  ltdiv23  12248  lediv23  12249  dvdscmulr  16498  dvdsmulcr  16499  modremain  16622  ndvdsadd  16624  rpexp12i  16944  isdrngd  21073  isdrngdOLD  21075  cramerimp  23059  tsmsxp  24529  xblcntrps  24784  xblcntr  24785  rrxmet  25784  nvaddsub4  31316  hvmulcan2  31732  adjlnop  32745  rrnmet  39029  lfladd  40389  lflsub  40390  lshpset2N  40442  atcvrj1  40754  athgt  40779  ltrncnvel  41465  trlcnv  41488  trljat2  41490  cdlemc5  41518  trlcoabs  42044  trlcolem  42049  dicvaddcl  42513  limsupre3uzlem  47018  fourierdlem42  47432  ovnhoilem2  47885  lincext3  49899