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

Theorem mpd3an23 1454
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 1363 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  rankcf  10187  bcpasc  13669  sqreulem  14707  qnumdencoprm  16073  qeqnumdivden  16074  xpsaddlem  16834  xpsvsca  16838  xpsle  16840  grpinvid  18098  qus0  18276  ghmid  18302  lsm01  18726  frgpadd  18818  abvneg  19534  lsmcv  19842  discmp  21934  kgenhaus  22080  idnghm  23279  xmetdcn2  23372  pi1addval  23579  ipcau2  23764  gausslemma2dlem1a  25868  2lgs  25910  uhgrsubgrself  26989  wlkl0  28073  carsgclctunlem2  31476  carsgclctun  31478  ballotlem1ri  31691  satefvfmla0  32562  satefvfmla1  32569  ftc1anclem5  34852  opoc1  36218  opoc0  36219  dochsat  38399  lcfrlem9  38566  relt0neg1  39122  pellfundex  39361  0ellimcdiv  41806  add2cncf  42062  stoweidlem21  42183  stoweidlem23  42185  stoweidlem32  42194  stoweidlem36  42198  stoweidlem40  42202  stoweidlem41  42203  mod42tp1mod8  43644  lincval0  44398
  Copyright terms: Public domain W3C validator