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  9318  cfeq0  10169  ltmul2  11993  lemul1  11994  lemul2  11995  lemuldiv  12023  lediv2  12033  ltdiv23  12034  lediv23  12035  dvdscmulr  16213  dvdsmulcr  16214  modremain  16337  ndvdsadd  16339  rpexp12i  16653  isdrngd  20668  isdrngdOLD  20670  cramerimp  22589  tsmsxp  24058  xblcntrps  24314  xblcntr  24315  rrxmet  25324  nvaddsub4  30619  hvmulcan2  31035  adjlnop  32048  rrnmet  37811  lfladd  39047  lflsub  39048  lshpset2N  39100  atcvrj1  39413  athgt  39438  ltrncnvel  40124  trlcnv  40147  trljat2  40149  cdlemc5  40177  trlcoabs  40703  trlcolem  40708  dicvaddcl  41172  limsupre3uzlem  45720  fourierdlem42  46134  ovnhoilem2  46587  lincext3  48445