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

Theorem 3adant1r 1188
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 474 . 2 ((𝜑𝜏) → 𝜑)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an1 1167 1 (((𝜑𝜏) ∧ 𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  3adant2rOLD  1193  3adant3rOLD  1197  ecopovtrn  8019  isf32lem9  9395  axdc3lem4  9487  tskun  9820  dvdscmulr  15232  divalglem8  15345  ghmgrp  17760  quscrng  19462  dvfsumlem3  24010  dvfsumrlim  24013  dvfsumrlim2  24014  dvfsumrlim3  24015  dchrisumlem3  25400  dchrisum  25401  abvcxp  25524  padicabv  25539  hvmulcan  28259  isarchi2  30069  archiabllem2c  30079  hasheuni  30477  carsgclctunlem1  30709  carsggect  30710  carsgclctunlem2  30711  carsgclctunlem3  30712  carsgclctun  30713  carsgsiga  30714  omsmeas  30715  tendoicl  36604  cdlemkfid2N  36731  erngdvlem4  36799  pellex  37919  refsumcn  39706  restuni3  39818  wessf1ornlem  39888  unirnmapsn  39923  ssmapsn  39925  iunmapsn  39926  ssfiunibd  40040  supxrgelem  40069  infleinf2  40157  fmuldfeq  40336  limsupmnfuzlem  40479  limsupre3uzlem  40488  cosknegpi  40601  icccncfext  40621  stoweidlem31  40769  stoweidlem43  40781  stoweidlem46  40784  stoweidlem52  40790  stoweidlem53  40791  stoweidlem54  40792  stoweidlem55  40793  stoweidlem56  40794  stoweidlem57  40795  stoweidlem58  40796  stoweidlem59  40797  stoweidlem60  40798  stoweidlem62  40800  stoweid  40801  fourierdlem12  40857  fourierdlem41  40886  fourierdlem48  40892  fourierdlem79  40923  fourierdlem81  40925  etransclem24  40996  etransclem46  41018  sge0f1o  41120  sge0iunmptlemre  41153  sge0iunmpt  41156  sge0seq  41184  caragenfiiuncl  41253  hoicvr  41286  hoidmvval0  41325  hspmbllem2  41365  smflimsuplem7  41556  el0ldep  42783
  Copyright terms: Public domain W3C validator