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

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

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 1090

This theorem is referenced by:  wfrlem12  7995  mapfien2  8946  cfeq0  9756  ltmul2  11569  lemul1  11570  lemul2  11571  lemuldiv  11598  lediv2  11608  ltdiv23  11609  lediv23  11610  dvdscmulr  15730  dvdsmulcr  15731  modremain  15853  ndvdsadd  15855  rpexp12i  16165  isdrngd  19646  cramerimp  21437  tsmsxp  22906  xblcntrps  23163  xblcntr  23164  rrxmet  24160  nvaddsub4  28592  hvmulcan2  29008  adjlnop  30021  rrnmet  35610  lfladd  36703  lflsub  36704  lshpset2N  36756  atcvrj1  37068  athgt  37093  ltrncnvel  37779  trlcnv  37802  trljat2  37804  cdlemc5  37832  trlcoabs  38358  trlcolem  38363  dicvaddcl  38827  limsupre3uzlem  42818  fourierdlem42  43232  ovnhoilem2  43682  lincext3  45331