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

Theorem 3adant1r 1177
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 1163 1 (((𝜑𝜏) ∧ 𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 397  df-3an 1089
This theorem is referenced by:  ecopovtrn  8758  isf32lem9  10296  axdc3lem4  10388  tskun  10721  dvdscmulr  16166  divalglem8  16281  ghmgrp  18869  dvfsumlem3  25390  dvfsumrlim  25393  dvfsumrlim2  25394  dvfsumrlim3  25395  dchrisumlem3  26837  dchrisum  26838  abvcxp  26961  padicabv  26976  hvmulcan  29961  isarchi2  31965  archiabllem2c  31975  hasheuni  32624  carsgclctunlem1  32857  carsggect  32858  carsgclctunlem2  32859  carsgclctunlem3  32860  carsgclctun  32861  carsgsiga  32862  omsmeas  32863  pibt2  35878  tendoicl  39249  cdlemkfid2N  39376  erngdvlem4  39444  pellex  41135  refsumcn  43216  restuni3  43309  wessf1ornlem  43378  unirnmapsn  43410  ssmapsn  43412  iunmapsn  43413  ssfiunibd  43518  supxrgelem  43546  infleinf2  43624  fmuldfeq  43795  limsupmnfuzlem  43938  limsupre3uzlem  43947  cosknegpi  44081  icccncfext  44099  stoweidlem31  44243  stoweidlem43  44255  stoweidlem46  44258  stoweidlem52  44264  stoweidlem53  44265  stoweidlem54  44266  stoweidlem55  44267  stoweidlem56  44268  stoweidlem57  44269  stoweidlem58  44270  stoweidlem59  44271  stoweidlem60  44272  stoweidlem62  44274  stoweid  44275  fourierdlem12  44331  fourierdlem41  44360  fourierdlem48  44366  fourierdlem79  44397  fourierdlem81  44399  etransclem24  44470  etransclem46  44492  sge0f1o  44594  sge0iunmptlemre  44627  sge0iunmpt  44630  sge0seq  44658  caragenfiiuncl  44727  hoicvr  44760  hoidmvval0  44799  hspmbllem2  44839  smflimsuplem7  45038  el0ldep  46518  2arymaptfo  46711  itschlc0yqe  46817  itsclc0yqsol  46821
  Copyright terms: Public domain W3C validator