MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp4an Unicode version

Theorem mp4an 673
Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.)
Hypotheses
Ref Expression
mp4an.1
mp4an.2
mp4an.3
mp4an.4
mp4an.5
Assertion
Ref Expression
mp4an

Proof of Theorem mp4an
StepHypRef Expression
1 mp4an.1 . . 3
2 mp4an.2 . . 3
31, 2pm3.2i 455 . 2
4 mp4an.3 . . 3
5 mp4an.4 . . 3
64, 5pm3.2i 455 . 2
7 mp4an.5 . 2
83, 6, 7mp2an 672 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  noinfep  8097  1lt2nq  9372  m1p1sr  9490  m1m1sr  9491  axi2m1  9557  mul4i  9798  add4i  9821  add42i  9822  addsub4i  9939  muladdi  10032  lt2addi  10140  le2addi  10141  mulne0i  10217  divne0i  10317  divmuldivi  10329  divadddivi  10331  divdivdivi  10332  subreci  10399  8th4div3  10784  xrsup0  11544  sqrt2gt1lt2  13108  nprmi  14232  mod2xnegi  14557  catcfuccl  15436  catcxpccl  15476  iccpnfhmeo  21445  xrhmeo  21446  cnheiborlem  21454  pcoval1  21513  pcoval2  21516  pcoass  21524  lhop1lem  22414  efcvx  22844  dvrelog  23018  dvlog  23032  dvlog2  23034  dvsqrt  23118  cxpcn3  23122  ang180lem1  23141  dvatan  23266  log2cnv  23275  log2tlbnd  23276  log2ub  23280  harmonicbnd3  23337  ppiub  23479  bposlem8  23566  bposlem9  23567  lgsdir2lem1  23598  m1lgs  23637  2sqlem11  23650  chebbnd1  23657  usgraexmpl  24401  constr3lem4  24647  vdegp1ai  24984  vdegp1bi  24985  siilem1  25766  hvadd4i  25975  his35i  26006  bdophsi  27015  bdopcoi  27017  mdcompli  27348  dmdcompli  27349  xrge00  27674  sqsscirc1  27890  raddcn  27911  xrge0iifcnv  27915  xrge0iifiso  27917  xrge0iifhom  27919  dstfrvclim1  28416  signsply0  28508  cvmlift2lem6  28753  cvmlift2lem12  28759  dvcnsqrt  30101  lhe4.4ex1a  31234  dvcosre  31706  wallispi  31852  fourierdlem57  31946  fourierdlem58  31947  fourierdlem112  32001  fouriersw  32014  zlmodzxzequa  33097  zlmodzxzequap  33100
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 185  df-an 371
  Copyright terms: Public domain W3C validator