ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpan Unicode 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  |-  ph
mpan.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mpan  |-  ( ps 
->  ch )

Proof of Theorem mpan
StepHypRef Expression
1 mpan.1 . . 3  |-  ph
21a1i 9 . 2  |-  ( ps 
->  ph )
3 mpan.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
42, 3mpancom 418 1  |-  ( ps 
->  ch )
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  djucomen  7072  0nnq  7179  mulidnq  7204  archnqq  7232  prarloclemarch2  7234  nqnq0pi  7253  nq0m0r  7271  nq02m  7280  prarloclemlt  7308  prarloclemn  7314  prarloclem5  7315  addnqprllem  7342  addnqprulem  7343  appdivnq  7378  1idprl  7405  1idpru  7406  addextpr  7436  cauappcvgprlemdisj  7466  cauappcvgprlemloc  7467  cauappcvgprlemladdru  7471  cauappcvgprlemladdrl  7472  caucvgprlemnbj  7482  caucvgprlemloc  7490  caucvgprprlemnbj  7508  caucvgprprlemloc  7518  caucvgprprlemaddq  7523  suplocexprlemmu  7533  suplocexprlemru  7534  suplocexprlemloc  7536  suplocexprlemlub  7539  0nsr  7564  ltsosr  7579  recexgt0sr  7588  prsrpos  7600  caucvgsr  7617  mappsrprg  7619  suplocsrlem  7623  mulresr  7653  axcnre  7696  axpre-ltwlin  7698  mulid2  7771  0re  7773  axmulgt0  7843  ltnsym2  7861  eqlei  7864  ltnei  7874  muladd11  7902  cnegex  7947  0cnALT  7959  negcl  7969  negneg  8019  mul02  8156  mulm1  8169  lt0neg2  8238  le0neg2  8240  recexre  8347  recexgt0  8349  mulge0  8388  gt0ap0i  8396  recextlem1  8419  recexap  8421  recclapzi  8504  recap0apzi  8505  recidapzi  8506  divassapzi  8529  divmulapzi  8530  divdirapzi  8531  rerecclapzi  8543  ltp1  8609  recgt0i  8671  ltmul1i  8685  ltdiv1i  8686  ltmuldivi  8687  ltmul2i  8688  lemul1i  8689  lemul2i  8690  sup3exmid  8722  nngt1ne1  8762  nnrecre  8764  nn0ge0  9009  nn0addcl  9019  nn0mulcl  9020  zgt0ge1  9119  dfuzi  9168  eluzel2  9338  eluz2b1  9402  uz2m1nn  9406  nn01to3  9416  zq  9425  nnrecq  9444  rpge0  9461  rpreccl  9475  mnflt  9576  pnfnlt  9580  mnfle  9585  xrlelttr  9596  xrltletr  9597  xrletr  9598  xgepnf  9606  xlt0neg2  9629  xle0neg2  9631  xaddpnf2  9637  xaddmnf2  9639  xaddid2  9653  elioomnf  9758  ige3m2fz  9836  fzshftral  9895  ige2m1fz1  9896  1fv  9923  4fvwrd4  9924  rebtwn2zlemstep  10037  qbtwnxr  10042  btwnzge0  10080  zmodid2  10132  q2txmodxeq0  10164  frec2uzrand  10185  frecuzrdgtcl  10192  frecfzennn  10206  nn0ennn  10213  uzennn  10216  0exp  10335  sqgt0api  10385  subsq2  10407  bernneq  10419  faclbnd  10494  faclbnd2  10495  faclbnd3  10496  hashinfuni  10530  hashxp  10579  2shfti  10610  reim  10631  imcl  10633  crim  10637  caucvgre  10760  rennim  10781  resqrexlemdecn  10791  qabsor  10854  absimle  10863  sqrtthi  10898  sqrtcli  10899  sqrtgt0i  10900  sqrtmsqi  10901  sqrtsqi  10902  sqsqrti  10903  sqrtge0i  10904  absidi  10905  absnidi  10906  xrmaxiflemlub  11024  serclim0  11081  fsum2d  11211  fsumcnv  11213  fsumconst  11230  modfsummodlem1  11232  fsumabs  11241  binom11  11262  prodf1  11318  prodfclim1  11320  efzval  11396  eftlub  11403  efsep  11404  ef4p  11407  efgt1  11410  reef11  11413  sinf  11418  cosf  11419  efi4p  11431  sinneg  11440  cosneg  11441  efival  11446  efmival  11447  cos01gt0  11476  sin02gt0  11477  absefib  11484  efieq1re  11485  demoivre  11486  demoivreALT  11487  eirraplem  11490  0dvds  11520  odd2np1lem  11576  odd2np1  11577  even2n  11578  mod2eq0even  11582  2teven  11591  opoe  11599  omoe  11600  opeo  11601  omeo  11602  m1exp1  11605  gcd0id  11674  gcdid0  11675  1gcd  11687  lcmdvds  11767  isprm2lem  11804  isprm3  11806  prmgt1  11819  coprm  11829  isevengcd2  11843  isoddgcd1  11844  sqpweven  11860  2sqpwodd  11861  unennn  11917  ctinfomlemom  11947  qnnen  11951  strslfv  12013  strle1g  12059  1strbas  12068  istopon  12190  tgval  12228  eltg4i  12234  eltg3  12236  tg1  12238  tg2  12239  topnex  12265  cldrcl  12281  restsn  12359  lmrcl  12370  metflem  12528  xmetf  12529  ismet2  12533  xmeteq0  12538  xmettri2  12540  xmetpsmet  12548  xmetres2  12558  blfvalps  12564  blex  12566  blvalps  12567  blval  12568  blfps  12588  blf  12589  mopnval  12621  cnbl0  12713  cnblcld  12714  blssioo  12724  resubmet  12727  cncfmet  12758  cnplimcim  12815  cnlimcim  12819  cnlimc  12820  dvfgg  12836  dvfpm  12837  dvfcnpm  12838  dvcj  12852  reeff1olem  12870  ef2kpi  12900  sinperlem  12902  sin2kpi  12905  cos2kpi  12906  sinhalfpip  12914  sinhalfpim  12915  coshalfpip  12916  coshalfpim  12917  sincosq1sgn  12920  sinq12gt0  12924  sinkpi  12941  reeflog  12955  relogef  12956  djucllem  13037  bdrabexg  13134  bdunexb  13148  peano5set  13168  speano5  13172  bj-omtrans  13184  pwf1oexmid  13224  nninfsellemeq  13240
  Copyright terms: Public domain W3C validator