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

Theorem 3adant1r 1223
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 1202 1 (((𝜑𝜏) ∧ 𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  3adant2rOLD  1228  3adant3rOLD  1232  ecopovtrn  8054  isf32lem9  9436  axdc3lem4  9528  tskun  9861  dvdscmulr  15297  divalglem8  15407  ghmgrp  17808  quscrng  19514  dvfsumlem3  24082  dvfsumrlim  24085  dvfsumrlim2  24086  dvfsumrlim3  24087  dchrisumlem3  25471  dchrisum  25472  abvcxp  25595  padicabv  25610  hvmulcan  28320  isarchi2  30121  archiabllem2c  30131  hasheuni  30529  carsgclctunlem1  30761  carsggect  30762  carsgclctunlem2  30763  carsgclctunlem3  30764  carsgclctun  30765  carsgsiga  30766  omsmeas  30767  tendoicl  36684  cdlemkfid2N  36811  erngdvlem4  36879  pellex  38009  refsumcn  39773  restuni3  39883  wessf1ornlem  39950  unirnmapsn  39983  ssmapsn  39985  iunmapsn  39986  ssfiunibd  40094  supxrgelem  40123  infleinf2  40210  fmuldfeq  40385  limsupmnfuzlem  40528  limsupre3uzlem  40537  cosknegpi  40650  icccncfext  40670  stoweidlem31  40817  stoweidlem43  40829  stoweidlem46  40832  stoweidlem52  40838  stoweidlem53  40839  stoweidlem54  40840  stoweidlem55  40841  stoweidlem56  40842  stoweidlem57  40843  stoweidlem58  40844  stoweidlem59  40845  stoweidlem60  40846  stoweidlem62  40848  stoweid  40849  fourierdlem12  40905  fourierdlem41  40934  fourierdlem48  40940  fourierdlem79  40971  fourierdlem81  40973  etransclem24  41044  etransclem46  41066  sge0f1o  41168  sge0iunmptlemre  41201  sge0iunmpt  41204  sge0seq  41232  caragenfiiuncl  41301  hoicvr  41334  hoidmvval0  41373  hspmbllem2  41413  smflimsuplem7  41604  el0ldep  42856
  Copyright terms: Public domain W3C validator