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

Theorem mp3an23 1450
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 1447 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan2 690 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:  sbciegf  3795  predeq1  6137  wrecseq1  7946  ac6sfi  8759  unfilem1  8779  ordtypelem2  8980  infxpenc2  9446  dju0en  9599  cfsmolem  9690  axdc4lem  9875  1nqenq  10382  mul02lem1  10814  muleqadd  11282  halfcl  11859  rehalfcl  11860  half0  11861  2halves  11862  halfpos2  11863  halfnneg2  11865  halfaddsub  11867  nneo  12063  zeo  12065  peano5uzi  12068  fztp  12967  uzrdgxfr  13339  bcn2  13684  bcpasc  13686  hashxplem  13799  hashfun  13803  swrds2  14302  repsw2  14312  repsw3  14313  imre  14467  reim  14468  crim  14474  addcj  14507  imval2  14510  cnpart  14599  sqrlem7  14608  absmax  14689  binomfallfaclem2  15394  bpoly2  15411  bpoly3  15412  fsumcube  15414  efgt0  15456  sinf  15477  efi4p  15490  resin4p  15491  recos4p  15492  sinneg  15499  efival  15505  cosadd  15518  sinmul  15525  sinbnd  15533  cosbnd  15534  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  sin01gt0  15543  cos01gt0  15544  sin02gt0  15545  rpnnen2lem11  15577  rpnnen2lem12  15578  odd2np1lem  15689  odd2np1  15690  pythagtriplem12  16161  pythagtriplem14  16163  pythagtriplem15  16164  pythagtriplem16  16165  pythagtriplem17  16166  pockthi  16241  prmreclem5  16254  prmreclem6  16255  prmlem0  16439  prdsplusg  16731  prdsmulr  16732  prdsvsca  16733  odinf  18690  lbsexg  19936  psgnghm2  20725  mopnex  23129  tngnm  23260  tngngp2  23261  tngngpd  23262  tngngp  23263  addccncf  23525  sub1cncf  23527  sub2cncf  23528  iihalf1  23539  iihalf2  23541  pjthlem1  24044  ovolunlem1a  24103  ovolunlem1  24104  opnmbllem  24208  vitalilem4  24218  iblcnlem1  24394  itgcnlem  24396  dvmptre  24575  dvmptim  24576  dvlipcn  24600  mdegldg  24670  aaliou3lem3  24943  aaliou3lem8  24944  sincosq1lem  25093  sincosq2sgn  25095  sincosq3sgn  25096  sincosq4sgn  25097  sinq12gt0  25103  abssinper  25116  coskpi  25118  sineq0  25119  coseq1  25120  efeq1  25123  resinf1o  25131  efif1olem2  25138  efif1olem4  25140  logneg2  25209  cxpsqrtlem  25296  cxpsqrt  25297  logsqrt  25298  1cubr  25431  leibpilem2  25530  basellem3  25671  ppiub  25791  chtublem  25798  chtub  25799  bcmax  25865  bcp1ctr  25866  bposlem2  25872  bposlem6  25876  bposlem9  25879  logdivsum  26120  4ipval2  28494  ipidsq  28496  dipcl  28498  dipcj  28500  ipasslem11  28626  hvmul0  28810  pjhthlem1  29177  h1de2bi  29340  spanunsni  29365  adjeu  29675  nmopge0  29697  nmfnge0  29713  opsqrlem6  29931  mdsl1i  30107  mdsl2bi  30109  mdexchi  30121  superpos  30140  atabsi  30187  dmdbr5ati  30208  cdj3lem1  30220  fpwrelmapffslem  30479  dp2cl  30567  dpfrac1  30579  cshw1s2  30645  ogrpaddlt  30750  ofldlt1  30919  ofldchr  30920  oddpwdc  31669  eulerpartgbij  31687  subfacp1lem2a  32484  subfacp1lem5  32488  subfacp1lem6  32489  subfaclim  32492  sinccvglem  32972  dfon2lem3  33087  dfon2lem7  33091  wsuceq1  33159  clsun  33733  vtoclefex  34696  finxpreclem5  34757  sin2h  34992  cos2h  34993  tan2h  34994  poimirlem22  35024  poimirlem31  35033  opnmbllem0  35038  mblfinlem3  35041  itg2addnclem3  35055  ftc1cnnclem  35073  ftc1anclem6  35080  ftc2nc  35084  dvasin  35086  fdc  35128  constcncf  35145  heiborlem7  35200  atlatmstc  36560  lcmineqlem10  39274  lcmineqlem12  39276  facp2  39293  fac2xp3  39322  sn-00idlem1  39466  0prjspnlem  39528  diophren  39670  dftrcl3  40337  dfrtrcl3  40350  cotrclrcl  40359  lhe4.4ex1a  40953  dirkerper  42664  zlmodzxznm  44832  sinh-conventional  45191
  Copyright terms: Public domain W3C validator