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

Theorem mp3an3 1567
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 1143 . 2 ((𝜑𝜓) → (𝜒𝜃))
41, 3mpi 20 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  mp3an13  1569  mp3an23  1570  mp3anl3  1574  opelxp  5359  ov  7020  ovmpt2a  7031  ovmpt2  7036  oaword1  7879  oneo  7908  oeoalem  7923  oeoelem  7925  nnaword1  7956  nnneo  7978  erov  8090  enrefg  8234  f1imaen  8264  mapxpen  8375  acnlem  9164  cdacomen  9298  infmap  9693  canthnumlem  9765  tskin  9876  tsksn  9877  tsk0  9880  gruxp  9924  gruina  9935  genpprecl  10118  addsrpr  10191  mulsrpr  10192  supsrlem  10227  mulid1  10333  00id  10506  mul02lem1  10507  ltneg  10823  leneg  10826  suble0  10837  div1  11011  nnaddcl  11339  nnmulcl  11340  nnmulclOLD  11341  nnge1  11344  nnsub  11357  2halves  11547  halfaddsub  11552  addltmul  11555  zleltp1  11714  nnaddm1cl  11720  zextlt  11737  eluzp1p1  11950  uzaddcl  11982  znq  12031  xrre  12238  xrre2  12239  fzshftral  12671  fraclt1  12847  expadd  13145  expmul  13148  expubnd  13164  sqmul  13169  bernneq  13233  faclbnd2  13318  faclbnd6  13326  hashgadd  13404  hashun2  13410  hashssdif  13437  hashfun  13461  ccatlcan  13716  ccatrcan  13717  shftval3  14059  sqrlem1  14226  caubnd2  14340  bpoly2  15028  bpoly3  15029  fsumcube  15031  efexp  15071  efival  15122  cos01gt0  15161  odd2np1  15305  halfleoddlt  15326  omoe  15328  opeo  15329  divalglem5  15360  gcdmultiple  15508  sqgcd  15517  nn0seqcvgd  15522  phiprmpw  15718  eulerthlem2  15724  odzcllem  15734  pythagtriplem15  15771  pythagtriplem17  15773  pcelnn  15811  4sqlem3  15891  xpscfn  16444  fullfunc  16790  fthfunc  16791  prfcl  17068  curf1cl  17093  curfcl  17097  hofcl  17124  odinv  18199  lsmelvalix  18277  dprdval  18624  lsp0  19236  lss0v  19243  coe1scl  19885  zndvds0  20126  frlmlbs  20367  lindfres  20393  lmisfree  20412  ntrin  21100  lpsscls  21180  restperf  21223  txuni2  21603  txopn  21640  elqtop2  21739  xkocnv  21852  ptcmp  22096  xblpnfps  22434  xblpnf  22435  bl2in  22439  unirnblps  22458  unirnbl  22459  blpnfctr  22475  dscopn  22612  bcthlem4  23358  minveclem2  23432  minveclem4  23438  icombl  23568  i1fadd  23699  i1fmul  23700  dvn1  23926  dvexp3  23978  plyconst  24199  plyid  24202  sincosq1eq  24502  sinord  24518  cxpp1  24663  cxpsqrtlem  24685  cxpsqrt  24686  angneg  24770  dcubic  24810  issqf  25099  ppiub  25166  bposlem1  25246  bposlem2  25247  bposlem9  25254  axlowdimlem6  26064  axlowdimlem14  26072  axcontlem2  26082  structgrssvtxlemOLD  26152  pthdlem2  26915  0ewlk  27310  ipasslem1  28037  ipasslem2  28038  ipasslem11  28046  minvecolem2  28082  minvecolem3  28083  minvecolem4  28087  shsva  28530  h1datomi  28791  lnfnmuli  29254  leopsq  29339  nmopleid  29349  opsqrlem6  29355  pjnmopi  29358  hstle  29440  csmdsymi  29544  atcvatlem  29595  dpfrac1  29948  elsx  30605  dya2iocnrect  30691  cvmliftphtlem  31644  wlimeq12  32107  frecseq123  32120  nosupno  32192  nosupfv  32195  scutval  32254  scutun12  32260  fvray  32591  fvline  32594  tailfb  32715  uncov  33722  tan2h  33733  matunitlindflem1  33737  matunitlindflem2  33738  poimirlem32  33773  mblfinlem4  33781  mbfresfi  33787  mbfposadd  33788  itg2addnc  33795  ftc1anclem5  33820  ftc1anclem8  33823  dvasin  33827  heiborlem7  33946  igenidl  34192  el3v3  34330  atlatmstc  35118  dihglblem2N  37093  eldioph4b  37895  diophren  37897  rmxp1  38016  rmyp1  38017  rmxm1  38018  rmym1  38019  wepwso  38132  pfx2  42005  dig0  42986  onetansqsecsq  43091  cotsqcscsq  43092
  Copyright terms: Public domain W3C validator