Theorem 3adant3r 1182

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 1165	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:  mapfien2  9312  cfeq0  10166  ltmul2  11992  lemul1  11993  lemul2  11994  lemuldiv  12022  lediv2  12032  ltdiv23  12033  lediv23  12034  dvdscmulr  16211  dvdsmulcr  16212  modremain  16335  ndvdsadd  16337  rpexp12i  16651  isdrngd  20698  isdrngdOLD  20700  cramerimp  22630  tsmsxp  24099  xblcntrps  24354  xblcntr  24355  rrxmet  25364  nvaddsub4  30732  hvmulcan2  31148  adjlnop  32161  rrnmet  38030  lfladd  39326  lflsub  39327  lshpset2N  39379  atcvrj1  39691  athgt  39716  ltrncnvel  40402  trlcnv  40425  trljat2  40427  cdlemc5  40455  trlcoabs  40981  trlcolem  40986  dicvaddcl  41450  limsupre3uzlem  45979  fourierdlem42  46393  ovnhoilem2  46846  lincext3  48702