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

Theorem mpd3an23 1567
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 1473 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  rankcf  9783  bcpasc  13294  sqreulem  14290  qnumdencoprm  15647  qeqnumdivden  15648  xpsaddlem  16429  xpsvsca  16433  xpsle  16435  grpinvid  17669  qus0  17845  ghmid  17859  lsm01  18276  frgpadd  18368  abvneg  19028  lsmcv  19335  discmp  21395  kgenhaus  21541  idnghm  22740  xmetdcn2  22833  pi1addval  23040  ipcau2  23225  gausslemma2dlem1a  25281  2lgs  25323  uhgrsubgrself  26363  wlkl0  27520  carsgclctunlem2  30682  carsgclctun  30684  ballotlem1ri  30897  ftc1anclem5  33794  opoc1  34984  opoc0  34985  dochsat  37166  lcfrlem9  37333  pellfundex  37944  0ellimcdiv  40376  add2cncf  40611  stoweidlem21  40733  stoweidlem23  40735  stoweidlem32  40744  stoweidlem36  40748  stoweidlem40  40752  stoweidlem41  40753  mod42tp1mod8  42021  lincval0  42706
  Copyright terms: Public domain W3C validator