ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpan Unicode 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  |-  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 413 1  |-  ( ps 
->  ch )
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  1260  mp3an12  1263  mp3an13  1264  ax9o  1633  sbnfc2  2986  ssdifss  3128  undifss  3359  uneqdifeqim  3364  elssuni  3676  csbexa  3960  difexg  3972  rabexg  3974  abssexg  4008  snexg  4010  copsexg  4062  sotritric  4142  sotritrieq  4143  trsuc  4240  oneli  4246  unexb  4258  opeluu  4263  rabxfr  4283  reuhyp  4285  ordunisuc2r  4321  reg3exmid  4385  brrelexi  4468  brrelex12i  4469  brrelex1i  4470  brrelex2i  4471  xpss2  4537  opabid2  4555  eliunxp  4563  releldmi  4662  relelrni  4663  dmexg  4685  rnexg  4686  elres  4735  resexg  4739  relbrcnvg  4798  brcodir  4806  sotri  4814  sotri2  4816  sotri3  4817  dfrel2  4868  coi1  4933  fco  5161  fssres  5171  fabexg  5182  fvopab3g  5361  mpteqb  5377  ffvelrni  5417  fsn2  5455  dfmptg  5460  fvpr1  5483  fvconst2  5495  mptexg  5504  oprabid  5663  ovprc  5666  caovcl  5781  caovass  5787  caovdi  5806  elmpt2cl  5824  ofexg  5842  resfunexgALT  5863  fo1stresm  5914  fo2ndresm  5915  1stexg  5920  2ndexg  5921  elopabi  5947  mpt2exxg  5959  mpt2xopn0yelv  5986  rntpos  6004  smores  6039  tfr0dm  6069  tfrlemibxssdm  6074  tfrexlem  6081  tfr1onlembxssdm  6090  tfrcllembxssdm  6103  rdgruledefgg  6122  rdgruledefg  6123  rdgivallem  6128  rdgexg  6136  frec0g  6144  ordgt0ge1  6181  omfnex  6192  oeiv  6199  nna0r  6221  nnm0r  6222  nnsucsssuc  6235  nn2m  6265  nnaordex  6266  nnawordex  6267  ecdmn0m  6314  ecelqsi  6326  ecidg  6336  ectocl  6339  encv  6443  f1oen  6456  ssdomg  6475  map1  6509  fiprc  6512  xpdom1  6531  fict  6564  isinfinf  6593  ac6sfi  6594  xpfi  6619  en1eqsn  6636  fidcenumlemr  6643  eqinfti  6694  djueq2  6713  djulclr  6720  djurclr  6721  djulcl  6722  djurcl  6723  djuf1olem  6724  djulclb  6726  djuun  6739  eldju1st  6741  1stinl  6744  2ndinl  6745  1stinr  6746  2ndinr  6747  isomnimap  6772  0nnq  6902  mulidnq  6927  archnqq  6955  prarloclemarch2  6957  nqnq0pi  6976  nq0m0r  6994  nq02m  7003  prarloclemlt  7031  prarloclemn  7037  prarloclem5  7038  addnqprllem  7065  addnqprulem  7066  appdivnq  7101  1idprl  7128  1idpru  7129  addextpr  7159  cauappcvgprlemdisj  7189  cauappcvgprlemloc  7190  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  caucvgprlemnbj  7205  caucvgprlemloc  7213  caucvgprprlemnbj  7231  caucvgprprlemloc  7241  caucvgprprlemaddq  7246  0nsr  7274  ltsosr  7289  recexgt0sr  7298  prsrpos  7309  caucvgsr  7326  mulresr  7354  axcnre  7395  axpre-ltwlin  7397  mulid2  7465  0re  7467  axmulgt0  7537  ltnsym2  7554  eqlei  7557  ltnei  7567  muladd11  7594  cnegex  7639  0cnALT  7651  negcl  7661  negneg  7711  mul02  7844  mulm1  7857  lt0neg2  7926  le0neg2  7928  recexre  8031  recexgt0  8033  mulge0  8072  gt0ap0i  8079  recextlem1  8094  recexap  8096  recclapzi  8178  recap0apzi  8179  recidapzi  8180  divassapzi  8203  divmulapzi  8204  divdirapzi  8205  rerecclapzi  8217  ltp1  8277  recgt0i  8339  ltmul1i  8353  ltdiv1i  8354  ltmuldivi  8355  ltmul2i  8356  lemul1i  8357  lemul2i  8358  nngt1ne1  8428  nnrecre  8430  nn0ge0  8668  nn0addcl  8678  nn0mulcl  8679  zgt0ge1  8778  dfuzi  8826  eluzel2  8993  eluz2b1  9057  uz2m1nn  9061  nn01to3  9071  zq  9080  nnrecq  9099  rpge0  9115  rpreccl  9129  mnflt  9222  pnfnlt  9226  mnfle  9231  xrlelttr  9240  xrltletr  9241  xrletr  9242  xlt0neg2  9270  xle0neg2  9272  elioomnf  9355  ige3m2fz  9432  fzshftral  9489  ige2m1fz1  9490  1fv  9515  4fvwrd4  9516  rebtwn2zlemstep  9629  qbtwnxr  9634  btwnzge0  9672  zmodid2  9724  q2txmodxeq0  9756  frec2uzrand  9777  frecuzrdgtcl  9784  frecfzennn  9798  nn0ennn  9805  0exp  9955  sqgt0api  10005  subsq2  10027  bernneq  10039  faclbnd  10114  faclbnd2  10115  faclbnd3  10116  hashinfuni  10150  hashxp  10199  2shfti  10230  reim  10251  imcl  10253  crim  10257  caucvgre  10379  rennim  10400  resqrexlemdecn  10410  qabsor  10473  absimle  10482  sqrtthi  10517  sqrtcli  10518  sqrtgt0i  10519  sqrtmsqi  10520  sqrtsqi  10521  sqsqrti  10522  sqrtge0i  10523  absidi  10524  absnidi  10525  serclim0  10657  iserclim0  10658  fsum2d  10792  fsumcnv  10794  fsumconst  10811  modfsummodlem1  10813  fsumabs  10822  binom11  10842  0dvds  10898  odd2np1lem  10954  odd2np1  10955  even2n  10956  mod2eq0even  10960  2teven  10969  opoe  10977  omoe  10978  opeo  10979  omeo  10980  m1exp1  10983  gcd0id  11052  gcdid0  11053  1gcd  11065  lcmdvds  11143  isprm2lem  11180  isprm3  11182  prmgt1  11195  coprm  11205  isevengcd2  11219  isoddgcd1  11220  sqpweven  11235  2sqpwodd  11236  unennn  11292  djucllem  11346  bdrabexg  11443  bdunexb  11457  peano5set  11481  speano5  11485  bj-omtrans  11497  nninfsellemeq  11552
  Copyright terms: Public domain W3C validator