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  9322  cfeq0  10178  ltmul2  12006  lemul1  12007  lemul2  12008  lemuldiv  12036  lediv2  12046  ltdiv23  12047  lediv23  12048  dvdscmulr  16253  dvdsmulcr  16254  modremain  16377  ndvdsadd  16379  rpexp12i  16694  isdrngd  20742  isdrngdOLD  20744  cramerimp  22651  tsmsxp  24120  xblcntrps  24375  xblcntr  24376  rrxmet  25375  nvaddsub4  30728  hvmulcan2  31144  adjlnop  32157  rrnmet  38150  lfladd  39512  lflsub  39513  lshpset2N  39565  atcvrj1  39877  athgt  39902  ltrncnvel  40588  trlcnv  40611  trljat2  40613  cdlemc5  40641  trlcoabs  41167  trlcolem  41172  dicvaddcl  41636  limsupre3uzlem  46163  fourierdlem42  46577  ovnhoilem2  47030  lincext3  48932