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

Theorem mp2and 695
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mp2and.1 (𝜑𝜓)
mp2and.2 (𝜑𝜒)
mp2and.3 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
mp2and (𝜑𝜃)

Proof of Theorem mp2and
StepHypRef Expression
1 mp2and.2 . 2 (𝜑𝜒)
2 mp2and.1 . . 3 (𝜑𝜓)
3 mp2and.3 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
42, 3mpand 691 . 2 (𝜑 → (𝜒𝜃))
51, 4mpd 15 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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
This theorem is referenced by:  reu2eqd  3726  ssnelpssd  4088  tfisi  7561  tfindsg2  7564  mposn  7789  smoord  7993  oelimcl  8216  oeeui  8218  nnawordex  8253  omabs  8264  ertrd  8295  omxpenlem  8607  ixpfi2  8811  oismo  8993  cantnflem1c  9139  cantnflem1  9141  cantnflem3  9143  infxpenc2  9437  isfin2-2  9730  axdc2lem  9859  r1limwun  10147  letrd  10786  lelttrd  10787  ltletrd  10789  lttrd  10790  le2addd  11248  le2subd  11249  ltleaddd  11250  leltaddd  11251  lt2subd  11253  ltmul12a  11485  lemul12ad  11571  lemul12bd  11572  lt2halvesd  11874  uzind  12063  uztrn  12250  xrlttrd  12542  xrlelttrd  12543  xrltletrd  12544  xrletrd  12545  supxrunb1  12702  supxrunb2  12703  ixxun  12744  ixxss1  12746  ixxss2  12747  ixxss12  12748  fldiv4p1lem1div2  13195  fldiv4lem1div2uz2  13196  seqf1o  13401  faclbnd3  13642  rtrclreclem3  14409  relexpindlem  14412  sqrlem1  14592  sqrlem4  14595  sqrlem7  14598  abs3lemd  14811  rlimcn2  14937  o1of2  14959  lo1add  14973  lo1mul  14974  modfsummod  15139  mertenslem1  15230  sin01gt0  15533  cos01gt0  15534  sin02gt0  15535  dvds2subd  15635  bitsmod  15775  sadaddlem  15805  bezoutlem4  15880  mulgcd  15886  gcddvdslcm  15936  lcmgcdeq  15946  lcmfunsnlem2lem2  15973  mulgcddvds  15989  rpmulgcd2  15990  rpdvds  15994  divgcdcoprmex  16000  isprm5  16041  rpexp  16054  phimullem  16106  eulerthlem1  16108  eulerthlem2  16109  prmdiveq  16113  pythagtriplem4  16146  pcpremul  16170  pcqmul  16180  pcdvdstr  16202  pcgcd1  16203  pcadd  16215  pockthlem  16231  prmreclem2  16243  4sqlem8  16271  4sqlem14  16284  4sqlem16  16286  ramub1lem1  16352  ramub1lem2  16353  prmdvdsprmop  16369  prmgaplem1  16375  prmgaplcmlem1  16377  prmgaplem7  16383  iscatd2  16942  cicsym  17064  initoeu2  17266  joinval  17605  meetval  17619  lattrd  17658  latledi  17689  mulgass  18204  gaorber  18378  psgnunilem4  18556  efgredlem  18804  odadd2  18900  dmdprdpr  19102  ablfacrp2  19120  ablfac1b  19123  ablfac1eu  19126  pgpfac1  19133  gsumbagdiaglem  20085  znunit  20640  mdetunilem1  21151  mdetunilem4  21154  mdetunilem9  21159  neiptoptop  21669  lmcnp  21842  txcls  22142  txlly  22174  txnlly  22175  tx1stc  22188  alexsubALTlem1  22585  prdsmet  22909  blin2  22968  blcvx  23335  tgqioo  23337  metnrmlem3  23398  iscmet3lem2  23824  ovolmge0  24007  ovolunlem2  24028  mbfi1flimlem  24252  mbfmullem  24255  itg2add  24289  dvferm1lem  24510  dvferm2lem  24512  dvlip2  24521  dvge0  24532  dvcvx  24546  dvfsumabs  24549  ftc1a  24563  plyadd  24736  plymul  24737  dgrlb  24755  plydivlem4  24814  vieta1lem2  24829  ulmdvlem3  24919  sinq12gt0  25022  logdivlti  25130  fsumharmonic  25517  fsumdvdsdiaglem  25688  dvdsmulf1o  25699  logfacubnd  25725  perfectlem1  25733  dchrptlem2  25769  lgsmod  25827  2sqlem3  25924  2sqlem5  25926  2sqlem8  25930  2sqmod  25940  dchrisum0flblem2  26013  pntibndlem2  26095  pntlemr  26106  pntlemp  26114  axtgpasch  26181  tgjustr  26188  wlkcompim  27341  wwlksnredwwlkn  27601  wwlksnextsurj  27606  upgr4cycl4dv4e  27892  ex-natded5.2-2  28112  chscllem2  29343  chscllem4  29345  nmopge0  29616  nmfnge0  29632  nmoptrii  29799  staddi  29951  stadd3i  29953  atcvatlem  30090  supssd  30372  infssd  30373  xrofsup  30419  xrge0addgt0  30606  archiabllem2c  30752  orngmul  30804  linds2eq  30869  lbsdiflsp0  30922  fedgmullem2  30926  esumpmono  31238  unelldsys  31317  omssubaddlem  31457  signstfvneq0  31742  axtgupdim2ALTV  31839  bnj1098  31955  bnj1110  32152  bnj1121  32155  0nn0m1nnn0  32249  cplgredgex  32265  erdszelem8  32343  txsconn  32386  cvmlift2lem10  32457  cvmlift3lem7  32470  dvdspw  32880  sotrd  32899  dfon2lem6  32931  dfon2lem8  32933  frpomin  32976  nosupbnd1  33112  nosupbnd2lem1  33113  nosupbnd2  33114  noetalem3  33117  slttrd  33136  sltletrd  33137  slelttrd  33138  sletrd  33139  cgrtr4d  33344  cgrtrand  33352  cgrtr3and  33354  cgrextendand  33368  btwnexch3and  33380  btwnexchand  33385  linecgrand  33441  endofsegidand  33445  btwnconn1lem4  33449  btwnconn1lem8  33453  btwnconn1lem11  33456  btwnconn1lem12  33457  brsegle2  33468  seglecgr12im  33469  segleantisym  33474  colinbtwnle  33477  broutsideof2  33481  outsideoftr  33488  outsidele  33491  lineelsb2  33507  linethru  33512  gtinf  33565  copsex2d  34324  relowlssretop  34527  pibt2  34581  heicant  34809  mbfresfi  34820  ftc1anclem6  34854  eqvreltrd  35725  riotasv2d  35975  lcvnbtwn2  36045  lcvnbtwn3  36046  lcvexchlem4  36055  omlfh1N  36276  atlen0  36328  atlatmstc  36337  cvratlem  36439  lnnat  36445  2atlt  36457  athgt  36474  1cvratex  36491  ps-2  36496  llncmp  36540  llncvrlpln  36576  lplncmp  36580  lplncvrlvol  36634  lvolcmp  36635  dalemcea  36678  dalem-cly  36689  dalem10  36691  dalem17  36698  dalem25  36716  dalem38  36728  dalem44  36734  dalem55  36745  2atm2atN  36803  cdlema1N  36809  paddasslem5  36842  dalawlem3  36891  dalawlem7  36895  dalawlem11  36899  dalawlem12  36900  lhp0lt  37021  4atexlemc  37087  cdlemg33a  37724  cdlemg33  37729  cdlemk51  37971  dia2dimlem2  38083  dia2dimlem3  38084  dihmeetlem20N  38344  ismrcd2  39176  pellqrex  39356  jm2.17b  39438  dvdsacongtr  39461  jm2.26lem3  39478  jm2.27a  39482  jm2.27c  39484  fnwe2lem2  39531  addrcom  40687  infxrunb2  41516  0ellimcdiv  41810  stoweidlem15  42181  stoweidlem26  42192  stoweidlem28  42194  stoweidlem32  42198  stoweidlem44  42210  meadjuni  42620  dfatcolem  43335  icceuelpart  43443  perfectALTVlem1  43733  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  copisnmnd  43923  symgsubmefmndALT  43966  assintopass  44019  lcoss  44389  islindeps2  44436  isldepslvec2  44438  difmodm1lt  44480
  Copyright terms: Public domain W3C validator