Theorem 3adant3r 1194

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  mapfien2  9349  cfeq0  10207  ltmul2  12036  lemul1  12037  lemul2  12038  lemuldiv  12066  lediv2  12076  ltdiv23  12077  lediv23  12078  dvdscmulr  16309  dvdsmulcr  16310  modremain  16433  ndvdsadd  16435  rpexp12i  16750  isdrngd  20802  isdrngdOLD  20804  cramerimp  22734  tsmsxp  24203  xblcntrps  24458  xblcntr  24459  rrxmet  25458  nvaddsub4  30817  hvmulcan2  31233  adjlnop  32246  rrnmet  38289  lfladd  39651  lflsub  39652  lshpset2N  39704  atcvrj1  40016  athgt  40041  ltrncnvel  40727  trlcnv  40750  trljat2  40752  cdlemc5  40780  trlcoabs  41306  trlcolem  41311  dicvaddcl  41775  limsupre3uzlem  46270  fourierdlem42  46684  ovnhoilem2  47137  lincext3  49039