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

Theorem mp3an23 1454
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 1451 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan2 690 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  sbciegf  3779  predeq1  6256  wrecseq1  8250  ac6sfi  9234  unfilem1  9257  ordtypelem2  9460  infxpenc2  9963  dju0en  10116  cfsmolem  10211  axdc4lem  10396  1nqenq  10903  mul02lem1  11336  muleqadd  11804  halfcl  12383  rehalfcl  12384  half0  12385  2halves  12386  halfpos2  12387  halfnneg2  12389  halfaddsub  12391  nneo  12592  zeo  12594  peano5uzi  12597  fztp  13503  uzrdgxfr  13878  bcn2  14225  bcpasc  14227  hashxplem  14339  hashfun  14343  swrds2  14835  repsw2  14845  repsw3  14846  imre  14999  reim  15000  crim  15006  addcj  15039  imval2  15042  cnpart  15131  01sqrexlem7  15139  absmax  15220  binomfallfaclem2  15928  bpoly2  15945  bpoly3  15946  fsumcube  15948  efgt0  15990  sinf  16011  efi4p  16024  resin4p  16025  recos4p  16026  sinneg  16033  efival  16039  cosadd  16052  sinmul  16059  sinbnd  16067  cosbnd  16068  ef01bndlem  16071  sin01bnd  16072  cos01bnd  16073  sin01gt0  16077  cos01gt0  16078  sin02gt0  16079  rpnnen2lem11  16111  rpnnen2lem12  16112  odd2np1lem  16227  odd2np1  16228  pythagtriplem12  16703  pythagtriplem14  16705  pythagtriplem15  16706  pythagtriplem16  16707  pythagtriplem17  16708  pockthi  16784  prmreclem5  16797  prmreclem6  16798  prmlem0  16983  prdsplusg  17345  prdsmulr  17346  prdsvsca  17347  odinf  19350  lbsexg  20641  psgnghm2  21001  mopnex  23891  tngnm  24031  tngngp2  24032  tngngpd  24033  tngngp  24034  addccncf  24296  sub1cncf  24298  sub2cncf  24299  iihalf1  24310  iihalf2  24312  pjthlem1  24817  ovolunlem1a  24876  ovolunlem1  24877  opnmbllem  24981  vitalilem4  24991  iblcnlem1  25168  itgcnlem  25170  dvmptre  25349  dvmptim  25350  dvlipcn  25374  mdegldg  25447  aaliou3lem3  25720  aaliou3lem8  25721  sincosq1lem  25870  sincosq2sgn  25872  sincosq3sgn  25873  sincosq4sgn  25874  sinq12gt0  25880  abssinper  25893  coskpi  25895  sineq0  25896  coseq1  25897  efeq1  25900  resinf1o  25908  efif1olem2  25915  efif1olem4  25917  logneg2  25986  cxpsqrtlem  26073  cxpsqrt  26074  logsqrt  26075  1cubr  26208  leibpilem2  26307  basellem3  26448  ppiub  26568  chtublem  26575  chtub  26576  bcmax  26642  bcp1ctr  26643  bposlem2  26649  bposlem6  26653  bposlem9  26656  logdivsum  26897  4ipval2  29692  ipidsq  29694  dipcl  29696  dipcj  29698  ipasslem11  29824  hvmul0  30008  pjhthlem1  30375  h1de2bi  30538  spanunsni  30563  adjeu  30873  nmopge0  30895  nmfnge0  30911  opsqrlem6  31129  mdsl1i  31305  mdsl2bi  31307  mdexchi  31319  superpos  31338  atabsi  31385  dmdbr5ati  31406  cdj3lem1  31418  fpwrelmapffslem  31696  dp2cl  31785  dpfrac1  31797  cshw1s2  31863  ogrpaddlt  31974  ofldlt1  32155  ofldchr  32156  oddpwdc  33011  eulerpartgbij  33029  subfacp1lem2a  33831  subfacp1lem5  33835  subfacp1lem6  33836  subfaclim  33839  sinccvglem  34317  dfon2lem3  34416  dfon2lem7  34420  wsuceq1  34446  clsun  34846  vtoclefex  35851  finxpreclem5  35912  sin2h  36114  cos2h  36115  tan2h  36116  poimirlem22  36146  poimirlem31  36155  opnmbllem0  36160  mblfinlem3  36163  itg2addnclem3  36177  ftc1cnnclem  36195  ftc1anclem6  36202  ftc2nc  36206  dvasin  36208  fdc  36250  constcncf  36267  heiborlem7  36322  atlatmstc  37827  lcmineqlem10  40541  lcmineqlem12  40543  facp2  40597  fac2xp3  40658  sn-00idlem1  40910  0prjspnlem  41004  diophren  41179  oaabsb  41672  dftrcl3  42080  dfrtrcl3  42093  cotrclrcl  42102  lhe4.4ex1a  42697  dirkerper  44423  zlmodzxznm  46664  sinh-conventional  47270
  Copyright terms: Public domain W3C validator