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

Theorem mpan2d 693
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 419 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpid 44 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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
This theorem is referenced by:  mpand  694  mpan2i  696  ralxfrd  5277  ralxfrd2  5281  sotri3  5961  oeordi  8200  xpfi  8777  alephle  9503  axdc3lem4  9868  dedekindle  10797  addlsub  11049  letrp1  11477  ledivp1  11535  peano2uz2  12062  uzind  12066  xrre  12554  xrre2  12555  xrltmin  12567  xrlemin  12569  lemaxle  12580  xralrple  12590  xlemul1a  12673  xrinfmsslem  12693  flge  13174  flflp1  13176  fsequb  13342  seqcl2  13388  monoord  13400  facwordi  13649  facavg  13661  sqrlem6  14603  leabs  14655  caubnd  14714  limsupgre  14834  limsupbnd2  14836  lo1bdd2  14877  lo1bddrp  14878  o1lo1  14890  o1rlimmul  14971  lo1mul  14980  isercolllem2  15018  climcndslem1  15200  climcndslem2  15201  ruclem3  15582  ruclem9  15587  ruclem12  15590  dvdsmultr1  15643  ltoddhalfle  15706  divalglem0  15738  dvdsgcdb  15887  dfgcd2  15888  coprmgcdb  15987  coprmdvds2  15992  exprmfct  16042  prmdvdsfz  16043  prmfac1  16057  rpexp  16058  eulerthlem2  16113  pcpremul  16174  pcdvdsb  16199  pcprmpw2  16212  pockthlem  16235  prmreclem3  16248  4sqlem11  16285  vdwnnlem3  16327  meetle  17634  latjlej1  17671  latnlej2  17677  clatleglb  17732  mndodconglem  18665  efgsrel  18856  ablfac1b  19189  pgpfac1lem1  19193  lbsextlem2  19928  chfacfscmul0  21467  chfacfpmmul0  21471  lmcls  21911  ufileu  22528  ufilcmp  22641  cnpfcf  22650  tsmsxp  22764  prdsbl  23102  reconnlem2  23436  evth  23568  ivthlem2  24060  ivthlem3  24061  ovollb2lem  24096  ovoliunlem2  24111  ovolicc2lem3  24127  ismbf3d  24262  itg2seq  24350  itg2monolem1  24358  dvcnvrelem1  24624  itgsubst  24656  plypf1  24813  coeaddlem  24850  coemullem  24851  ulmcau  24994  abelth  25040  wilth  25660  ftalem2  25663  ftalem3  25664  muval1  25722  dvdssqf  25727  sqff1o  25771  chtub  25800  bposlem3  25874  lgsne0  25923  gausslemma2dlem1a  25953  gausslemma2dlem2  25955  lgseisenlem1  25963  lgseisenlem2  25964  lgsquadlem1  25968  lgsquadlem2  25969  lgsquadlem3  25970  lgsquad2lem1  25972  lgsquad2lem2  25973  dchrisum0lem1  26104  pntlem3  26197  upgrewlkle2  27400  pthdlem1  27559  crctcshwlkn0lem3  27602  ex-natded5.8-2  28203  nmoub3i  28560  ubthlem1  28657  ubthlem2  28658  shsel1  29108  nmopub2tALT  29696  nmfnleub2  29713  lnconi  29820  eulerpartlemb  31740  dfon2lem4  33145  btwncomim  33588  nn0prpwlem  33784  ltflcei  35044  poimirlem9  35065  poimirlem18  35074  poimirlem21  35077  poimirlem22  35078  poimirlem24  35080  poimirlem29  35085  heicant  35091  mbfresfi  35102  itg2addnclem2  35108  itg2addnclem3  35109  incsequz  35185  heibor1lem  35246  atlelt  36733  1cvratex  36768  dalem3  36959  linepsubN  37047  pmapsub  37063  2llnma3r  37083  cdlemblem  37088  pmapjoin  37147  atmod1i1  37152  atmod1i2  37154  llnmod1i2  37155  lhpmcvr4N  37321  4atexlemnclw  37365  cdlemd3  37495  cdleme3g  37529  cdleme3h  37530  cdleme7d  37541  cdleme7ga  37543  cdleme21c  37622  cdleme35fnpq  37744  cdleme35f  37749  cdlemf1  37856  cdlemg4  37912  cdlemg6c  37915  cdlemg27a  37987  cdlemg33b0  37996  cdlemg33a  38001  cdlemk3  38128  dia2dimlem1  38359  dvheveccl  38407  dihord6apre  38551  dihord6b  38555  coprmdvdsb  39923  harval3  40241  monoordxrv  42118  stoweid  42702  smonoord  43885  iccpartgt  43941  goldbachthlem2  44060  lighneallem2  44121  tgoldbach  44332  nn0sumltlt  44749  dignn0flhalflem1  45026
  Copyright terms: Public domain W3C validator