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

Theorem 3adant1r 1178
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 484 . 2 ((𝜑𝜏) → 𝜑)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an1 1164 1 (((𝜑𝜏) ∧ 𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  ecopovtrn  8762  isf32lem9  10302  axdc3lem4  10394  tskun  10727  dvdscmulr  16172  divalglem8  16287  ghmgrp  18876  dvfsumlem3  25408  dvfsumrlim  25411  dvfsumrlim2  25412  dvfsumrlim3  25413  dchrisumlem3  26855  dchrisum  26856  abvcxp  26979  padicabv  26994  hvmulcan  30056  isarchi2  32070  archiabllem2c  32080  hasheuni  32741  carsgclctunlem1  32974  carsggect  32975  carsgclctunlem2  32976  carsgclctunlem3  32977  carsgclctun  32978  carsgsiga  32979  omsmeas  32980  pibt2  35934  tendoicl  39305  cdlemkfid2N  39432  erngdvlem4  39500  pellex  41201  refsumcn  43323  restuni3  43416  wessf1ornlem  43491  unirnmapsn  43522  ssmapsn  43524  iunmapsn  43525  ssfiunibd  43630  supxrgelem  43658  infleinf2  43735  fmuldfeq  43910  limsupmnfuzlem  44053  limsupre3uzlem  44062  cosknegpi  44196  icccncfext  44214  stoweidlem31  44358  stoweidlem43  44370  stoweidlem46  44373  stoweidlem52  44379  stoweidlem53  44380  stoweidlem54  44381  stoweidlem55  44382  stoweidlem56  44383  stoweidlem57  44384  stoweidlem58  44385  stoweidlem59  44386  stoweidlem60  44387  stoweidlem62  44389  stoweid  44390  fourierdlem12  44446  fourierdlem41  44475  fourierdlem48  44481  fourierdlem79  44512  fourierdlem81  44514  etransclem24  44585  etransclem46  44607  sge0f1o  44709  sge0iunmptlemre  44742  sge0iunmpt  44745  sge0seq  44773  caragenfiiuncl  44842  hoicvr  44875  hoidmvval0  44914  hspmbllem2  44954  smflimsuplem7  45153  el0ldep  46633  2arymaptfo  46826  itschlc0yqe  46932  itsclc0yqsol  46936
  Copyright terms: Public domain W3C validator