Theorem 3adant3r 1198

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 1181	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)

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

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 1103

This theorem is referenced by:  mapfien2  9365  cfeq0  10236  ltmul2  12062  lemul1  12063  lemul2  12064  lemuldiv  12091  lediv2  12101  ltdiv23  12102  lediv23  12103  dvdscmulr  16338  dvdsmulcr  16339  modremain  16462  ndvdsadd  16464  rpexp12i  16779  isdrngd  20843  isdrngdOLD  20845  cramerimp  22808  tsmsxp  24277  xblcntrps  24532  xblcntr  24533  rrxmet  25532  nvaddsub4  30946  hvmulcan2  31362  adjlnop  32375  rrnmet  38363  lfladd  39725  lflsub  39726  lshpset2N  39778  atcvrj1  40090  athgt  40115  ltrncnvel  40801  trlcnv  40824  trljat2  40826  cdlemc5  40854  trlcoabs  41380  trlcolem  41385  dicvaddcl  41849  limsupre3uzlem  46334  fourierdlem42  46748  ovnhoilem2  47201  lincext3  49114