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  9336  cfeq0  10185  ltmul2  12009  lemul1  12010  lemul2  12011  lemuldiv  12039  lediv2  12049  ltdiv23  12050  lediv23  12051  dvdscmulr  16230  dvdsmulcr  16231  modremain  16354  ndvdsadd  16356  rpexp12i  16670  isdrngd  20650  isdrngdOLD  20652  cramerimp  22549  tsmsxp  24018  xblcntrps  24274  xblcntr  24275  rrxmet  25284  nvaddsub4  30559  hvmulcan2  30975  adjlnop  31988  rrnmet  37796  lfladd  39032  lflsub  39033  lshpset2N  39085  atcvrj1  39398  athgt  39423  ltrncnvel  40109  trlcnv  40132  trljat2  40134  cdlemc5  40162  trlcoabs  40688  trlcolem  40693  dicvaddcl  41157  limsupre3uzlem  45706  fourierdlem42  46120  ovnhoilem2  46573  lincext3  48418