MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adant1r Structured version   Visualization version   GIF version

Theorem 3adant1r 1174
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Hypothesis
Ref Expression
ad4ant3.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3adant1r (((𝜑𝜏) ∧ 𝜓𝜒) → 𝜃)

Proof of Theorem 3adant1r
StepHypRef Expression
1 simpl 486 . 2 ((𝜑𝜏) → 𝜑)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an1 1160 1 (((𝜑𝜏) ∧ 𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  ecopovtrn  8387  isf32lem9  9776  axdc3lem4  9868  tskun  10201  dvdscmulr  15634  divalglem8  15745  ghmgrp  18219  dvfsumlem3  24635  dvfsumrlim  24638  dvfsumrlim2  24639  dvfsumrlim3  24640  dchrisumlem3  26079  dchrisum  26080  abvcxp  26203  padicabv  26218  hvmulcan  28859  isarchi2  30868  archiabllem2c  30878  hasheuni  31458  carsgclctunlem1  31689  carsggect  31690  carsgclctunlem2  31691  carsgclctunlem3  31692  carsgclctun  31693  carsgsiga  31694  omsmeas  31695  pibt2  34835  tendoicl  38091  cdlemkfid2N  38218  erngdvlem4  38286  pellex  39769  refsumcn  41652  restuni3  41746  wessf1ornlem  41804  unirnmapsn  41836  ssmapsn  41838  iunmapsn  41839  ssfiunibd  41934  supxrgelem  41962  infleinf2  42044  fmuldfeq  42218  limsupmnfuzlem  42361  limsupre3uzlem  42370  cosknegpi  42504  icccncfext  42522  stoweidlem31  42666  stoweidlem43  42678  stoweidlem46  42681  stoweidlem52  42687  stoweidlem53  42688  stoweidlem54  42689  stoweidlem55  42690  stoweidlem56  42691  stoweidlem57  42692  stoweidlem58  42693  stoweidlem59  42694  stoweidlem60  42695  stoweidlem62  42697  stoweid  42698  fourierdlem12  42754  fourierdlem41  42783  fourierdlem48  42789  fourierdlem79  42820  fourierdlem81  42822  etransclem24  42893  etransclem46  42915  sge0f1o  43014  sge0iunmptlemre  43047  sge0iunmpt  43050  sge0seq  43078  caragenfiiuncl  43147  hoicvr  43180  hoidmvval0  43219  hspmbllem2  43259  smflimsuplem7  43450  el0ldep  44868  2arymaptfo  45061  itschlc0yqe  45167  itsclc0yqsol  45171
  Copyright terms: Public domain W3C validator