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

Theorem mp3an1 1409
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an1.1 𝜑
mp3an1.2 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an1 ((𝜓𝜒) → 𝜃)

Proof of Theorem mp3an1
StepHypRef Expression
1 mp3an1.1 . 2 𝜑
2 mp3an1.2 . . 3 ((𝜑𝜓𝜒) → 𝜃)
323expb 1264 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
41, 3mpan 705 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  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:  mp3an12  1412  mp3an1i  1415  mp3anl1  1416  mp3an  1422  mp3an2i  1427  mp3an3an  1428  onint  6980  wfrlem12  7411  wfrlem17  7416  tfrlem9  7466  oaord1  7616  oaword2  7618  oawordeulem  7619  oa00  7624  omword1  7638  omword2  7639  omlimcl  7643  oeoelem  7663  nnaordex  7703  enp1i  8180  unfilem2  8210  dffi3  8322  unbnn3  8541  pwcdaen  8992  ackbij1b  9046  zorn2  9313  zornn0  9315  ttukey  9325  brdom7disj  9338  brdom6disj  9339  wunex2  9545  muladd11  10191  00id  10196  mul02  10199  negsubdi  10322  mulneg1  10451  ltaddpos  10503  addge01  10523  reccl  10677  recid  10684  recid2  10685  recdiv2  10723  divdiv23zi  10763  ltmul12a  10864  lemul12a  10866  mulgt1  10867  ltmulgt11  10868  gt0div  10874  ge0div  10875  lediv12a  10901  ledivp1  10910  ltdiv23i  10933  ledivp1i  10934  ltdivp1i  10935  infm3  10967  nngt1ne1  11032  8th4div3  11237  gtndiv  11439  nn0ind  11457  fnn0ind  11461  supminf  11760  xrre2  11986  2resupmax  12004  qsqueeze  12017  xmulpnf1  12089  xlemul1a  12103  xrub  12127  ioorebas  12260  elfz0ubfz0  12427  expubnd  12904  le2sq2  12922  crreczi  12972  bernneq  12973  faclbnd5  13068  faclbnd6  13069  bccl  13092  hashbc  13220  wrdred1hash  13333  ccatlid  13352  shftfval  13791  sgnp  13811  mulre  13842  sqrlem4  13967  sqrlem7  13970  sqreulem  14080  binom1p  14544  0.999...OLD  14594  fallrisefac  14737  bpoly3  14770  efsub  14811  efi4p  14848  sinadd  14875  cosadd  14876  cos2t  14889  cos2tsin  14890  sin01gt0  14901  cos01gt0  14902  absefib  14909  efieq1re  14910  demoivreALT  14912  rpnnen2lem4  14927  odd2np1  15046  opoe  15068  omoe  15069  opeo  15070  omeo  15071  divalglem0  15097  divalglem4  15100  divalglem9  15105  gcdcllem3  15204  gcdn0gt0  15220  gcdadd  15228  gcdmultiple  15250  algcvgblem  15271  algcvga  15273  isprm3  15377  divgcdodd  15403  coprm  15404  pythagtriplem4  15505  pythagtriplem11  15511  pythagtriplem12  15512  pythagtriplem13  15513  pythagtriplem14  15514  infpn2  15598  1arith2  15613  vdwap0  15661  vdwap1  15662  ipolt  17140  gsumval2a  17260  f1otrspeq  17848  rmodislmod  18912  mplsubrglem  19420  evls1rhm  19668  cnfldneg  19753  cnflddiv  19757  cnfldmulg  19759  cnfldexp  19760  zringmulg  19807  remulg  19934  resubgval  19936  thlleval  20023  frlmsslsp  20116  neiptoptop  20916  iccordt  20999  qustgplem  21905  bl2ioo  22576  ioo2blex  22578  blssioo  22579  tgioo  22580  xrsblre  22595  iccntr  22605  icccmplem3  22608  reconnlem2  22611  opnreen  22615  iccpnfcnv  22724  cnllycmp  22736  pcoptcl  22802  ovolmge0  23226  ovolctb2  23241  ismbl2  23276  cmmbl  23283  nulmbl  23284  unmbl  23286  voliunlem1  23299  voliunlem2  23300  ioombl1  23311  opnmbllem  23350  mbfima  23380  i1fsub  23456  itg1sub  23457  ellimc3  23624  limcflf  23626  dvcnvre  23763  coe1termlem  23995  dgrsub  24009  dvnply2  24023  dvnply  24024  reeff1o  24182  sinperlem  24213  sincosq1eq  24245  resinf1o  24263  logeftb  24311  logge0  24332  logdivlti  24347  efopn  24385  logtayl2  24389  loglesqrt  24480  logrec  24482  xrlimcnp  24676  ppinncl  24881  chtrpcl  24882  bposlem2  24991  bposlem8  24997  lgsdir2  25036  1lgs  25046  brbtwn2  25766  colinearalglem4  25770  ax5seglem1  25789  ax5seglem2  25790  axcontlem2  25826  axcontlem4  25828  axcontlem7  25831  fusgrfis  26203  3cyclfrgrrn  27130  isgrpoi  27322  imsmetlem  27515  nmcvcn  27520  ipval2  27532  lnocoi  27582  nmlno0lem  27618  nmblolbii  27624  blometi  27628  blocnilem  27629  blocni  27630  ipasslem1  27656  ipasslem2  27657  ipasslem4  27659  ipasslem5  27660  ipasslem8  27662  ipblnfi  27681  ip2eqi  27682  ubthlem1  27696  htthlem  27744  h2hmetdval  27805  axhvcom-zf  27810  axhis1-zf  27821  axhis4-zf  27824  hvm1neg  27859  hvsub4  27864  hvsubass  27871  hvsubdistr2  27877  hv2times  27888  hvsubcan  27901  hvsubcan2  27902  his2sub  27919  norm-i  27956  normpyc  27973  hhip  28004  hhph  28005  norm1exi  28077  hhssabloilem  28088  hhssnv  28091  hhshsslem2  28095  hhssmetdval  28105  shscli  28146  shunssi  28197  shsleji  28199  shsidmi  28213  spanunsni  28408  h1datomi  28410  spansncvi  28481  pjss2i  28509  pjssmii  28510  pjocini  28527  homulid2  28629  honegdi  28638  ho2times  28648  nmopge0  28740  nmopgt0  28741  nmfnge0  28756  lnopaddi  28800  lnopmuli  28801  lnopsubi  28803  hmopbdoptHIL  28817  nmbdoplbi  28853  nmcoplbi  28857  nmophmi  28860  lnopconi  28863  lnfnaddi  28872  lnfnsubi  28875  nmbdfnlbi  28878  nmcfnlbi  28881  lnfnconi  28884  imaelshi  28887  cnlnadjlem2  28897  cnlnadjlem7  28902  nmoptrii  28923  nmopcoi  28924  adjcoi  28929  nmopcoadji  28930  bracnlnval  28943  leopmul  28963  opsqrlem1  28969  opsqrlem6  28974  hmopidmpji  28981  sto2i  29066  strlem1  29079  atcveq0  29177  atcv0eq  29208  atomli  29211  atcvati  29215  atcvat3i  29225  cdjreui  29261  cdj1i  29262  xdiv0  29611  xdivpnfrp  29615  mhmhmeotmd  29947  rezh  29989  qqhucn  30010  blsconn  31200  cnllysconn  31201  sinccvglem  31540  frrlem11  31766  nosupno  31823  nosupbday  31825  noetalem3  31839  opnrebl2  32291  ptrecube  33380  poimirlem6  33386  poimirlem7  33387  poimirlem29  33409  poimirlem30  33410  opnmbllem0  33416  mblfinlem3  33419  mblfinlem4  33420  ismblfin  33421  voliunnfl  33424  ftc1anclem5  33460  ftc1anclem6  33461  ftc1anclem7  33462  ftc1anclem8  33463  ftc1anc  33464  heiborlem7  33587  rrnequiv  33605  ismrer1  33608  cnaddcom  34078  mapco2  37097  mzpaddmpt  37123  mzpmulmpt  37124  zindbi  37330  mpaaeu  37539  eel000cT  38748  eel0TT  38749  supminfxr  39507  fmtno4prmfac  41249  zringsubgval  41948  aacllem  42312
  Copyright terms: Public domain W3C validator