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

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

Proof of Theorem mpan2d
StepHypRef Expression
1 mpan2d.1 . 2 (𝜑𝜒)
2 mpan2d.2 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
32expd 451 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpid 44 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  mpand  711  mpan2i  713  ralxfrd  4909  ralxfrdOLD  4910  ralxfrd2  4914  sotri3  5561  oeordi  7712  xpfi  8272  alephle  8949  axdc3lem4  9313  dedekindle  10239  addlsub  10485  letrp1  10903  ledivp1  10963  peano2uz2  11503  uzind  11507  xrre  12038  xrre2  12039  xrltmin  12051  xrlemin  12053  lemaxle  12064  xralrple  12074  xlemul1a  12156  xrinfmsslem  12176  flge  12646  flflp1  12648  fsequb  12814  seqcl2  12859  monoord  12871  facwordi  13116  facavg  13128  sqrlem6  14032  leabs  14083  caubnd  14142  limsupgre  14256  limsupbnd2  14258  lo1bdd2  14299  lo1bddrp  14300  o1lo1  14312  o1rlimmul  14393  lo1mul  14402  isercolllem2  14440  climcndslem1  14625  climcndslem2  14626  ruclem3  15006  ruclem9  15011  ruclem12  15014  dvdsmultr1  15066  ltoddhalfle  15132  divalglem0  15163  dvdsgcdb  15309  dfgcd2  15310  coprmgcdb  15409  coprmdvds2  15415  exprmfct  15463  prmdvdsfz  15464  prmfac1  15478  rpexp  15479  eulerthlem2  15534  pcpremul  15595  pcdvdsb  15620  pcprmpw2  15633  pockthlem  15656  prmreclem3  15669  4sqlem11  15706  vdwnnlem3  15748  meetle  17075  latjlej1  17112  latnlej2  17118  clatleglb  17173  mndodconglem  18006  efgsrel  18193  ablfac1b  18515  pgpfac1lem1  18519  lbsextlem2  19207  chfacfscmul0  20711  chfacfpmmul0  20715  lmcls  21154  ufileu  21770  ufilcmp  21883  cnpfcf  21892  tsmsxp  22005  prdsbl  22343  reconnlem2  22677  evth  22805  ivthlem2  23267  ivthlem3  23268  ovollb2lem  23302  ovoliunlem2  23317  ovolicc2lem3  23333  ismbf3d  23466  itg2seq  23554  itg2monolem1  23562  dvcnvrelem1  23825  itgsubst  23857  plypf1  24013  coeaddlem  24050  coemullem  24051  ulmcau  24194  abelth  24240  wilth  24842  ftalem2  24845  ftalem3  24846  muval1  24904  dvdssqf  24909  sqff1o  24953  chtub  24982  bposlem3  25056  lgsne0  25105  gausslemma2dlem1a  25135  gausslemma2dlem2  25137  lgseisenlem1  25145  lgseisenlem2  25146  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  lgsquad2lem1  25154  lgsquad2lem2  25155  dchrisum0lem1  25250  pntlem3  25343  upgrewlkle2  26558  pthdlem1  26718  crctcshwlkn0lem3  26760  ex-natded5.8-2  27401  nmoub3i  27756  ubthlem1  27854  ubthlem2  27855  shsel1  28308  nmopub2tALT  28896  nmfnleub2  28913  lnconi  29020  eulerpartlemb  30558  dfon2lem4  31815  btwncomim  32245  nn0prpwlem  32442  ltflcei  33527  poimirlem9  33548  poimirlem18  33557  poimirlem21  33560  poimirlem22  33561  poimirlem24  33563  poimirlem29  33568  heicant  33574  mbfresfi  33586  itg2addnclem2  33592  itg2addnclem3  33593  incsequz  33674  heibor1lem  33738  atlelt  35042  1cvratex  35077  dalem3  35268  linepsubN  35356  pmapsub  35372  2llnma3r  35392  cdlemblem  35397  pmapjoin  35456  atmod1i1  35461  atmod1i2  35463  llnmod1i2  35464  lhpmcvr4N  35630  4atexlemnclw  35674  cdlemd3  35805  cdleme3g  35839  cdleme3h  35840  cdleme7d  35851  cdleme7ga  35853  cdleme21c  35932  cdleme35fnpq  36054  cdleme35f  36059  cdlemf1  36166  cdlemg4  36222  cdlemg6c  36225  cdlemg27a  36297  cdlemg33b0  36306  cdlemg33a  36311  cdlemk3  36438  dia2dimlem1  36670  dvheveccl  36718  dihord6apre  36862  dihord6b  36866  coprmdvdsb  37869  monoordxrv  40025  stoweid  40598  smonoord  41666  iccpartgt  41688  goldbachthlem2  41783  lighneallem2  41848  tgoldbach  42030  tgoldbachOLD  42037  nn0sumltlt  42453  dignn0flhalflem1  42734
  Copyright terms: Public domain W3C validator