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

Theorem mp3an3 1451
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an3.1 𝜒
mp3an3.2 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an3 ((𝜑𝜓) → 𝜃)

Proof of Theorem mp3an3
StepHypRef Expression
1 mp3an3.1 . 2 𝜒
2 mp3an3.2 . . 3 ((𝜑𝜓𝜒) → 𝜃)
323expia 1122 . 2 ((𝜑𝜓) → (𝜒𝜃))
41, 3mpi 20 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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  df-3an 1090
This theorem is referenced by:  mp3an13  1453  mp3an23  1454  mp3anl3  1458  opelxp  5670  ov  7500  ovmpoa  7511  ovmpo  7516  frecseq123  8214  oaword1  8500  oneo  8529  oeoalem  8544  oeoelem  8546  nnaword1  8577  nnneo  8602  erov  8754  enrefg  8925  f1imaen  8957  mapxpen  9088  0sdom1dom  9183  acnlem  9985  djucomen  10114  nnadju  10134  infmap  10513  canthnumlem  10585  tskin  10696  tsksn  10697  tsk0  10700  gruxp  10744  gruina  10755  genpprecl  10938  addsrpr  11012  mulsrpr  11013  supsrlem  11048  mulid1  11154  00id  11331  mul02lem1  11332  ltneg  11656  leneg  11659  suble0  11670  div1  11845  nnaddcl  12177  nnmulcl  12178  nnge1  12182  nnsub  12198  2halves  12382  halfaddsub  12387  addltmul  12390  fcdmnn0fsuppg  12473  zleltp1  12555  nnaddm1cl  12561  zextlt  12578  eluzp1p1  12792  uzaddcl  12830  znq  12878  xrre  13089  xrre2  13090  fzshftral  13530  fraclt1  13708  expadd  14011  expmul  14014  sqmul  14025  expubnd  14083  bernneq  14133  faclbnd2  14192  faclbnd6  14200  hashgadd  14278  hashun2  14284  hashunsnggt  14295  hashssdif  14313  hashfun  14338  ccatlcan  14607  ccatrcan  14608  pfx2  14837  shftval3  14962  01sqrexlem1  15128  caubnd2  15243  bpoly2  15941  bpoly3  15942  fsumcube  15944  efexp  15984  efival  16035  cos01gt0  16074  odd2np1  16224  halfleoddlt  16245  omoe  16247  opeo  16248  divalglem5  16280  sqgcd  16442  nn0seqcvgd  16447  prmdvdssq  16595  phiprmpw  16649  eulerthlem2  16655  odzcllem  16665  pythagtriplem15  16702  pythagtriplem17  16704  pcelnn  16743  4sqlem3  16823  fullfunc  17794  fthfunc  17795  prfcl  18092  curf1cl  18118  curfcl  18122  hofcl  18149  odinv  19344  lsmelvalix  19424  dprdval  19783  lsp0  20473  lss0v  20480  zndvds0  20960  frlmlbs  21206  lindfres  21232  lmisfree  21251  coe1scl  21661  ntrin  22415  lpsscls  22495  restperf  22538  txuni2  22919  txopn  22956  elqtop2  23055  xkocnv  23168  ptcmp  23412  xblpnfps  23751  xblpnf  23752  bl2in  23756  unirnblps  23775  unirnbl  23776  blpnfctr  23792  dscopn  23932  bcthlem4  24694  minveclem2  24793  minveclem4  24799  icombl  24931  i1fadd  25062  i1fmul  25063  dvn1  25293  dvexp3  25345  plyconst  25570  plyid  25573  sincosq1eq  25872  sinord  25893  cxpp1  26038  cxpsqrtlem  26060  cxpsqrt  26061  angneg  26156  dcubic  26199  issqf  26488  ppiub  26555  bposlem1  26635  bposlem2  26636  bposlem9  26643  nosupno  27054  nosupfv  27057  noinfno  27069  noinffv  27072  scutval  27142  scutun12  27152  cuteq0  27174  cofcut1  27242  cofcutr  27246  sleadd1  27301  addsunif  27313  addsasslem1  27314  addsasslem2  27315  negscut2  27341  axlowdimlem6  27899  axlowdimlem14  27907  axcontlem2  27917  pthdlem2  28719  0ewlk  29061  ipasslem1  29776  ipasslem2  29777  ipasslem11  29785  minvecolem2  29820  minvecolem3  29821  minvecolem4  29825  shsva  30265  h1datomi  30526  lnfnmuli  30989  leopsq  31074  nmopleid  31084  opsqrlem6  31090  pjnmopi  31093  hstle  31175  csmdsymi  31279  atcvatlem  31330  dpfrac1  31751  cshf1o  31819  cycpmconjslem2  32007  rspidlid  32166  elsx  32796  dya2iocnrect  32884  cvmliftphtlem  33914  satfv1  33960  satffunlem1lem2  34000  satffunlem1  34004  wlimeq12  34397  fvray  34729  fvline  34732  tailfb  34852  uncov  36062  tan2h  36073  matunitlindflem1  36077  matunitlindflem2  36078  poimirlem32  36113  mblfinlem4  36121  mbfresfi  36127  mbfposadd  36128  itg2addnc  36135  ftc1anclem5  36158  ftc1anclem8  36161  dvasin  36165  heiborlem7  36279  igenidl  36525  el3v3  36683  atlatmstc  37784  dihglblem2N  39760  2xp3dxp2ge1d  40617  factwoffsmonot  40618  eldioph4b  41137  diophren  41139  rmxp1  41259  rmyp1  41260  rmxm1  41261  rmym1  41262  dig0  46699  i0oii  46959  onetansqsecsq  47213  cotsqcscsq  47214
  Copyright terms: Public domain W3C validator