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

Theorem mp3an 1458
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 1445 . 2 ((𝜓𝜒) → 𝜃)
61, 2, 5mp2an 691 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:  raltp  4626  rextp  4627  opthhausdorff  5395  funopg  6379  feq12i  6498  ftp  6912  caovass  7344  caovdi  7363  ordom  7585  mptexw  7651  ofmres  7682  mpoexw  7774  omopthlem1  8280  omopthlem2  8281  omopthi  8282  xpcomen  8606  unfilem3  8783  hartogs  9007  card2on  9017  unwf  9238  inlresf1  9343  inrresf1  9345  tskwe  9378  alephsmo  9528  dfac4  9548  dfac2a  9555  ackbij1lem13  9654  axdc2lem  9870  axcclem  9879  ondomon  9985  cfpwsdom  10006  pwfseqlem2  10081  pwfseqlem3  10082  1lt2pi  10327  addassi  10651  mulassi  10652  adddii  10653  adddiri  10654  lttri  10766  lelttri  10767  ltletri  10768  letri  10769  ltadd2i  10771  mul02lem2  10817  addid1  10820  addcani  10833  addcan2i  10834  mul12i  10835  mul32i  10836  add12i  10862  add32i  10863  subaddi  10973  subadd2i  10974  subsub23i  10976  addsubassi  10977  addsubi  10978  subcani  10979  subcan2i  10980  pnncani  10981  subdii  11089  subdiri  11090  ltadd1i  11194  leadd1i  11195  leadd2i  11196  ltsubaddi  11197  lesubaddi  11198  ltsubadd2i  11199  lesubadd2i  11200  ltaddsubi  11201  mulcani  11279  div23i  11398  div11i  11399  1mhlfehlf  11855  halfpm6th  11857  3halfnz  12060  addex  12386  mulex  12387  unirnioo  12838  ioorebas  12840  xnn0xrge0  12895  fldiv4lem1div2  13213  uzenom  13338  nnenom  13354  seqexw  13391  m1expcl2  13458  i4  13574  expnass  13577  faclbnd4lem1  13660  bcn1  13680  hashfxnn0  13704  ccat2s1p1  13987  ccat2s1p2  13988  cats1fvn  14222  cats1fv  14223  cats1cat  14225  cats2cat  14226  wrdlen3s3  14313  abs3difi  14771  0.999...  15239  bpoly3  15414  ef01bndlem  15539  cos1bnd  15542  cos2bnd  15543  sin4lt0  15550  rpnnen2lem3  15571  rpnnen2lem11  15579  rpnnen  15582  rexpen  15583  aleph1irr  15601  3dvdsdec  15683  3dvds2dec  15684  divalglem2  15746  ndvdsi  15763  flodddiv4  15764  gcdaddmlem  15872  bezout  15891  3lcm2e6woprm  15959  6lcm4e12  15960  lcmf0  15978  lcmf2a3a4e12  15991  dec2dvds  16399  modxai  16404  modsubi  16408  gcdi  16409  numexp2x  16415  2exp5  16422  prdsval  16730  prdsds  16739  0symgefmndeq  18524  pmtrprfval  18617  m1expaddsub  18628  0frgp  18907  staffval  19620  cnfldcj  20107  cnfldds  20110  cnfldfun  20112  xrsadd  20117  xrsmul  20118  xrsds  20143  cnmgpid  20162  nn0srg  20170  rge0srg  20171  zring0  20182  cnmsgnsubg  20275  psgninv  20280  re0g  20310  ocvfval  20364  frlmbas  20453  mdetrlin  21216  mdetunilem9  21234  leordtval2  21826  iscnp2  21853  utop3cls  22866  nmfval  23204  nmoffn  23326  nmofval  23329  icccld  23381  addcnlem  23478  iimulcn  23552  icopnfhmeo  23557  iccpnfcnv  23558  iccpnfhmeo  23559  xrhmeo  23560  xrhmph  23561  oprpiece1res1  23565  oprpiece1res2  23566  ishtpy  23586  pcoass  23638  cnstrcvs  23755  cncvs  23759  recvs  23760  qcvs  23761  zclmncvs  23762  tcphex  23830  cnfldcusp  23970  resscdrg  23971  reust  23994  recusp  23995  vitalilem4  24224  vitalilem5  24225  mbfdm  24239  dveflem  24591  dvlipcn  24606  c1lip2  24610  dgrid  24870  iaa  24930  abelthlem3  25037  abelthlem5  25039  abelth  25045  efcn  25047  sinhalfpilem  25065  sincosq1lem  25099  sincosq4sgn  25103  tangtx  25107  sincos4thpi  25115  sincos6thpi  25117  pigt3  25119  pige3ALT  25121  cos0pilt1  25133  relogcn  25238  dvlog2lem  25252  dvlog2  25253  logtayl  25260  logtayl2  25262  cxpsqrtlem  25302  cxpsqrt  25303  2irrexpq  25330  cxpcn2  25344  cxpcn3  25346  logblog  25387  2logb9irr  25390  2logb3irr  25392  2logb9irrALT  25393  sqrt2cxp2logb9e3  25394  2irrexpqALT  25395  ang180lem1  25404  ang180lem2  25405  1cubrlem  25436  mcubic  25442  quart1lem  25450  quart1  25451  reasinsin  25491  atancj  25505  efiatan  25507  atantan  25518  atanbndlem  25520  atan1  25523  atancn  25531  atantayl2  25533  log2cnv  25539  log2tlbnd  25540  log2ublem1  25541  log2ublem2  25542  log2ub  25544  efrlim  25564  scvxcvx  25580  1sgm2ppw  25793  ppiub  25797  bclbnd  25873  bposlem8  25884  lgsdir2lem1  25918  lgsdir2lem5  25922  lgseisenlem1  25968  lgseisenlem2  25969  lgsquadlem1  25973  chebbnd1  26065  dchrvmasumlem2  26091  istrkg3ld  26264  trgcgrg  26318  ax5seglem7  26738  axlowdimlem6  26750  axlowdimlem8  26752  axlowdimlem11  26755  elntg2  26788  cusgrsizeindb1  27249  vtxdginducedm1  27342  0grrusgr  27378  erclwwlktr  27816  erclwwlkntr  27865  wlk2v2e  27951  upgr3v3e3cycl  27974  konigsberglem1  28046  konigsberglem2  28047  konigsberglem3  28048  konigsberglem5  28050  ex-fl  28241  ex-mod  28243  ex-hash  28247  ex-lcm  28252  0vfval  28398  smcnlem  28489  lnocoi  28549  nmlno0lem  28585  nmblolbii  28591  blocnilem  28596  blocni  28597  cncph  28611  isph  28614  ip0i  28617  ip1ilem  28618  ip2i  28620  ipdirilem  28621  ipasslem7  28628  ipasslem8  28629  ipasslem9  28630  ipasslem10  28631  ipasslem11  28632  ip2dii  28636  pythi  28642  siilem1  28643  siilem2  28644  siii  28645  hvmulassi  28838  hvmulcomi  28839  hvdistr1i  28843  hvsubdistr1i  28844  hvassi  28845  hvadd32i  28846  hvsubassi  28847  hvsub32i  28848  normlem0  28901  normlem8  28909  normlem9  28910  bcseqi  28912  polid2i  28949  hhph  28970  hlim0  29027  shscli  29109  shlessi  29169  shlej1i  29170  omlsilem  29194  shlubi  29207  h1de2i  29345  pjadjii  29466  pjaddii  29467  pjmulii  29469  pjdifnormii  29475  pjcji  29476  hoaddsubassi  29612  eigrei  29626  eigposi  29628  eigorthi  29629  adj0  29786  lnopeq0lem1  29797  lnopunilem1  29802  lnophmlem2  29809  nmcexi  29818  nmcopexi  29819  lnfn0i  29834  nmcfnexi  29843  mdexchi  30127  xppreima2  30414  dp2clq  30578  dp2lt  30582  dp2ltc  30584  dpexpp1  30605  dpmul  30610  dpmul4  30611  elxrge02  30629  xrge0adddir  30721  psgnid  30781  cnmsgn0g  30830  altgnsg  30833  xrnarchi  30855  xrge0slmod  30960  ccfldextdgrr  31125  raddcn  31257  xrge0iifcnv  31261  xrge0iifiso  31263  xrge0iifhmeo  31264  xrge0iifhom  31265  xrge0iifmhm  31267  xrge0mulc1cn  31269  lmlimxrge0  31276  pnfneige0  31279  lmxrge0  31280  zringnm  31286  rezh  31297  qqh0  31310  qqh1  31311  qqhucn  31318  esumpinfval  31417  hashf2  31428  esumcvg  31430  br2base  31612  sxbrsigalem3  31615  dya2iocbrsiga  31618  dya2icobrsiga  31619  sxbrsigalem1  31628  sxbrsigalem2  31629  sxbrsigalem4  31630  sxbrsigalem5  31631  sxbrsiga  31633  ballotlem2  31831  ballotlem4  31841  ballotlemi1  31845  ballotth  31880  sgnclre  31882  signstf  31921  itgexpif  31962  chtvalz  31985  hgt750lemd  32004  hgt750lem  32007  tgoldbachgnn  32015  lfuhgr2  32450  subfacp1lem1  32511  subfacp1lem6  32517  kur14lem6  32543  cvmliftlem4  32620  satf0suc  32708  problem4  32996  quad3  32998  logi  33051  iexpire  33052  fununiq  33097  fvtransport  33578  bj-minftyccb  34612  taupilem2  34708  iccioo01  34713  1oequni2o  34757  finxp1o  34781  finxpreclem4  34783  cos2h  35020  tan2h  35021  poimirlem9  35038  poimirlem27  35056  poimirlem28  35057  ismblfin  35070  mbfposadd  35076  ftc1anclem5  35106  asindmre  35112  dvasin  35113  dvacos  35114  rrnval  35237  el3v  35623  dihjatcclem4  38689  lcmineqlem12  39303  sn-00idlem2  39495  sn-00id  39497  remul02  39501  sn-1ticom  39528  sn-0lt1  39535  sn-inelr  39538  rabren3dioph  39700  jm2.27dlem2  39895  rmydioph  39899  rmxdioph  39901  expdiophlem2  39907  expdioph  39908  arearect  40109  areaquad  40110  corclrcl  40352  iunrelexpuztr  40364  corcltrcl  40384  dffrege76  40585  k0004val0  40804  lhe4.4ex1a  40981  binomcxplemdvbinom  41005  binomcxplemnotnn0  41008  ax6e2ndeqALT  41585  sineq0ALT  41591  pnfel0pnf  42118  lptioo2cn  42240  limsup10ex  42368  liminf10ex  42369  icccncfext  42482  itgsin0pilem1  42545  itgsbtaddcnst  42577  stoweidlem13  42608  wallispilem2  42661  wallispilem4  42663  wallispi2lem1  42666  stirlinglem13  42681  dirkerper  42691  dirkertrigeqlem3  42695  dirkeritg  42697  dirkercncflem1  42698  dirkercncflem4  42701  fourierdlem42  42744  fourierdlem62  42763  fourierdlem102  42803  fourierdlem103  42804  fourierdlem104  42805  fourierdlem114  42815  sqwvfoura  42823  fourierswlem  42825  fouriersw  42826  smfmullem4  43379  fmtnoprmfac2lem1  44036  fmtno4prm  44045  2exp11  44071  3exp4mod41  44087  41prothprmlem2  44089  6gbe  44242  7gbow  44243  8gbe  44244  9gbo  44245  11gbo  44246  sbgoldbalt  44252  nnsum4primesevenALTV  44272  0nodd  44383  oddinmgm  44388  2zrng0  44515  zlmodzxz0  44711  zlmodzxzequa  44858  zlmodzxzequap  44861  zlmodzxzldeplem3  44864  nnlog2ge0lt1  44933  blen1  44951  blen2  44952  nnolog2flm1  44957  ackval42  45063  ehl2eudisval0  45092  line2ylem  45118
  Copyright terms: Public domain W3C validator