ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpan GIF version

Theorem mpan 415
Description: An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpan.1 𝜑
mpan.2 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
mpan (𝜓𝜒)

Proof of Theorem mpan
StepHypRef Expression
1 mpan.1 . . 3 𝜑
21a1i 9 . 2 (𝜓𝜑)
3 mpan.2 . 2 ((𝜑𝜓) → 𝜒)
42, 3mpancom 413 1 (𝜓𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  mp2an  417  mpanl12  427  mp3an1  1256  mp3an12  1259  mp3an13  1260  ax9o  1629  sbnfc2  2963  ssdifss  3103  undifss  3330  uneqdifeqim  3335  elssuni  3637  csbexa  3915  difexg  3927  rabexg  3929  abssexg  3963  snexg  3964  copsexg  4007  sotritric  4087  sotritrieq  4088  trsuc  4185  oneli  4191  unexb  4203  opeluu  4208  rabxfr  4228  reuhyp  4230  ordunisuc2r  4266  reg3exmid  4330  brrelexi  4410  brrelex2i  4411  xpss2  4477  opabid2  4495  eliunxp  4503  releldmi  4601  relelrni  4602  dmexg  4624  rnexg  4625  elres  4674  resexg  4678  relbrcnvg  4734  brcodir  4742  sotri  4750  sotri2  4752  sotri3  4753  dfrel2  4801  coi1  4866  fco  5087  fssres  5097  fabexg  5108  fvopab3g  5277  mpteqb  5293  ffvelrni  5333  fsn2  5369  dfmptg  5374  fvpr1  5397  fvconst2  5409  mptexg  5418  oprabid  5568  ovprc  5571  caovcl  5686  caovass  5692  caovdi  5711  elmpt2cl  5729  ofexg  5747  resfunexgALT  5768  fo1stresm  5819  fo2ndresm  5820  1stexg  5825  2ndexg  5826  elopabi  5852  mpt2exxg  5864  mpt2xopn0yelv  5888  rntpos  5906  smores  5941  tfr0dm  5971  tfrlemibxssdm  5976  tfrexlem  5983  tfr1onlembxssdm  5992  tfrcllembxssdm  6005  rdgruledefgg  6024  rdgruledefg  6025  rdgivallem  6030  rdgexg  6038  frec0g  6046  ordgt0ge1  6082  omfnex  6093  oeiv  6100  nna0r  6122  nnm0r  6123  nnsucsssuc  6136  nn2m  6165  nnaordex  6166  nnawordex  6167  ecdmn0m  6214  ecelqsi  6226  ecidg  6236  ectocl  6239  encv  6293  f1oen  6306  ssdomg  6325  fiprc  6360  xpdom1  6379  fict  6403  ac6sfi  6431  eqinfti  6492  0nnq  6616  mulidnq  6641  archnqq  6669  prarloclemarch2  6671  nqnq0pi  6690  nq0m0r  6708  nq02m  6717  prarloclemlt  6745  prarloclemn  6751  prarloclem5  6752  addnqprllem  6779  addnqprulem  6780  appdivnq  6815  1idprl  6842  1idpru  6843  addextpr  6873  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  caucvgprlemnbj  6919  caucvgprlemloc  6927  caucvgprprlemnbj  6945  caucvgprprlemloc  6955  caucvgprprlemaddq  6960  0nsr  6988  ltsosr  7003  recexgt0sr  7012  prsrpos  7023  caucvgsr  7040  mulresr  7068  axcnre  7109  axpre-ltwlin  7111  mulid2  7179  0re  7181  axmulgt0  7251  ltnsym2  7268  eqlei  7271  ltnei  7281  muladd11  7308  cnegex  7353  0cnALT  7365  negcl  7375  negneg  7425  mul02  7558  mulm1  7571  lt0neg2  7640  le0neg2  7642  recexre  7745  recexgt0  7747  mulge0  7786  gt0ap0i  7793  recextlem1  7808  recexap  7810  recclapzi  7892  recap0apzi  7893  recidapzi  7894  divassapzi  7917  divmulapzi  7918  divdirapzi  7919  rerecclapzi  7931  ltp1  7989  recgt0i  8051  ltmul1i  8065  ltdiv1i  8066  ltmuldivi  8067  ltmul2i  8068  lemul1i  8069  lemul2i  8070  nngt1ne1  8140  nnrecre  8142  nn0ge0  8380  nn0addcl  8390  nn0mulcl  8391  zgt0ge1  8490  dfuzi  8538  eluzel2  8705  eluz2b1  8769  uz2m1nn  8773  nn01to3  8783  zq  8792  nnrecq  8811  rpge0  8827  rpreccl  8841  mnflt  8934  pnfnlt  8938  mnfle  8943  xrlelttr  8952  xrltletr  8953  xrletr  8954  xlt0neg2  8982  xle0neg2  8984  elioomnf  9067  ige3m2fz  9144  fzshftral  9201  ige2m1fz1  9202  1fv  9226  4fvwrd4  9227  rebtwn2zlemstep  9339  qbtwnxr  9344  btwnzge0  9382  zmodid2  9434  q2txmodxeq0  9466  frec2uzrand  9487  frecuzrdgtcl  9494  frecfzennn  9508  nn0ennn  9515  iseqeq4  9527  expival  9575  0exp  9608  sqgt0api  9658  subsq2  9679  bernneq  9690  faclbnd  9765  faclbnd2  9766  faclbnd3  9767  sizeinfuni  9801  2shfti  9857  reim  9877  imcl  9879  crim  9883  caucvgre  10005  rennim  10026  resqrexlemdecn  10036  qabsor  10099  absimle  10108  sqrtthi  10143  sqrtcli  10144  sqrtgt0i  10145  sqrtmsqi  10146  sqrtsqi  10147  sqsqrti  10148  sqrtge0i  10149  absidi  10150  absnidi  10151  iserclim0  10282  0dvds  10360  odd2np1lem  10416  odd2np1  10417  even2n  10418  mod2eq0even  10422  2teven  10431  opoe  10439  omoe  10440  opeo  10441  omeo  10442  m1exp1  10445  gcd0id  10514  gcdid0  10515  1gcd  10527  lcmdvds  10605  isprm2lem  10642  isprm3  10644  prmgt1  10657  coprm  10667  isevengcd2  10681  isoddgcd1  10682  sqpweven  10697  2sqpwodd  10698  unennn  10708  bdrabexg  10855  bdunexb  10869  peano5set  10893  speano5  10897  bj-omtrans  10909
  Copyright terms: Public domain W3C validator