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

Theorem mpan 420
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 418 1 (𝜓𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  mp2an  422  mpanl12  432  mp3an1  1302  mp3an12  1305  mp3an13  1306  ax9o  1676  sbnfc2  3060  ssdifss  3206  undifss  3443  uneqdifeqim  3448  elssuni  3764  csbexa  4057  difexg  4069  rabexg  4071  abssexg  4106  snexg  4108  copsexg  4166  sotritric  4246  sotritrieq  4247  trsuc  4344  oneli  4350  unexb  4363  opeluu  4371  rabxfr  4391  reuhyp  4393  ordunisuc2r  4430  reg3exmid  4494  brrelex12i  4581  brrelex1i  4582  brrelex2i  4583  xpss2  4650  opabid2  4670  eliunxp  4678  releldmi  4778  relelrni  4779  dmexg  4803  rnexg  4804  elres  4855  resexg  4859  relbrcnvg  4918  brcodir  4926  sotri  4934  sotri2  4936  sotri3  4937  dfrel2  4989  coi1  5054  fco  5288  fssres  5298  fabexg  5310  fvopab3g  5494  mptrcl  5503  mpteqb  5511  elfvmptrab1  5515  ffvelrni  5554  fsn2  5594  dfmptg  5599  fvpr1  5624  fvconst2  5636  mptexg  5645  oprabid  5803  ovprc  5806  caovcl  5925  caovass  5931  caovdi  5950  elmpocl  5968  ofexg  5986  resfunexgALT  6008  fo1stresm  6059  fo2ndresm  6060  1stexg  6065  2ndexg  6066  elopabi  6093  mpoexxg  6108  mpoxopn0yelv  6136  rntpos  6154  smores  6189  tfr0dm  6219  tfrlemibxssdm  6224  tfrexlem  6231  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  rdgruledefgg  6272  rdgruledefg  6273  rdgivallem  6278  rdgexg  6286  frec0g  6294  ordgt0ge1  6332  omfnex  6345  oeiv  6352  nna0r  6374  nnm0r  6375  nnsucsssuc  6388  nn2m  6422  nnaordex  6423  nnawordex  6424  ecdmn0m  6471  ecelqsi  6483  ecidg  6493  ectocl  6496  encv  6640  f1oen  6653  ssdomg  6672  map1  6706  fiprc  6709  xpdom1  6729  fict  6762  isinfinf  6791  ac6sfi  6792  xpfi  6818  en1eqsn  6836  fidcenumlemr  6843  fiss  6865  eqinfti  6907  djueq2  6926  djulclr  6934  djurclr  6935  djulcl  6936  djurcl  6937  djuf1olem  6938  djulclb  6940  inl11  6950  eldju1st  6956  1stinl  6959  2ndinl  6960  1stinr  6961  2ndinr  6962  ctssdccl  6996  isomnimap  7009  ismkvmap  7028  iswomnimap  7038  djucomen  7077  0nnq  7184  mulidnq  7209  archnqq  7237  prarloclemarch2  7239  nqnq0pi  7258  nq0m0r  7276  nq02m  7285  prarloclemlt  7313  prarloclemn  7319  prarloclem5  7320  addnqprllem  7347  addnqprulem  7348  appdivnq  7383  1idprl  7410  1idpru  7411  addextpr  7441  cauappcvgprlemdisj  7471  cauappcvgprlemloc  7472  cauappcvgprlemladdru  7476  cauappcvgprlemladdrl  7477  caucvgprlemnbj  7487  caucvgprlemloc  7495  caucvgprprlemnbj  7513  caucvgprprlemloc  7523  caucvgprprlemaddq  7528  suplocexprlemmu  7538  suplocexprlemru  7539  suplocexprlemloc  7541  suplocexprlemlub  7544  0nsr  7569  ltsosr  7584  recexgt0sr  7593  prsrpos  7605  caucvgsr  7622  mappsrprg  7624  suplocsrlem  7628  mulresr  7658  axcnre  7701  axpre-ltwlin  7703  mulid2  7776  0re  7778  axmulgt0  7848  ltnsym2  7866  eqlei  7869  ltnei  7879  muladd11  7907  cnegex  7952  0cnALT  7964  negcl  7974  negneg  8024  mul02  8161  mulm1  8174  lt0neg2  8243  le0neg2  8245  recexre  8352  recexgt0  8354  mulge0  8393  gt0ap0i  8401  recextlem1  8424  recexap  8426  recclapzi  8509  recap0apzi  8510  recidapzi  8511  divassapzi  8534  divmulapzi  8535  divdirapzi  8536  rerecclapzi  8548  ltp1  8614  recgt0i  8676  ltmul1i  8690  ltdiv1i  8691  ltmuldivi  8692  ltmul2i  8693  lemul1i  8694  lemul2i  8695  sup3exmid  8727  nngt1ne1  8767  nnrecre  8769  nn0ge0  9014  nn0addcl  9024  nn0mulcl  9025  zgt0ge1  9124  dfuzi  9173  eluzel2  9343  eluz2b1  9407  uz2m1nn  9411  nn01to3  9421  zq  9430  nnrecq  9449  rpge0  9466  rpreccl  9480  mnflt  9581  pnfnlt  9585  mnfle  9590  xrlelttr  9601  xrltletr  9602  xrletr  9603  xgepnf  9611  xlt0neg2  9634  xle0neg2  9636  xaddpnf2  9642  xaddmnf2  9644  xaddid2  9658  elioomnf  9763  ige3m2fz  9841  fzshftral  9900  ige2m1fz1  9901  1fv  9928  4fvwrd4  9929  rebtwn2zlemstep  10042  qbtwnxr  10047  btwnzge0  10085  zmodid2  10137  q2txmodxeq0  10169  frec2uzrand  10190  frecuzrdgtcl  10197  frecfzennn  10211  nn0ennn  10218  uzennn  10221  0exp  10340  sqgt0api  10390  subsq2  10412  bernneq  10424  faclbnd  10499  faclbnd2  10500  faclbnd3  10501  hashinfuni  10535  hashxp  10584  2shfti  10615  reim  10636  imcl  10638  crim  10642  caucvgre  10765  rennim  10786  resqrexlemdecn  10796  qabsor  10859  absimle  10868  sqrtthi  10903  sqrtcli  10904  sqrtgt0i  10905  sqrtmsqi  10906  sqrtsqi  10907  sqsqrti  10908  sqrtge0i  10909  absidi  10910  absnidi  10911  xrmaxiflemlub  11029  serclim0  11086  fsum2d  11216  fsumcnv  11218  fsumconst  11235  modfsummodlem1  11237  fsumabs  11246  binom11  11267  prodf1  11323  prodfclim1  11325  efzval  11401  eftlub  11408  efsep  11409  ef4p  11412  efgt1  11415  reef11  11417  sinf  11422  cosf  11423  efi4p  11435  sinneg  11444  cosneg  11445  efival  11450  efmival  11451  cos01gt0  11480  sin02gt0  11481  absefib  11488  efieq1re  11489  demoivre  11490  demoivreALT  11491  eirraplem  11494  0dvds  11524  odd2np1lem  11580  odd2np1  11581  even2n  11582  mod2eq0even  11586  2teven  11595  opoe  11603  omoe  11604  opeo  11605  omeo  11606  m1exp1  11609  gcd0id  11678  gcdid0  11679  1gcd  11691  lcmdvds  11771  isprm2lem  11808  isprm3  11810  prmgt1  11823  coprm  11833  isevengcd2  11847  isoddgcd1  11848  sqpweven  11864  2sqpwodd  11865  unennn  11921  ctinfomlemom  11951  qnnen  11955  strslfv  12017  strle1g  12063  1strbas  12072  istopon  12194  tgval  12232  eltg4i  12238  eltg3  12240  tg1  12242  tg2  12243  topnex  12269  cldrcl  12285  restsn  12363  lmrcl  12374  metflem  12532  xmetf  12533  ismet2  12537  xmeteq0  12542  xmettri2  12544  xmetpsmet  12552  xmetres2  12562  blfvalps  12568  blex  12570  blvalps  12571  blval  12572  blfps  12592  blf  12593  mopnval  12625  cnbl0  12717  cnblcld  12718  blssioo  12728  resubmet  12731  cncfmet  12762  cnplimcim  12819  cnlimcim  12823  cnlimc  12824  dvfgg  12840  dvfpm  12841  dvfcnpm  12842  dvcj  12856  reeff1olem  12875  ef2kpi  12909  sinperlem  12911  sin2kpi  12914  cos2kpi  12915  sinhalfpip  12923  sinhalfpim  12924  coshalfpip  12925  coshalfpim  12926  sincosq1sgn  12929  sinq12gt0  12933  sinkpi  12950  reeflog  12964  relogef  12965  loggt0b  12989  djucllem  13066  bdrabexg  13163  bdunexb  13177  peano5set  13197  speano5  13201  bj-omtrans  13213  pwf1oexmid  13253  nninfsellemeq  13271
  Copyright terms: Public domain W3C validator