Theorem 3adant3r 1180

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 1164	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:  wfrlem12OLD  8359  mapfien2  9447  cfeq0  10294  ltmul2  12116  lemul1  12117  lemul2  12118  lemuldiv  12146  lediv2  12156  ltdiv23  12157  lediv23  12158  dvdscmulr  16319  dvdsmulcr  16320  modremain  16442  ndvdsadd  16444  rpexp12i  16758  isdrngd  20782  isdrngdOLD  20784  cramerimp  22708  tsmsxp  24179  xblcntrps  24436  xblcntr  24437  rrxmet  25456  nvaddsub4  30686  hvmulcan2  31102  adjlnop  32115  rrnmet  37816  lfladd  39048  lflsub  39049  lshpset2N  39101  atcvrj1  39414  athgt  39439  ltrncnvel  40125  trlcnv  40148  trljat2  40150  cdlemc5  40178  trlcoabs  40704  trlcolem  40709  dicvaddcl  41173  limsupre3uzlem  45691  fourierdlem42  46105  ovnhoilem2  46558  lincext3  48302