Theorem 3adant3r 1183

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

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

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 1089

This theorem is referenced by:  mapfien2  9315  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  20733  isdrngdOLD  20735  cramerimp  22661  tsmsxp  24130  xblcntrps  24385  xblcntr  24386  rrxmet  25385  nvaddsub4  30743  hvmulcan2  31159  adjlnop  32172  rrnmet  38164  lfladd  39526  lflsub  39527  lshpset2N  39579  atcvrj1  39891  athgt  39916  ltrncnvel  40602  trlcnv  40625  trljat2  40627  cdlemc5  40655  trlcoabs  41181  trlcolem  41186  dicvaddcl  41650  limsupre3uzlem  46181  fourierdlem42  46595  ovnhoilem2  47048  lincext3  48944