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

Theorem mp3an23 1407
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
Hypotheses
Ref Expression
mp3an23.1 𝜓
mp3an23.2 𝜒
mp3an23.3 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an23 (𝜑𝜃)

Proof of Theorem mp3an23
StepHypRef Expression
1 mp3an23.1 . 2 𝜓
2 mp3an23.2 . . 3 𝜒
3 mp3an23.3 . . 3 ((𝜑𝜓𝜒) → 𝜃)
42, 3mp3an3 1404 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan2 702 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  sbciegf  3433  predeq1  5585  wrecseq1  7274  ac6sfi  8066  unfilem1  8086  ordtypelem2  8284  infxpenc2  8705  cda0en  8861  cfsmolem  8952  axdc4lem  9137  1nqenq  9640  mul02lem1  10063  muleqadd  10520  halfcl  11104  rehalfcl  11105  half0  11106  2halves  11107  halfpos2  11108  halfnneg2  11110  halfaddsub  11112  nneo  11293  zeo  11295  peano5uzi  11298  fztp  12222  uzrdgxfr  12583  bcn2  12923  bcpasc  12925  hashxplem  13032  hashfun  13036  swrds2  13479  repsw2  13487  repsw3  13488  imre  13642  reim  13643  crim  13649  addcj  13682  imval2  13685  cnpart  13774  sqrlem7  13783  absmax  13863  binomfallfaclem2  14556  bpoly2  14573  bpoly3  14574  fsumcube  14576  efgt0  14618  sinf  14639  efi4p  14652  resin4p  14653  recos4p  14654  sinneg  14661  efival  14667  cosadd  14680  sinmul  14687  sinbnd  14695  cosbnd  14696  ef01bndlem  14699  sin01bnd  14700  cos01bnd  14701  sin01gt0  14705  cos01gt0  14706  sin02gt0  14707  rpnnen2lem11  14738  rpnnen2lem12  14739  odd2np1lem  14848  odd2np1  14849  pythagtriplem12  15315  pythagtriplem14  15317  pythagtriplem15  15318  pythagtriplem16  15319  pythagtriplem17  15320  pockthi  15395  prmreclem5  15408  prmreclem6  15409  prmlem0  15596  prdsplusg  15887  prdsmulr  15888  prdsvsca  15889  odinf  17749  lbsexg  18931  psgnghm2  19691  mopnex  22075  tngnm  22203  tngngp2  22204  tngngpd  22205  tngngp  22206  addccncf  22458  iihalf1  22469  iihalf2  22471  pjthlem1  22933  ovolunlem1a  22988  ovolunlem1  22989  opnmbllem  23092  vitalilem4  23103  iblcnlem1  23277  itgcnlem  23279  dvmptre  23455  dvmptim  23456  dvlipcn  23478  mdegldg  23547  aaliou3lem3  23820  aaliou3lem8  23821  sincosq1lem  23970  sincosq2sgn  23972  sincosq3sgn  23973  sincosq4sgn  23974  sinq12gt0  23980  abssinper  23991  coskpi  23993  sineq0  23994  coseq1  23995  efeq1  23996  resinf1o  24003  efif1olem2  24010  efif1olem4  24012  logneg2  24082  cxpsqrtlem  24165  cxpsqrt  24166  logsqrt  24167  1cubr  24286  leibpilem1  24384  leibpilem2  24385  basellem3  24526  ppiub  24646  chtublem  24653  chtub  24654  bcmax  24720  bcp1ctr  24721  bposlem2  24727  bposlem6  24731  bposlem9  24734  logdivsum  24939  4ipval2  26748  4ipval3  26752  ipidsq  26753  dipcl  26755  dipcj  26757  ipasslem11  26885  hvmul0  27071  pjhthlem1  27440  h1de2bi  27603  spanunsni  27628  adjeu  27938  nmopge0  27960  nmfnge0  27976  opsqrlem6  28194  mdsl1i  28370  mdsl2bi  28372  mdexchi  28384  superpos  28403  atabsi  28450  dmdbr5ati  28471  cdj3lem1  28483  fpwrelmapffslem  28701  ogrpaddlt  28855  ofldlt1  28950  ofldchr  28951  oddpwdc  29549  eulerpartgbij  29567  subfacp1lem2a  30222  subfacp1lem5  30226  subfacp1lem6  30227  subfaclim  30230  sinccvglem  30626  dfon2lem3  30740  dfon2lem7  30744  wsuceq1  30811  clsun  31299  vtoclefex  32153  finxpreclem5  32204  sin2h  32365  cos2h  32366  tan2h  32367  poimirlem22  32397  poimirlem31  32406  opnmbllem0  32411  mblfinlem3  32414  itg2addnclem3  32429  ftc1cnnclem  32449  ftc1anclem6  32456  ftc2nc  32460  dvasin  32462  fdc  32507  constcncf  32524  sub1cncf  32526  sub2cncf  32527  heiborlem7  32582  atlatmstc  33420  diophren  36191  dftrcl3  36827  dfrtrcl3  36840  cotrclrcl  36849  lhe4.4ex1a  37346  dirkerper  38786  upgr1wlkcompim  40846  upgrtrls  40904  upgrspths1wlk  40939  zlmodzxznm  42075  sinh-conventional  42235  dp2cl  42265  dpfrac1  42268  dpfrac1OLD  42269
  Copyright terms: Public domain W3C validator