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

Theorem mpd3an23 1423
 Description: An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.)
Hypotheses
Ref Expression
mpd3an23.1 (𝜑𝜓)
mpd3an23.2 (𝜑𝜒)
mpd3an23.3 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mpd3an23 (𝜑𝜃)

Proof of Theorem mpd3an23
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
2 mpd3an23.1 . 2 (𝜑𝜓)
3 mpd3an23.2 . 2 (𝜑𝜒)
4 mpd3an23.3 . 2 ((𝜑𝜓𝜒) → 𝜃)
51, 2, 3, 4syl3anc 1323 1 (𝜑𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1036 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 386  df-3an 1038 This theorem is referenced by:  rankcf  9559  bcpasc  13064  sqreulem  14049  qnumdencoprm  15396  qeqnumdivden  15397  xpsaddlem  16175  xpsvsca  16179  xpsle  16181  grpinvid  17416  qus0  17592  ghmid  17606  lsm01  18024  frgpadd  18116  abvneg  18774  lsmcv  19081  discmp  21141  kgenhaus  21287  idnghm  22487  xmetdcn2  22580  pi1addval  22788  ipcau2  22973  gausslemma2dlem1a  25024  2lgs  25066  uhgrsubgrself  26099  carsgclctunlem2  30204  carsgclctun  30206  ballotlem1ri  30419  ftc1anclem5  33160  opoc1  34008  opoc0  34009  dochsat  36191  lcfrlem9  36358  pellfundex  36969  0ellimcdiv  39317  add2cncf  39451  stoweidlem21  39575  stoweidlem23  39577  stoweidlem32  39586  stoweidlem36  39590  stoweidlem40  39594  stoweidlem41  39595  mod42tp1mod8  40848  lincval0  41522
 Copyright terms: Public domain W3C validator