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

Theorem mp3an3 1410
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 1264 . 2 ((𝜑𝜓) → (𝜒𝜃))
41, 3mpi 20 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  mp3an13  1412  mp3an23  1413  mp3anl3  1417  opelxp  5111  ov  6740  ovmpt2a  6751  ovmpt2  6756  oaword1  7584  oneo  7613  oeoalem  7628  oeoelem  7630  nnaword1  7661  nnneo  7683  erov  7796  enrefg  7939  f1imaen  7970  mapxpen  8078  acnlem  8823  cdacomen  8955  infmap  9350  canthnumlem  9422  tskin  9533  tsksn  9534  tsk0  9537  gruxp  9581  gruina  9592  genpprecl  9775  addsrpr  9848  mulsrpr  9849  supsrlem  9884  mulid1  9989  00id  10163  mul02lem1  10164  ltneg  10480  leneg  10483  suble0  10494  div1  10668  nnaddcl  10994  nnmulcl  10995  nnge1  10998  nnsub  11011  2halves  11212  halfaddsub  11217  addltmul  11220  zleltp1  11380  nnaddm1cl  11386  zextlt  11403  eluzp1p1  11665  uzaddcl  11696  znq  11744  xrre  11951  xrre2  11952  fzshftral  12377  fraclt1  12551  expadd  12850  expmul  12853  expubnd  12869  sqmul  12874  bernneq  12938  faclbnd2  13026  faclbnd6  13034  hashgadd  13114  hashun2  13120  hashssdif  13148  hashfun  13172  ccatlcan  13418  ccatrcan  13419  shftval3  13758  sqrlem1  13925  caubnd2  14039  bpoly2  14724  bpoly3  14725  fsumcube  14727  efexp  14767  efival  14818  cos01gt0  14857  odd2np1  15000  halfleoddlt  15021  omoe  15023  opeo  15024  divalglem5  15055  gcdmultiple  15204  sqgcd  15213  nn0seqcvgd  15218  phiprmpw  15416  eulerthlem2  15422  odzcllem  15432  pythagtriplem15  15469  pythagtriplem17  15471  pcelnn  15509  4sqlem3  15589  xpscfn  16151  fullfunc  16498  fthfunc  16499  prfcl  16775  curf1cl  16800  curfcl  16804  hofcl  16831  odinv  17910  lsmelvalix  17988  dprdval  18334  lsp0  18941  lss0v  18948  coe1scl  19589  zndvds0  19831  frlmlbs  20068  lindfres  20094  lmisfree  20113  ntrin  20788  lpsscls  20868  restperf  20911  txuni2  21291  txopn  21328  elqtop2  21427  xkocnv  21540  ptcmp  21785  xblpnfps  22123  xblpnf  22124  bl2in  22128  unirnblps  22147  unirnbl  22148  blpnfctr  22164  dscopn  22301  bcthlem4  23047  minveclem2  23120  minveclem4  23126  icombl  23255  i1fadd  23385  i1fmul  23386  dvn1  23612  dvexp3  23662  plyconst  23883  plyid  23886  sincosq1eq  24185  sinord  24201  cxpp1  24343  cxpsqrtlem  24365  cxpsqrt  24366  angneg  24450  dcubic  24490  issqf  24779  ppiub  24846  bposlem1  24926  bposlem2  24927  bposlem9  24934  axlowdimlem6  25744  axlowdimlem14  25752  axcontlem2  25762  structgrssvtxlemOLD  25832  pthdlem2  26550  0ewlk  26858  ipasslem1  27556  ipasslem2  27557  ipasslem11  27565  minvecolem2  27601  minvecolem3  27602  minvecolem4  27606  shsva  28049  h1datomi  28310  lnfnmuli  28773  leopsq  28858  nmopleid  28868  opsqrlem6  28874  pjnmopi  28877  hstle  28959  csmdsymi  29063  atcvatlem  29114  elsx  30062  dya2iocnrect  30148  cvmliftphtlem  31042  wlimeq12  31501  nosino  31610  nosifv  31611  fvray  31925  fvline  31928  tailfb  32049  uncov  33057  tan2h  33068  matunitlindflem1  33072  matunitlindflem2  33073  poimirlem32  33108  mblfinlem4  33116  mbfresfi  33123  mbfposadd  33124  itg2addnc  33131  ftc1anclem5  33156  ftc1anclem8  33159  dvasin  33163  heiborlem7  33283  igenidl  33529  atlatmstc  34121  dihglblem2N  36098  eldioph4b  36890  diophren  36892  rmxp1  37012  rmyp1  37013  rmxm1  37014  rmym1  37015  wepwso  37128  pfx2  40737  dig0  41718  onetansqsecsq  41821  cotsqcscsq  41822  dpfrac1  41832  dpfrac1OLD  41833
  Copyright terms: Public domain W3C validator