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 417 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpid 44 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  mpand  694  mpan2i  696  ralxfrd  5364  ralxfrd2  5368  sotri3  6085  predtrss  6277  oeordi  8535  coflton  8618  cofon1  8619  cofon2  8620  xpfiOLD  9263  ttrclss  9657  alephle  10025  axdc3lem4  10390  dedekindle  11320  addlsub  11572  letrp1  12000  ledivp1  12058  peano2uz2  12592  uzind  12596  xrre  13089  xrre2  13090  xrltmin  13102  xrlemin  13104  lemaxle  13115  xralrple  13125  xlemul1a  13208  xrinfmsslem  13228  flge  13711  flflp1  13713  fsequb  13881  seqcl2  13927  monoord  13939  facwordi  14190  facavg  14202  01sqrexlem6  15133  leabs  15185  caubnd  15244  limsupgre  15364  limsupbnd2  15366  lo1bdd2  15407  lo1bddrp  15408  o1lo1  15420  o1rlimmul  15502  lo1mul  15511  isercolllem2  15551  climcndslem1  15735  climcndslem2  15736  ruclem3  16116  ruclem9  16121  ruclem12  16124  dvdsmultr1  16179  ltoddhalfle  16244  divalglem0  16276  dvdsgcdb  16427  dfgcd2  16428  coprmgcdb  16526  coprmdvds2  16531  exprmfct  16581  prmdvdsfz  16582  prmfac1  16598  rpexp  16599  eulerthlem2  16655  pcpremul  16716  pcdvdsb  16742  pcprmpw2  16755  pockthlem  16778  prmreclem3  16791  4sqlem11  16828  vdwnnlem3  16870  meetle  18290  latjlej1  18343  latnlej2  18349  clatleglb  18408  mndodconglem  19324  efgsrel  19517  ablfac1b  19850  pgpfac1lem1  19854  lbsextlem2  20623  chfacfscmul0  22210  chfacfpmmul0  22214  lmcls  22656  ufileu  23273  ufilcmp  23386  cnpfcf  23395  tsmsxp  23509  prdsbl  23850  reconnlem2  24193  evth  24325  ivthlem2  24819  ivthlem3  24820  ovollb2lem  24855  ovoliunlem2  24870  ovolicc2lem3  24886  ismbf3d  25021  itg2seq  25110  itg2monolem1  25118  dvcnvrelem1  25384  itgsubst  25416  plypf1  25576  coeaddlem  25613  coemullem  25614  ulmcau  25757  abelth  25803  wilth  26423  ftalem2  26426  ftalem3  26427  muval1  26485  dvdssqf  26490  sqff1o  26534  chtub  26563  bposlem3  26637  lgsne0  26686  gausslemma2dlem1a  26716  gausslemma2dlem2  26718  lgseisenlem1  26726  lgseisenlem2  26727  lgsquadlem1  26731  lgsquadlem2  26732  lgsquadlem3  26733  lgsquad2lem1  26735  lgsquad2lem2  26736  dchrisum0lem1  26867  pntlem3  26960  upgrewlkle2  28557  pthdlem1  28717  crctcshwlkn0lem3  28760  ex-natded5.8-2  29361  nmoub3i  29718  ubthlem1  29815  ubthlem2  29816  shsel1  30266  nmopub2tALT  30854  nmfnleub2  30871  lnconi  30978  eulerpartlemb  32971  dfon2lem4  34364  btwncomim  34601  nn0prpwlem  34797  ltflcei  36069  poimirlem9  36090  poimirlem18  36099  poimirlem21  36102  poimirlem22  36103  poimirlem24  36105  poimirlem29  36110  heicant  36116  mbfresfi  36127  itg2addnclem2  36133  itg2addnclem3  36134  incsequz  36210  heibor1lem  36271  atlelt  37904  1cvratex  37939  dalem3  38130  linepsubN  38218  pmapsub  38234  2llnma3r  38254  cdlemblem  38259  pmapjoin  38318  atmod1i1  38323  atmod1i2  38325  llnmod1i2  38326  lhpmcvr4N  38492  4atexlemnclw  38536  cdlemd3  38666  cdleme3g  38700  cdleme3h  38701  cdleme7d  38712  cdleme7ga  38714  cdleme21c  38793  cdleme35fnpq  38915  cdleme35f  38920  cdlemf1  39027  cdlemg4  39083  cdlemg6c  39086  cdlemg27a  39158  cdlemg33b0  39167  cdlemg33a  39172  cdlemk3  39299  dia2dimlem1  39530  dvheveccl  39578  dihord6apre  39722  dihord6b  39726  coprmdvdsb  41312  harval3  41817  monoordxrv  43724  stoweid  44311  smonoord  45570  iccpartgt  45626  goldbachthlem2  45745  lighneallem2  45805  tgoldbach  46016  nn0sumltlt  46433  dignn0flhalflem1  46708
  Copyright terms: Public domain W3C validator