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

Theorem mpan2d 705
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 450 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpid 42 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  mpand  706  mpan2i  708  ralxfrd  4800  ralxfrdOLD  4801  ralxfrd2  4805  sotri3  5432  oeordi  7532  xpfi  8094  alephle  8772  axdc3lem4  9136  dedekindle  10053  addlsub  10299  letrp1  10717  ledivp1  10777  peano2uz2  11300  uzind  11304  xrre  11836  xrre2  11837  xrltmin  11849  xrlemin  11851  lemaxle  11862  xralrple  11872  xlemul1a  11950  xrinfmsslem  11969  flge  12426  flflp1  12428  fsequb  12594  seqcl2  12639  monoord  12651  facwordi  12896  facavg  12908  sqrlem6  13785  leabs  13836  caubnd  13895  limsupgre  14009  limsupbnd2  14011  lo1bdd2  14052  lo1bddrp  14053  o1lo1  14065  o1rlimmul  14146  lo1mul  14155  isercolllem2  14193  climcndslem1  14369  climcndslem2  14370  ruclem3  14750  ruclem9  14755  ruclem12  14758  dvdsmultr1  14806  ltoddhalfle  14872  divalglem0  14903  dvdsgcdb  15049  dfgcd2  15050  coprmgcdb  15149  coprmdvds2  15155  exprmfct  15203  prmdvdsfz  15204  prmfac1  15218  rpexp  15219  eulerthlem2  15274  pcpremul  15335  pcdvdsb  15360  pcprmpw2  15373  pockthlem  15396  prmreclem3  15409  4sqlem11  15446  vdwnnlem3  15488  meetle  16800  latjlej1  16837  latnlej2  16843  clatleglb  16898  mndodconglem  17732  efgsrel  17919  ablfac1b  18241  pgpfac1lem1  18245  lbsextlem2  18929  chfacfscmul0  20430  chfacfpmmul0  20434  lmcls  20864  ufileu  21481  ufilcmp  21594  cnpfcf  21603  tsmsxp  21716  prdsbl  22054  reconnlem2  22386  evth  22514  ivthlem2  22973  ivthlem3  22974  ovollb2lem  23008  ovoliunlem2  23023  ovolicc2lem3  23039  ismbf3d  23172  itg2seq  23260  itg2monolem1  23268  dvcnvrelem1  23529  itgsubst  23561  plypf1  23717  coeaddlem  23754  coemullem  23755  ulmcau  23898  abelth  23944  wilth  24542  ftalem2  24545  ftalem3  24546  muval1  24604  dvdssqf  24609  sqff1o  24653  chtub  24682  bposlem3  24756  lgsne0  24805  gausslemma2dlem1a  24835  gausslemma2dlem2  24837  lgseisenlem1  24845  lgseisenlem2  24846  lgsquadlem1  24850  lgsquadlem2  24851  lgsquadlem3  24852  lgsquad2lem1  24854  lgsquad2lem2  24855  dchrisum0lem1  24950  pntlem3  25043  ex-natded5.8-2  26457  nmoub3i  26846  ubthlem1  26944  ubthlem2  26945  shsel1  27398  nmopub2tALT  27986  nmfnleub2  28003  lnconi  28110  eulerpartlemb  29591  dfon2lem4  30769  btwncomim  31124  nn0prpwlem  31321  ltflcei  32391  poimirlem9  32412  poimirlem18  32421  poimirlem21  32424  poimirlem22  32425  poimirlem24  32427  poimirlem29  32432  heicant  32438  mbfresfi  32450  itg2addnclem2  32456  itg2addnclem3  32457  incsequz  32538  heibor1lem  32602  atlelt  33566  1cvratex  33601  dalem3  33792  linepsubN  33880  pmapsub  33896  2llnma3r  33916  cdlemblem  33921  pmapjoin  33980  atmod1i1  33985  atmod1i2  33987  llnmod1i2  33988  lhpmcvr4N  34154  4atexlemnclw  34198  cdlemd3  34329  cdleme3g  34363  cdleme3h  34364  cdleme7d  34375  cdleme7ga  34377  cdleme21c  34457  cdleme35fnpq  34579  cdleme35f  34584  cdlemf1  34691  cdlemg4  34747  cdlemg6c  34750  cdlemg27a  34822  cdlemg33b0  34831  cdlemg33a  34836  cdlemk3  34963  dia2dimlem1  35195  dvheveccl  35243  dihord6apre  35387  dihord6b  35391  coprmdvdsb  36394  stoweid  38780  smonoord  39769  iccpartgt  39790  goldbachthlem2  39821  lighneallem2  39886  tgoldbach  40057  tgoldbachOLD  40064  upgrewlkle2  40830  pthdlem1  40994  crctcsh1wlkn0lem3  41037  nn0sumltlt  41943  dignn0flhalflem1  42229
  Copyright terms: Public domain W3C validator