Theorem 3adant3r 1188

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 483	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an3 1171	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  mapfien2  9312  cfeq0  10169  ltmul2  11997  lemul1  11998  lemul2  11999  lemuldiv  12027  lediv2  12037  ltdiv23  12038  lediv23  12039  dvdscmulr  16244  dvdsmulcr  16245  modremain  16368  ndvdsadd  16370  rpexp12i  16685  isdrngd  20737  isdrngdOLD  20739  cramerimp  22669  tsmsxp  24138  xblcntrps  24393  xblcntr  24394  rrxmet  25393  nvaddsub4  30746  hvmulcan2  31162  adjlnop  32175  rrnmet  38196  lfladd  39558  lflsub  39559  lshpset2N  39611  atcvrj1  39923  athgt  39948  ltrncnvel  40634  trlcnv  40657  trljat2  40659  cdlemc5  40687  trlcoabs  41213  trlcolem  41218  dicvaddcl  41682  limsupre3uzlem  46178  fourierdlem42  46592  ovnhoilem2  47045  lincext3  48947