Theorem 3adant3r 1178

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  wfrlem12  7949  mapfien2  8856  cfeq0  9667  ltmul2  11480  lemul1  11481  lemul2  11482  lemuldiv  11509  lediv2  11519  ltdiv23  11520  lediv23  11521  dvdscmulr  15630  dvdsmulcr  15631  modremain  15749  ndvdsadd  15751  rpexp12i  16056  isdrngd  19520  cramerimp  21291  tsmsxp  22760  xblcntrps  23017  xblcntr  23018  rrxmet  24012  nvaddsub4  28440  hvmulcan2  28856  adjlnop  29869  rrnmet  35267  lfladd  36362  lflsub  36363  lshpset2N  36415  atcvrj1  36727  athgt  36752  ltrncnvel  37438  trlcnv  37461  trljat2  37463  cdlemc5  37491  trlcoabs  38017  trlcolem  38022  dicvaddcl  38486  limsupre3uzlem  42377  fourierdlem42  42791  ovnhoilem2  43241  lincext3  44865