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

Theorem mpd3an23 1460
 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 1368 1 (𝜑𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  rankcf  10237  bcpasc  13731  sqreulem  14767  qnumdencoprm  16140  qeqnumdivden  16141  xpsaddlem  16904  xpsvsca  16908  xpsle  16910  grpinvid  18227  qus0  18405  ghmid  18431  lsm01  18864  frgpadd  18956  abvneg  19673  lsmcv  19981  discmp  22098  kgenhaus  22244  idnghm  23445  xmetdcn2  23538  pi1addval  23749  ipcau2  23934  gausslemma2dlem1a  26048  2lgs  26090  uhgrsubgrself  27169  wlkl0  28251  carsgclctunlem2  31805  carsgclctun  31807  ballotlem1ri  32020  satefvfmla0  32896  satefvfmla1  32903  etasslt2  33569  ftc1anclem5  35414  opoc1  36778  opoc0  36779  dochsat  38959  lcfrlem9  39126  pellfundex  40200  mnringmulrcld  41309  0ellimcdiv  42657  add2cncf  42910  stoweidlem21  43029  stoweidlem23  43031  stoweidlem32  43040  stoweidlem36  43044  stoweidlem40  43048  stoweidlem41  43049  mod42tp1mod8  44487  lincval0  45189
 Copyright terms: Public domain W3C validator