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

Theorem mp3an23 1414
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 1411 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan2 706 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  sbciegf  3461  predeq1  5670  wrecseq1  7395  ac6sfi  8189  unfilem1  8209  ordtypelem2  8409  infxpenc2  8830  cda0en  8986  cfsmolem  9077  axdc4lem  9262  1nqenq  9769  mul02lem1  10197  muleqadd  10656  halfcl  11242  rehalfcl  11243  half0  11244  2halves  11245  halfpos2  11246  halfnneg2  11248  halfaddsub  11250  nneo  11446  zeo  11448  peano5uzi  11451  fztp  12382  uzrdgxfr  12749  bcn2  13089  bcpasc  13091  hashxplem  13203  hashfun  13207  swrds2  13666  repsw2  13674  repsw3  13675  imre  13829  reim  13830  crim  13836  addcj  13869  imval2  13872  cnpart  13961  sqrlem7  13970  absmax  14050  binomfallfaclem2  14752  bpoly2  14769  bpoly3  14770  fsumcube  14772  efgt0  14814  sinf  14835  efi4p  14848  resin4p  14849  recos4p  14850  sinneg  14857  efival  14863  cosadd  14876  sinmul  14883  sinbnd  14891  cosbnd  14892  ef01bndlem  14895  sin01bnd  14896  cos01bnd  14897  sin01gt0  14901  cos01gt0  14902  sin02gt0  14903  rpnnen2lem11  14934  rpnnen2lem12  14935  odd2np1lem  15045  odd2np1  15046  pythagtriplem12  15512  pythagtriplem14  15514  pythagtriplem15  15515  pythagtriplem16  15516  pythagtriplem17  15517  pockthi  15592  prmreclem5  15605  prmreclem6  15606  prmlem0  15793  prdsplusg  16099  prdsmulr  16100  prdsvsca  16101  odinf  17961  lbsexg  19145  psgnghm2  19908  mopnex  22305  tngnm  22436  tngngp2  22437  tngngpd  22438  tngngp  22439  addccncf  22700  iihalf1  22711  iihalf2  22713  pjthlem1  23189  ovolunlem1a  23245  ovolunlem1  23246  opnmbllem  23350  vitalilem4  23361  iblcnlem1  23535  itgcnlem  23537  dvmptre  23713  dvmptim  23714  dvlipcn  23738  mdegldg  23807  aaliou3lem3  24080  aaliou3lem8  24081  sincosq1lem  24230  sincosq2sgn  24232  sincosq3sgn  24233  sincosq4sgn  24234  sinq12gt0  24240  abssinper  24251  coskpi  24253  sineq0  24254  coseq1  24255  efeq1  24256  resinf1o  24263  efif1olem2  24270  efif1olem4  24272  logneg2  24342  cxpsqrtlem  24429  cxpsqrt  24430  logsqrt  24431  1cubr  24550  leibpilem1  24648  leibpilem2  24649  basellem3  24790  ppiub  24910  chtublem  24917  chtub  24918  bcmax  24984  bcp1ctr  24985  bposlem2  24991  bposlem6  24995  bposlem9  24998  logdivsum  25203  4ipval2  27533  ipidsq  27535  dipcl  27537  dipcj  27539  ipasslem11  27665  hvmul0  27851  pjhthlem1  28220  h1de2bi  28383  spanunsni  28408  adjeu  28718  nmopge0  28740  nmfnge0  28756  opsqrlem6  28974  mdsl1i  29150  mdsl2bi  29152  mdexchi  29164  superpos  29183  atabsi  29230  dmdbr5ati  29251  cdj3lem1  29263  fpwrelmapffslem  29481  dp2cl  29561  dpfrac1  29573  dpfrac1OLD  29574  ogrpaddlt  29692  ofldlt1  29787  ofldchr  29788  oddpwdc  30390  eulerpartgbij  30408  subfacp1lem2a  31136  subfacp1lem5  31140  subfacp1lem6  31141  subfaclim  31144  sinccvglem  31540  dfon2lem3  31664  dfon2lem7  31668  wsuceq1  31735  clsun  32298  vtoclefex  33152  finxpreclem5  33203  sin2h  33370  cos2h  33371  tan2h  33372  poimirlem22  33402  poimirlem31  33411  opnmbllem0  33416  mblfinlem3  33419  itg2addnclem3  33434  ftc1cnnclem  33454  ftc1anclem6  33461  ftc2nc  33465  dvasin  33467  fdc  33512  constcncf  33529  sub1cncf  33531  sub2cncf  33532  heiborlem7  33587  atlatmstc  34425  diophren  37196  dftrcl3  37831  dfrtrcl3  37844  cotrclrcl  37853  lhe4.4ex1a  38348  dirkerper  40076  zlmodzxznm  42051  sinh-conventional  42245
  Copyright terms: Public domain W3C validator