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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  mapfien2  9304  cfeq0  10158  ltmul2  11983  lemul1  11984  lemul2  11985  lemuldiv  12013  lediv2  12023  ltdiv23  12024  lediv23  12025  dvdscmulr  16202  dvdsmulcr  16203  modremain  16326  ndvdsadd  16328  rpexp12i  16642  isdrngd  20689  isdrngdOLD  20691  cramerimp  22621  tsmsxp  24090  xblcntrps  24345  xblcntr  24346  rrxmet  25355  nvaddsub4  30658  hvmulcan2  31074  adjlnop  32087  rrnmet  37942  lfladd  39238  lflsub  39239  lshpset2N  39291  atcvrj1  39603  athgt  39628  ltrncnvel  40314  trlcnv  40337  trljat2  40339  cdlemc5  40367  trlcoabs  40893  trlcolem  40898  dicvaddcl  41362  limsupre3uzlem  45895  fourierdlem42  46309  ovnhoilem2  46762  lincext3  48618