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  9360  cfeq0  10209  ltmul2  12033  lemul1  12034  lemul2  12035  lemuldiv  12063  lediv2  12073  ltdiv23  12074  lediv23  12075  dvdscmulr  16254  dvdsmulcr  16255  modremain  16378  ndvdsadd  16380  rpexp12i  16694  isdrngd  20674  isdrngdOLD  20676  cramerimp  22573  tsmsxp  24042  xblcntrps  24298  xblcntr  24299  rrxmet  25308  nvaddsub4  30586  hvmulcan2  31002  adjlnop  32015  rrnmet  37823  lfladd  39059  lflsub  39060  lshpset2N  39112  atcvrj1  39425  athgt  39450  ltrncnvel  40136  trlcnv  40159  trljat2  40161  cdlemc5  40189  trlcoabs  40715  trlcolem  40720  dicvaddcl  41184  limsupre3uzlem  45733  fourierdlem42  46147  ovnhoilem2  46600  lincext3  48445