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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  mapfien2  9370  cfeq0  10241  ltmul2  12067  lemul1  12068  lemul2  12069  lemuldiv  12096  lediv2  12106  ltdiv23  12107  lediv23  12108  dvdscmulr  16343  dvdsmulcr  16344  modremain  16467  ndvdsadd  16469  rpexp12i  16784  isdrngd  20850  isdrngdOLD  20852  cramerimp  22824  tsmsxp  24293  xblcntrps  24548  xblcntr  24549  rrxmet  25548  nvaddsub4  30990  hvmulcan2  31406  adjlnop  32419  rrnmet  38461  lfladd  39821  lflsub  39822  lshpset2N  39874  atcvrj1  40186  athgt  40211  ltrncnvel  40897  trlcnv  40920  trljat2  40922  cdlemc5  40950  trlcoabs  41476  trlcolem  41481  dicvaddcl  41945  limsupre3uzlem  46432  fourierdlem42  46846  ovnhoilem2  47299  lincext3  49219