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

Theorem mpan2d 690
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 416 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpid 44 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:  mpand  691  mpan2i  693  ralxfrd  5300  ralxfrd2  5304  sotri3  5984  oeordi  8203  xpfi  8778  alephle  9503  axdc3lem4  9864  dedekindle  10793  addlsub  11045  letrp1  11473  ledivp1  11531  peano2uz2  12059  uzind  12063  xrre  12552  xrre2  12553  xrltmin  12565  xrlemin  12567  lemaxle  12578  xralrple  12588  xlemul1a  12671  xrinfmsslem  12691  flge  13165  flflp1  13167  fsequb  13333  seqcl2  13378  monoord  13390  facwordi  13639  facavg  13651  sqrlem6  14597  leabs  14649  caubnd  14708  limsupgre  14828  limsupbnd2  14830  lo1bdd2  14871  lo1bddrp  14872  o1lo1  14884  o1rlimmul  14965  lo1mul  14974  isercolllem2  15012  climcndslem1  15194  climcndslem2  15195  ruclem3  15576  ruclem9  15581  ruclem12  15584  dvdsmultr1  15637  ltoddhalfle  15700  divalglem0  15734  dvdsgcdb  15883  dfgcd2  15884  coprmgcdb  15983  coprmdvds2  15988  exprmfct  16038  prmdvdsfz  16039  prmfac1  16053  rpexp  16054  eulerthlem2  16109  pcpremul  16170  pcdvdsb  16195  pcprmpw2  16208  pockthlem  16231  prmreclem3  16244  4sqlem11  16281  vdwnnlem3  16323  meetle  17628  latjlej1  17665  latnlej2  17671  clatleglb  17726  mndodconglem  18600  efgsrel  18791  ablfac1b  19123  pgpfac1lem1  19127  lbsextlem2  19862  chfacfscmul0  21396  chfacfpmmul0  21400  lmcls  21840  ufileu  22457  ufilcmp  22570  cnpfcf  22579  tsmsxp  22692  prdsbl  23030  reconnlem2  23364  evth  23492  ivthlem2  23982  ivthlem3  23983  ovollb2lem  24018  ovoliunlem2  24033  ovolicc2lem3  24049  ismbf3d  24184  itg2seq  24272  itg2monolem1  24280  dvcnvrelem1  24543  itgsubst  24575  plypf1  24731  coeaddlem  24768  coemullem  24769  ulmcau  24912  abelth  24958  wilth  25576  ftalem2  25579  ftalem3  25580  muval1  25638  dvdssqf  25643  sqff1o  25687  chtub  25716  bposlem3  25790  lgsne0  25839  gausslemma2dlem1a  25869  gausslemma2dlem2  25871  lgseisenlem1  25879  lgseisenlem2  25880  lgsquadlem1  25884  lgsquadlem2  25885  lgsquadlem3  25886  lgsquad2lem1  25888  lgsquad2lem2  25889  dchrisum0lem1  26020  pntlem3  26113  upgrewlkle2  27316  pthdlem1  27475  crctcshwlkn0lem3  27518  ex-natded5.8-2  28121  nmoub3i  28478  ubthlem1  28575  ubthlem2  28576  shsel1  29026  nmopub2tALT  29614  nmfnleub2  29631  lnconi  29738  eulerpartlemb  31526  dfon2lem4  32929  btwncomim  33372  nn0prpwlem  33568  ltflcei  34762  poimirlem9  34783  poimirlem18  34792  poimirlem21  34795  poimirlem22  34796  poimirlem24  34798  poimirlem29  34803  heicant  34809  mbfresfi  34820  itg2addnclem2  34826  itg2addnclem3  34827  incsequz  34906  heibor1lem  34970  atlelt  36456  1cvratex  36491  dalem3  36682  linepsubN  36770  pmapsub  36786  2llnma3r  36806  cdlemblem  36811  pmapjoin  36870  atmod1i1  36875  atmod1i2  36877  llnmod1i2  36878  lhpmcvr4N  37044  4atexlemnclw  37088  cdlemd3  37218  cdleme3g  37252  cdleme3h  37253  cdleme7d  37264  cdleme7ga  37266  cdleme21c  37345  cdleme35fnpq  37467  cdleme35f  37472  cdlemf1  37579  cdlemg4  37635  cdlemg6c  37638  cdlemg27a  37710  cdlemg33b0  37719  cdlemg33a  37724  cdlemk3  37851  dia2dimlem1  38082  dvheveccl  38130  dihord6apre  38274  dihord6b  38278  coprmdvdsb  39462  harval3  39784  monoordxrv  41638  stoweid  42229  smonoord  43412  iccpartgt  43434  goldbachthlem2  43555  lighneallem2  43618  tgoldbach  43829  nn0sumltlt  44296  dignn0flhalflem1  44573
  Copyright terms: Public domain W3C validator