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

Theorem mp3an23 1456
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 1453 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan2 707 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 1056
This theorem is referenced by:  sbciegf  3500  predeq1  5720  wrecseq1  7455  ac6sfi  8245  unfilem1  8265  ordtypelem2  8465  infxpenc2  8883  cda0en  9039  cfsmolem  9130  axdc4lem  9315  1nqenq  9822  mul02lem1  10250  muleqadd  10709  halfcl  11295  rehalfcl  11296  half0  11297  2halves  11298  halfpos2  11299  halfnneg2  11301  halfaddsub  11303  nneo  11499  zeo  11501  peano5uzi  11504  fztp  12435  uzrdgxfr  12806  bcn2  13146  bcpasc  13148  hashxplem  13258  hashfun  13262  swrds2  13731  repsw2  13739  repsw3  13740  imre  13892  reim  13893  crim  13899  addcj  13932  imval2  13935  cnpart  14024  sqrlem7  14033  absmax  14113  binomfallfaclem2  14815  bpoly2  14832  bpoly3  14833  fsumcube  14835  efgt0  14877  sinf  14898  efi4p  14911  resin4p  14912  recos4p  14913  sinneg  14920  efival  14926  cosadd  14939  sinmul  14946  sinbnd  14954  cosbnd  14955  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  sin01gt0  14964  cos01gt0  14965  sin02gt0  14966  rpnnen2lem11  14997  rpnnen2lem12  14998  odd2np1lem  15111  odd2np1  15112  pythagtriplem12  15578  pythagtriplem14  15580  pythagtriplem15  15581  pythagtriplem16  15582  pythagtriplem17  15583  pockthi  15658  prmreclem5  15671  prmreclem6  15672  prmlem0  15859  prdsplusg  16165  prdsmulr  16166  prdsvsca  16167  odinf  18026  lbsexg  19212  psgnghm2  19975  mopnex  22371  tngnm  22502  tngngp2  22503  tngngpd  22504  tngngp  22505  addccncf  22766  iihalf1  22777  iihalf2  22779  pjthlem1  23254  ovolunlem1a  23310  ovolunlem1  23311  opnmbllem  23415  vitalilem4  23425  iblcnlem1  23599  itgcnlem  23601  dvmptre  23777  dvmptim  23778  dvlipcn  23802  mdegldg  23871  aaliou3lem3  24144  aaliou3lem8  24145  sincosq1lem  24294  sincosq2sgn  24296  sincosq3sgn  24297  sincosq4sgn  24298  sinq12gt0  24304  abssinper  24315  coskpi  24317  sineq0  24318  coseq1  24319  efeq1  24320  resinf1o  24327  efif1olem2  24334  efif1olem4  24336  logneg2  24406  cxpsqrtlem  24493  cxpsqrt  24494  logsqrt  24495  1cubr  24614  leibpilem1  24712  leibpilem2  24713  basellem3  24854  ppiub  24974  chtublem  24981  chtub  24982  bcmax  25048  bcp1ctr  25049  bposlem2  25055  bposlem6  25059  bposlem9  25062  logdivsum  25267  4ipval2  27691  ipidsq  27693  dipcl  27695  dipcj  27697  ipasslem11  27823  hvmul0  28009  pjhthlem1  28378  h1de2bi  28541  spanunsni  28566  adjeu  28876  nmopge0  28898  nmfnge0  28914  opsqrlem6  29132  mdsl1i  29308  mdsl2bi  29310  mdexchi  29322  superpos  29341  atabsi  29388  dmdbr5ati  29409  cdj3lem1  29421  fpwrelmapffslem  29635  dp2cl  29715  dpfrac1  29727  dpfrac1OLD  29728  ogrpaddlt  29846  ofldlt1  29941  ofldchr  29942  oddpwdc  30544  eulerpartgbij  30562  subfacp1lem2a  31288  subfacp1lem5  31292  subfacp1lem6  31293  subfaclim  31296  sinccvglem  31692  dfon2lem3  31814  dfon2lem7  31818  wsuceq1  31885  clsun  32448  vtoclefex  33311  finxpreclem5  33362  sin2h  33529  cos2h  33530  tan2h  33531  poimirlem22  33561  poimirlem31  33570  opnmbllem0  33575  mblfinlem3  33578  itg2addnclem3  33593  ftc1cnnclem  33613  ftc1anclem6  33620  ftc2nc  33624  dvasin  33626  fdc  33671  constcncf  33688  sub1cncf  33690  sub2cncf  33691  heiborlem7  33746  atlatmstc  34924  diophren  37694  dftrcl3  38329  dfrtrcl3  38342  cotrclrcl  38351  lhe4.4ex1a  38845  dirkerper  40631  zlmodzxznm  42611  sinh-conventional  42808
  Copyright terms: Public domain W3C validator