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

Theorem 3adant1r 1169
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 483 . 2 ((𝜑𝜏) → 𝜑)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an1 1155 1 (((𝜑𝜏) ∧ 𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  ecopovtrn  8389  isf32lem9  9771  axdc3lem4  9863  tskun  10196  dvdscmulr  15626  divalglem8  15739  ghmgrp  18161  dvfsumlem3  24552  dvfsumrlim  24555  dvfsumrlim2  24556  dvfsumrlim3  24557  dchrisumlem3  25994  dchrisum  25995  abvcxp  26118  padicabv  26133  hvmulcan  28776  isarchi2  30741  archiabllem2c  30751  hasheuni  31243  carsgclctunlem1  31474  carsggect  31475  carsgclctunlem2  31476  carsgclctunlem3  31477  carsgclctun  31478  carsgsiga  31479  omsmeas  31480  pibt2  34580  tendoicl  37812  cdlemkfid2N  37939  erngdvlem4  38007  pellex  39310  refsumcn  41164  restuni3  41261  wessf1ornlem  41321  unirnmapsn  41353  ssmapsn  41355  iunmapsn  41356  ssfiunibd  41452  supxrgelem  41481  infleinf2  41564  fmuldfeq  41740  limsupmnfuzlem  41883  limsupre3uzlem  41892  cosknegpi  42026  icccncfext  42046  stoweidlem31  42193  stoweidlem43  42205  stoweidlem46  42208  stoweidlem52  42214  stoweidlem53  42215  stoweidlem54  42216  stoweidlem55  42217  stoweidlem56  42218  stoweidlem57  42219  stoweidlem58  42220  stoweidlem59  42221  stoweidlem60  42222  stoweidlem62  42224  stoweid  42225  fourierdlem12  42281  fourierdlem41  42310  fourierdlem48  42316  fourierdlem79  42347  fourierdlem81  42349  etransclem24  42420  etransclem46  42442  sge0f1o  42541  sge0iunmptlemre  42574  sge0iunmpt  42577  sge0seq  42605  caragenfiiuncl  42674  hoicvr  42707  hoidmvval0  42746  hspmbllem2  42786  smflimsuplem7  42977  el0ldep  44449  itschlc0yqe  44675  itsclc0yqsol  44679
  Copyright terms: Public domain W3C validator