Theorem 3adant3r 1179

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 1163	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  wfrlem12OLD  8122  mapfien2  9098  cfeq0  9943  ltmul2  11756  lemul1  11757  lemul2  11758  lemuldiv  11785  lediv2  11795  ltdiv23  11796  lediv23  11797  dvdscmulr  15922  dvdsmulcr  15923  modremain  16045  ndvdsadd  16047  rpexp12i  16357  isdrngd  19931  cramerimp  21743  tsmsxp  23214  xblcntrps  23471  xblcntr  23472  rrxmet  24477  nvaddsub4  28920  hvmulcan2  29336  adjlnop  30349  rrnmet  35914  lfladd  37007  lflsub  37008  lshpset2N  37060  atcvrj1  37372  athgt  37397  ltrncnvel  38083  trlcnv  38106  trljat2  38108  cdlemc5  38136  trlcoabs  38662  trlcolem  38667  dicvaddcl  39131  limsupre3uzlem  43166  fourierdlem42  43580  ovnhoilem2  44030  lincext3  45685