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

Theorem mp3an3 1443
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 1115 . 2 ((𝜑𝜓) → (𝜒𝜃))
41, 3mpi 20 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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  df-3an 1083
This theorem is referenced by:  mp3an13  1445  mp3an23  1446  mp3anl3  1450  opelxp  5589  ov  7287  ovmpoa  7298  ovmpo  7303  oaword1  8171  oneo  8200  oeoalem  8215  oeoelem  8217  nnaword1  8248  nnneo  8271  erov  8387  enrefg  8533  f1imaen  8563  mapxpen  8675  acnlem  9466  djucomen  9595  infmap  9990  canthnumlem  10062  tskin  10173  tsksn  10174  tsk0  10177  gruxp  10221  gruina  10232  genpprecl  10415  addsrpr  10489  mulsrpr  10490  supsrlem  10525  mulid1  10631  00id  10807  mul02lem1  10808  ltneg  11132  leneg  11135  suble0  11146  div1  11321  nnaddcl  11652  nnmulcl  11653  nnge1  11657  nnsub  11673  2halves  11857  halfaddsub  11862  addltmul  11865  zleltp1  12025  nnaddm1cl  12031  zextlt  12048  eluzp1p1  12262  uzaddcl  12296  znq  12344  xrre  12555  xrre2  12556  fzshftral  12988  fraclt1  13165  expadd  13464  expmul  13467  sqmul  13478  expubnd  13534  bernneq  13583  faclbnd2  13644  faclbnd6  13652  hashgadd  13731  hashun2  13737  hashunsnggt  13748  hashssdif  13766  hashfun  13791  ccatlcan  14073  ccatrcan  14074  pfx2  14302  shftval3  14428  sqrlem1  14595  caubnd2  14710  bpoly2  15403  bpoly3  15404  fsumcube  15406  efexp  15446  efival  15497  cos01gt0  15536  odd2np1  15682  halfleoddlt  15703  omoe  15705  opeo  15706  divalglem5  15740  gcdmultipleOLD  15892  sqgcd  15901  nn0seqcvgd  15906  phiprmpw  16105  eulerthlem2  16111  odzcllem  16121  pythagtriplem15  16158  pythagtriplem17  16160  pcelnn  16198  4sqlem3  16278  fullfunc  17168  fthfunc  17169  prfcl  17445  curf1cl  17470  curfcl  17474  hofcl  17501  odinv  18610  lsmelvalix  18688  dprdval  19047  lsp0  19703  lss0v  19710  coe1scl  20372  zndvds0  20613  frlmlbs  20857  lindfres  20883  lmisfree  20902  ntrin  21585  lpsscls  21665  restperf  21708  txuni2  22089  txopn  22126  elqtop2  22225  xkocnv  22338  ptcmp  22582  xblpnfps  22920  xblpnf  22921  bl2in  22925  unirnblps  22944  unirnbl  22945  blpnfctr  22961  dscopn  23098  bcthlem4  23845  minveclem2  23944  minveclem4  23950  icombl  24080  i1fadd  24211  i1fmul  24212  dvn1  24438  dvexp3  24490  plyconst  24711  plyid  24714  sincosq1eq  25013  sinord  25031  cxpp1  25176  cxpsqrtlem  25198  cxpsqrt  25199  angneg  25294  dcubic  25337  issqf  25627  ppiub  25694  bposlem1  25774  bposlem2  25775  bposlem9  25782  axlowdimlem6  26647  axlowdimlem14  26655  axcontlem2  26665  pthdlem2  27463  0ewlk  27807  ipasslem1  28522  ipasslem2  28523  ipasslem11  28531  minvecolem2  28566  minvecolem3  28567  minvecolem4  28571  shsva  29011  h1datomi  29272  lnfnmuli  29735  leopsq  29820  nmopleid  29830  opsqrlem6  29836  pjnmopi  29839  hstle  29921  csmdsymi  30025  atcvatlem  30076  dpfrac1  30482  cshf1o  30550  cycpmconjslem2  30711  elsx  31339  dya2iocnrect  31425  cvmliftphtlem  32448  satfv1  32494  satffunlem1lem2  32534  satffunlem1  32538  wlimeq12  32990  frecseq123  33003  nosupno  33087  nosupfv  33090  scutval  33149  scutun12  33155  fvray  33486  fvline  33489  tailfb  33609  uncov  34740  tan2h  34751  matunitlindflem1  34755  matunitlindflem2  34756  poimirlem32  34791  mblfinlem4  34799  mbfresfi  34805  mbfposadd  34806  itg2addnc  34813  ftc1anclem5  34838  ftc1anclem8  34841  dvasin  34845  heiborlem7  34963  igenidl  35209  el3v3  35362  atlatmstc  36322  dihglblem2N  38297  eldioph4b  39269  diophren  39271  rmxp1  39390  rmyp1  39391  rmxm1  39392  rmym1  39393  wepwso  39504  dig0  44494  onetansqsecsq  44688  cotsqcscsq  44689
  Copyright terms: Public domain W3C validator