Theorem 3adant3r 1181

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  wfrlem12OLD  8322  mapfien2  9406  cfeq0  10253  ltmul2  12067  lemul1  12068  lemul2  12069  lemuldiv  12096  lediv2  12106  ltdiv23  12107  lediv23  12108  dvdscmulr  16230  dvdsmulcr  16231  modremain  16353  ndvdsadd  16355  rpexp12i  16663  isdrngd  20394  isdrngdOLD  20396  cramerimp  22195  tsmsxp  23666  xblcntrps  23923  xblcntr  23924  rrxmet  24932  nvaddsub4  29948  hvmulcan2  30364  adjlnop  31377  rrnmet  36783  lfladd  38022  lflsub  38023  lshpset2N  38075  atcvrj1  38388  athgt  38413  ltrncnvel  39099  trlcnv  39122  trljat2  39124  cdlemc5  39152  trlcoabs  39678  trlcolem  39683  dicvaddcl  40147  limsupre3uzlem  44530  fourierdlem42  44944  ovnhoilem2  45397  lincext3  47215