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  9367  cfeq0  10216  ltmul2  12040  lemul1  12041  lemul2  12042  lemuldiv  12070  lediv2  12080  ltdiv23  12081  lediv23  12082  dvdscmulr  16261  dvdsmulcr  16262  modremain  16385  ndvdsadd  16387  rpexp12i  16701  isdrngd  20681  isdrngdOLD  20683  cramerimp  22580  tsmsxp  24049  xblcntrps  24305  xblcntr  24306  rrxmet  25315  nvaddsub4  30593  hvmulcan2  31009  adjlnop  32022  rrnmet  37830  lfladd  39066  lflsub  39067  lshpset2N  39119  atcvrj1  39432  athgt  39457  ltrncnvel  40143  trlcnv  40166  trljat2  40168  cdlemc5  40196  trlcoabs  40722  trlcolem  40727  dicvaddcl  41191  limsupre3uzlem  45740  fourierdlem42  46154  ovnhoilem2  46607  lincext3  48449