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

Theorem mp3an 1452
Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
Hypotheses
Ref Expression
mp3an.1 𝜑
mp3an.2 𝜓
mp3an.3 𝜒
mp3an.4 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an 𝜃

Proof of Theorem mp3an
StepHypRef Expression
1 mp3an.2 . 2 𝜓
2 mp3an.3 . 2 𝜒
3 mp3an.1 . . 3 𝜑
4 mp3an.4 . . 3 ((𝜑𝜓𝜒) → 𝜃)
53, 4mp3an1 1439 . 2 ((𝜓𝜒) → 𝜃)
61, 2, 5mp2an 688 1 𝜃
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  raltp  4633  rextp  4634  opthhausdorff  5398  funopg  6382  feq12i  6500  ftp  6911  caovass  7337  caovdi  7356  ordom  7578  mptexw  7643  ofmres  7674  mpoexw  7765  omopthlem1  8271  omopthlem2  8272  omopthi  8273  xpcomen  8596  unfilem3  8772  hartogs  8996  card2on  9006  unwf  9227  inlresf1  9332  inrresf1  9334  tskwe  9367  alephsmo  9516  dfac4  9536  dfac2a  9543  ackbij1lem13  9642  axdc2lem  9858  axcclem  9867  ondomon  9973  cfpwsdom  9994  pwfseqlem2  10069  pwfseqlem3  10070  1lt2pi  10315  addassi  10639  mulassi  10640  adddii  10641  adddiri  10642  lttri  10754  lelttri  10755  ltletri  10756  letri  10757  ltadd2i  10759  mul02lem2  10805  addid1  10808  addcani  10821  addcan2i  10822  mul12i  10823  mul32i  10824  add12i  10850  add32i  10851  subaddi  10961  subadd2i  10962  subsub23i  10964  addsubassi  10965  addsubi  10966  subcani  10967  subcan2i  10968  pnncani  10969  subdii  11077  subdiri  11078  ltadd1i  11182  leadd1i  11183  leadd2i  11184  ltsubaddi  11185  lesubaddi  11186  ltsubadd2i  11187  lesubadd2i  11188  ltaddsubi  11189  mulcani  11267  div23i  11386  div11i  11387  1mhlfehlf  11844  halfpm6th  11846  3halfnz  12049  addex  12375  mulex  12376  unirnioo  12825  ioorebas  12827  xnn0xrge0  12879  fldiv4lem1div2  13195  uzenom  13320  nnenom  13336  seqexw  13373  m1expcl2  13439  i4  13555  expnass  13558  faclbnd4lem1  13641  bcn1  13661  hashfxnn0  13685  ccat2s1p1  13973  ccat2s1p2  13974  cats1fvn  14208  cats1fv  14209  cats1cat  14211  cats2cat  14212  wrdlen3s3  14299  abs3difi  14757  0.999...  15225  bpoly3  15400  ef01bndlem  15525  cos1bnd  15528  cos2bnd  15529  sin4lt0  15536  rpnnen2lem3  15557  rpnnen2lem11  15565  rpnnen  15568  rexpen  15569  aleph1irr  15587  3dvdsdec  15669  3dvds2dec  15670  divalglem2  15734  ndvdsi  15751  flodddiv4  15752  gcdaddmlem  15860  bezout  15879  3lcm2e6woprm  15947  6lcm4e12  15948  lcmf0  15966  lcmf2a3a4e12  15979  dec2dvds  16387  modxai  16392  modsubi  16396  gcdi  16397  numexp2x  16403  prdsval  16716  prdsds  16725  pmtrprfval  18544  m1expaddsub  18555  0frgp  18834  staffval  19547  cnfldcj  20480  cnfldds  20483  cnfldfun  20485  xrsadd  20490  xrsmul  20491  xrsds  20516  cnmgpid  20535  nn0srg  20543  rge0srg  20544  zring0  20555  cnmsgnsubg  20649  psgninv  20654  re0g  20684  ocvfval  20738  frlmbas  20827  mdetrlin  21139  mdetunilem9  21157  leordtval2  21748  iscnp2  21775  utop3cls  22787  nmfval  23125  nmoffn  23247  nmofval  23250  icccld  23302  addcnlem  23399  iimulcn  23469  icopnfhmeo  23474  iccpnfcnv  23475  iccpnfhmeo  23476  xrhmeo  23477  xrhmph  23478  oprpiece1res1  23482  oprpiece1res2  23483  ishtpy  23503  pcoass  23555  cnstrcvs  23672  cncvs  23676  recvs  23677  qcvs  23678  zclmncvs  23679  tcphex  23747  cnfldcusp  23887  resscdrg  23888  reust  23911  recusp  23912  vitalilem4  24139  vitalilem5  24140  mbfdm  24154  dveflem  24503  dvlipcn  24518  c1lip2  24522  dgrid  24781  iaa  24841  abelthlem3  24948  abelthlem5  24950  abelth  24956  efcn  24958  sinhalfpilem  24976  sincosq1lem  25010  sincosq4sgn  25014  tangtx  25018  sincos4thpi  25026  sincos6thpi  25028  pigt3  25030  pige3ALT  25032  relogcn  25148  dvlog2lem  25162  dvlog2  25163  logtayl  25170  logtayl2  25172  cxpsqrtlem  25212  cxpsqrt  25213  2irrexpq  25240  cxpcn2  25254  cxpcn3  25256  logblog  25297  2logb9irr  25300  2logb3irr  25302  2logb9irrALT  25303  sqrt2cxp2logb9e3  25304  2irrexpqALT  25305  ang180lem1  25314  ang180lem2  25315  1cubrlem  25346  mcubic  25352  quart1lem  25360  quart1  25361  reasinsin  25401  atancj  25415  efiatan  25417  atantan  25428  atanbndlem  25430  atan1  25433  atancn  25441  atantayl2  25443  log2cnv  25449  log2tlbnd  25450  log2ublem1  25451  log2ublem2  25452  log2ub  25454  efrlim  25474  scvxcvx  25490  1sgm2ppw  25703  ppiub  25707  bclbnd  25783  bposlem8  25794  lgsdir2lem1  25828  lgsdir2lem5  25832  lgseisenlem1  25878  lgseisenlem2  25879  lgsquadlem1  25883  chebbnd1  25975  dchrvmasumlem2  26001  istrkg3ld  26174  trgcgrg  26228  ax5seglem7  26648  axlowdimlem6  26660  axlowdimlem8  26662  axlowdimlem11  26665  elntg2  26698  cusgrsizeindb1  27159  vtxdginducedm1  27252  0grrusgr  27288  erclwwlktr  27727  erclwwlkntr  27777  wlk2v2e  27863  upgr3v3e3cycl  27886  konigsberglem1  27958  konigsberglem2  27959  konigsberglem3  27960  konigsberglem5  27962  ex-fl  28153  ex-mod  28155  ex-hash  28159  ex-lcm  28164  0vfval  28310  smcnlem  28401  lnocoi  28461  nmlno0lem  28497  nmblolbii  28503  blocnilem  28508  blocni  28509  cncph  28523  isph  28526  ip0i  28529  ip1ilem  28530  ip2i  28532  ipdirilem  28533  ipasslem7  28540  ipasslem8  28541  ipasslem9  28542  ipasslem10  28543  ipasslem11  28544  ip2dii  28548  pythi  28554  siilem1  28555  siilem2  28556  siii  28557  hvmulassi  28750  hvmulcomi  28751  hvdistr1i  28755  hvsubdistr1i  28756  hvassi  28757  hvadd32i  28758  hvsubassi  28759  hvsub32i  28760  normlem0  28813  normlem8  28821  normlem9  28822  bcseqi  28824  polid2i  28861  hhph  28882  hlim0  28939  shscli  29021  shlessi  29081  shlej1i  29082  omlsilem  29106  shlubi  29119  h1de2i  29257  pjadjii  29378  pjaddii  29379  pjmulii  29381  pjdifnormii  29387  pjcji  29388  hoaddsubassi  29524  eigrei  29538  eigposi  29540  eigorthi  29541  adj0  29698  lnopeq0lem1  29709  lnopunilem1  29714  lnophmlem2  29721  nmcexi  29730  nmcopexi  29731  lnfn0i  29746  nmcfnexi  29755  mdexchi  30039  xppreima2  30323  dp2clq  30484  dp2lt  30488  dp2ltc  30490  dpexpp1  30511  dpmul  30516  dpmul4  30517  elxrge02  30535  xrge0adddir  30606  psgnid  30666  cnmsgn0g  30715  altgnsg  30718  xrnarchi  30740  xrge0slmod  30844  ccfldextdgrr  30956  raddcn  31071  xrge0iifcnv  31075  xrge0iifiso  31077  xrge0iifhmeo  31078  xrge0iifhom  31079  xrge0iifmhm  31081  xrge0mulc1cn  31083  lmlimxrge0  31090  pnfneige0  31093  lmxrge0  31094  zringnm  31100  rezh  31111  qqh0  31124  qqh1  31125  qqhucn  31132  esumpinfval  31231  hashf2  31242  esumcvg  31244  br2base  31426  sxbrsigalem3  31429  dya2iocbrsiga  31432  dya2icobrsiga  31433  sxbrsigalem1  31442  sxbrsigalem2  31443  sxbrsigalem4  31444  sxbrsigalem5  31445  sxbrsiga  31447  ballotlem2  31645  ballotlem4  31655  ballotlemi1  31659  ballotth  31694  sgnclre  31696  signstf  31735  itgexpif  31776  chtvalz  31799  hgt750lemd  31818  hgt750lem  31821  tgoldbachgnn  31829  lfuhgr2  32262  subfacp1lem1  32323  subfacp1lem6  32329  kur14lem6  32355  cvmliftlem4  32432  satf0suc  32520  problem4  32808  quad3  32810  logi  32863  iexpire  32864  fununiq  32909  fvtransport  33390  bj-minftyccb  34399  taupilem2  34485  1oequni2o  34531  finxp1o  34555  finxpreclem4  34557  cos2h  34764  tan2h  34765  poimirlem9  34782  poimirlem27  34800  poimirlem28  34801  ismblfin  34814  mbfposadd  34820  ftc1anclem5  34852  asindmre  34858  dvasin  34859  dvacos  34860  rrnval  34986  el3v  35372  dihjatcclem4  38437  sn-00idlem2  39107  sn-00id  39109  remul02  39113  sn-0lt1  39124  rabren3dioph  39290  jm2.27dlem2  39485  rmydioph  39489  rmxdioph  39491  expdiophlem2  39497  expdioph  39498  arearect  39700  areaquad  39701  corclrcl  39930  iunrelexpuztr  39942  corcltrcl  39962  dffrege76  40163  k0004val0  40382  lhe4.4ex1a  40538  binomcxplemdvbinom  40562  binomcxplemnotnn0  40565  ax6e2ndeqALT  41142  sineq0ALT  41148  pnfel0pnf  41680  lptioo2cn  41802  limsup10ex  41930  liminf10ex  41931  icccncfext  42046  itgsin0pilem1  42111  itgsbtaddcnst  42143  stoweidlem13  42175  wallispilem2  42228  wallispilem4  42230  wallispi2lem1  42233  stirlinglem13  42248  dirkerper  42258  dirkertrigeqlem3  42262  dirkeritg  42264  dirkercncflem1  42265  dirkercncflem4  42268  fourierdlem42  42311  fourierdlem62  42330  fourierdlem102  42370  fourierdlem103  42371  fourierdlem104  42372  fourierdlem114  42382  sqwvfoura  42390  fourierswlem  42392  fouriersw  42393  smfmullem4  42946  fmtnoprmfac2lem1  43605  fmtno4prm  43614  2exp5  43632  2exp11  43642  3exp4mod41  43658  41prothprmlem2  43660  6gbe  43813  7gbow  43814  8gbe  43815  9gbo  43816  11gbo  43817  sbgoldbalt  43823  nnsum4primesevenALTV  43843  0nodd  43954  oddinmgm  43959  2zrng0  44137  zlmodzxz0  44332  zlmodzxzequa  44479  zlmodzxzequap  44482  zlmodzxzldeplem3  44485  nnlog2ge0lt1  44554  blen1  44572  blen2  44573  nnolog2flm1  44578  ehl2eudisval0  44640  line2ylem  44666
  Copyright terms: Public domain W3C validator