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

Theorem mpan 408
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 407 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  mp2an  410  mpanl12  420  mp3an1  1230  mp3an12  1233  mp3an13  1234  ax9o  1604  sbnfc2  2934  ssdifss  3102  undifss  3331  uneqdifeqim  3336  elssuni  3636  csbexa  3914  difexg  3926  rabexg  3928  abssexg  3962  snexgOLD  3963  snexg  3964  copsexg  4009  sotritric  4089  sotritrieq  4090  trsuc  4187  oneli  4193  unexb  4205  opeluu  4210  rabxfr  4230  reuhyp  4232  ordunisuc2r  4268  reg3exmid  4332  brrelexi  4412  brrelex2i  4413  xpss2  4477  opabid2  4495  eliunxp  4503  releldmi  4601  relelrni  4602  dmexg  4624  rnexg  4625  elres  4674  resexg  4678  relbrcnvg  4732  brcodir  4740  sotri  4748  sotri2  4750  sotri3  4751  dfrel2  4799  coi1  4864  fco  5084  fssres  5094  fabexg  5105  fvopab3g  5273  mpteqb  5289  ffvelrni  5329  fsn2  5365  dfmptg  5370  fvpr1  5393  fvconst2  5405  mptexg  5414  oprabid  5565  ovprc  5568  caovcl  5683  caovass  5689  caovdi  5708  elmpt2cl  5726  ofexg  5744  resfunexgALT  5765  fo1stresm  5816  fo2ndresm  5817  1stexg  5822  2ndexg  5823  elopabi  5849  mpt2exxg  5861  mpt2xopn0yelv  5885  rntpos  5903  smores  5938  tfr0  5968  tfrlemibxssdm  5972  tfrexlem  5979  rdgruledefgg  5993  rdgruledefg  5994  rdgivallem  5999  rdgon  6004  rdgexg  6007  frec0g  6014  ordgt0ge1  6049  omfnex  6060  oeiv  6067  oeicl  6073  nna0r  6088  nnm0r  6089  nnsucsssuc  6102  nn2m  6130  nnaordex  6131  nnawordex  6132  ecdmn0m  6179  ecelqsi  6191  ecidg  6201  ectocl  6204  encv  6258  f1oen  6270  ssdomg  6289  fiprc  6323  xpdom1  6340  ac6sfi  6383  0nnq  6520  mulidnq  6545  archnqq  6573  prarloclemarch2  6575  nqnq0pi  6594  nq0m0r  6612  nq02m  6621  prarloclemlt  6649  prarloclemn  6655  prarloclem5  6656  addnqprllem  6683  addnqprulem  6684  appdivnq  6719  1idprl  6746  1idpru  6747  addextpr  6777  cauappcvgprlemdisj  6807  cauappcvgprlemloc  6808  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgprlemnbj  6823  caucvgprlemloc  6831  caucvgprprlemnbj  6849  caucvgprprlemloc  6859  caucvgprprlemaddq  6864  0nsr  6892  ltsosr  6907  recexgt0sr  6916  prsrpos  6927  caucvgsr  6944  mulresr  6972  axcnre  7013  axpre-ltwlin  7015  mulid2  7083  0re  7085  axmulgt0  7150  ltnsym2  7167  eqlei  7170  ltnei  7180  muladd11  7207  cnegex  7252  0cnALT  7264  negcl  7274  negneg  7324  mul02  7456  mulm1  7469  lt0neg2  7538  le0neg2  7540  recexre  7643  recexgt0  7645  mulge0  7684  gt0ap0i  7691  recextlem1  7706  recexap  7708  recclapzi  7788  recap0apzi  7789  recidapzi  7790  divassapzi  7813  divmulapzi  7814  divdirapzi  7815  rerecclapzi  7827  ltp1  7885  recgt0i  7947  ltmul1i  7961  ltdiv1i  7962  ltmuldivi  7963  ltmul2i  7964  lemul1i  7965  lemul2i  7966  nngt1ne1  8024  nnrecre  8026  nn0ge0  8264  nn0addcl  8274  nn0mulcl  8275  zgt0ge1  8360  dfuzi  8407  eluzel2  8574  eluz2b1  8635  uz2m1nn  8639  nn01to3  8649  zq  8658  nnrecq  8677  rpge0  8693  rpreccl  8707  mnflt  8805  pnfnlt  8809  mnfle  8814  xrlelttr  8823  xrltletr  8824  xrletr  8825  xlt0neg2  8853  xle0neg2  8855  elioomnf  8938  ige3m2fz  9015  fzshftral  9072  ige2m1fz1  9073  1fv  9098  4fvwrd4  9099  rebtwn2zlemstep  9209  qbtwnxr  9214  btwnzge0  9250  zmodid2  9302  q2txmodxeq0  9334  frec2uzrand  9355  frecuzrdgfn  9362  frecuzrdgsuc  9365  frecfzennn  9367  nn0ennn  9373  iseqeq4  9381  expival  9422  0exp  9455  sqgt0api  9505  subsq2  9526  bernneq  9537  faclbnd  9609  faclbnd2  9610  faclbnd3  9611  2shfti  9660  reim  9680  imcl  9682  crim  9686  caucvgre  9808  rennim  9829  resqrexlemdecn  9839  qabsor  9902  absimle  9911  sqrtthi  9946  sqrtcli  9947  sqrtgt0i  9948  sqrtmsqi  9949  sqrtsqi  9950  sqsqrti  9951  sqrtge0i  9952  absidi  9953  absnidi  9954  iserclim0  10057  0dvds  10128  odd2np1lem  10183  odd2np1  10184  even2n  10185  mod2eq0even  10189  2teven  10199  opoe  10207  omoe  10208  opeo  10209  omeo  10210  m1exp1  10213  bdrabexg  10413  bdunexb  10427  peano5set  10451  speano5  10456  bj-omtrans  10468
  Copyright terms: Public domain W3C validator