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

Theorem mpd3an23 1418
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 1318 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  rankcf  9478  bcpasc  12970  sqreulem  13947  qnumdencoprm  15291  qeqnumdivden  15292  xpsaddlem  16058  xpsvsca  16062  xpsle  16064  grpinvid  17299  qus0  17475  ghmid  17489  lsm01  17907  frgpadd  17999  abvneg  18657  lsmcv  18962  discmp  21011  kgenhaus  21157  idnghm  22357  xmetdcn2  22448  pi1addval  22656  ipcau2  22841  gausslemma2dlem1a  24890  2lgs  24932  carsgclctunlem2  29708  carsgclctun  29710  ballotlem1ri  29923  ftc1anclem5  32659  opoc1  33507  opoc0  33508  dochsat  35690  lcfrlem9  35857  pellfundex  36468  0ellimcdiv  38716  add2cncf  38789  stoweidlem21  38914  stoweidlem23  38916  stoweidlem32  38925  stoweidlem36  38929  stoweidlem40  38933  stoweidlem41  38934  mod42tp1mod8  40057  uhgrsubgrself  40504  lincval0  41998
  Copyright terms: Public domain W3C validator