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

Theorem mp2an 417
Description: An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
Hypotheses
Ref Expression
mp2an.1  |-  ph
mp2an.2  |-  ps
mp2an.3  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mp2an  |-  ch

Proof of Theorem mp2an
StepHypRef Expression
1 mp2an.2 . 2  |-  ps
2 mp2an.1 . . 3  |-  ph
3 mp2an.3 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
42, 3mpan 415 . 2  |-  ( ps 
->  ch )
51, 4ax-mp 7 1  |-  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:  mp4an  418  jaoi  669  mp3an  1271  barbara  2043  eqeq12i  2098  vtocl2  2668  spc2ev  2707  sbc2ie  2899  csbieb  2958  sseq12i  3041  uneq12i  3141  ineq12i  3188  nelpri  3455  ralpr  3482  rexpr  3483  preq12i  3509  dfop  3606  opeq12i  3612  breq12i  3831  mpteq2ia  3901  exmidundif  4011  opex  4032  opi2  4036  opth2  4043  opeqsn  4055  opeqpr  4056  uniop  4058  opelopaba  4069  braba  4070  opelopab  4074  brab  4075  opelopabaf  4076  unex  4242  snnex  4247  op1stb  4275  onun2i  4283  onsucssi  4298  ontr2exmid  4316  onsucsssucexmid  4318  onsucelsucexmid  4321  opthreg  4347  tfis  4373  finds  4390  finds2  4391  nnregexmid  4409  xpeq12i  4435  opelvv  4458  eqrelriiv  4502  eqrelrdv  4504  xpss  4516  xpex  4523  relop  4556  brco  4577  opelcnv  4588  brcnv  4589  asymref  4786  codir  4789  ssrnres  4841  dmprop  4873  dfco2  4898  cossxp  4921  cocnvss  4924  coex  4944  funsn  5029  fnsn  5035  feq23i  5123  resasplitss  5155  fabex  5164  fvex  5290  xpsn  5438  fmptap  5452  opabex  5484  acexmidlemv  5613  oveq12i  5627  oprabid  5640  oprabss  5693  caovcom  5761  opabex3  5852  iunex  5853  oprabex  5858  ofmres  5866  op1st  5876  op2nd  5877  fo1st  5887  fo2nd  5888  mpt2ex  5939  1stconst  5945  2ndconst  5946  algrflem  5953  dftpos4  5984  tpostpos  5985  tpossym  5997  frecex  6115  frecfnom  6122  sucinc  6162  fnoei  6169  oeiexg  6170  nnacli  6199  nnmcli  6200  elec  6285  ecovcom  6353  ecovass  6355  ecovdi  6357  fnmap  6366  mapval  6371  elmap  6388  elpm  6390  elpm2  6391  map0  6400  entri  6457  endisj  6494  xpcomco  6496  phplem2  6523  ssfiexmid  6546  domfiexmid  6548  unfiexmid  6582  unfiin  6590  inresflem  6699  djuin  6703  casefun  6723  caserel  6725  caseinj  6727  djufun  6731  djuinj  6733  fodjuomnilemdc  6746  dju1p1e2  6770  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  1lt2pi  6846  indpi  6848  1nq  6872  rec1nq  6901  1lt2nq  6912  ltaddnq  6913  halfnqq  6916  prarloclemarch2  6925  prarloclemlt  6999  prarloclemcalc  7008  genpelxp  7017  ltexprlempr  7114  recexprlempr  7138  cauappcvgprlemcl  7159  cauappcvgprlemladd  7164  caucvgprlemcl  7182  caucvgprprlemcl  7210  0r  7243  1sr  7244  m1r  7245  m1p1sr  7253  m1m1sr  7254  0lt1sr  7258  1ne0sr  7259  1idsr  7261  recexgt0sr  7266  prsradd  7278  caucvgsrlemoffres  7292  caucvgsr  7294  pitonnlem1p1  7330  pitonnlem2  7331  pitoregt0  7333  peano2nnnn  7337  axi2m1  7357  axprecex  7362  axcnre  7363  nnindnn  7375  nntopi  7376  0cn  7427  addcli  7439  mulcli  7440  mulcomi  7441  readdcli  7448  remulcli  7449  rexpssxrxp  7479  ltrelxr  7494  gtneii  7527  lttri3i  7529  letri3i  7530  ltnsymi  7531  lenlti  7532  ltlei  7533  mulgt0i  7541  mulgt0ii  7542  0lt1  7557  addcomi  7573  pncan3oi  7645  resubcli  7692  subcli  7705  pncan3i  7706  negsubi  7707  subnegi  7708  subeq0i  7709  neg11i  7710  negcon1i  7711  negcon2i  7712  mulneg1i  7829  mulneg2i  7830  mul2negi  7831  addgt0ii  7913  ltnegi  7915  lenegi  7916  ltnegcon2i  7917  lesub0i  7918  ltaddposi  7919  posdifi  7920  ltnegcon1i  7921  lenegcon1i  7922  subge0i  7923  1ap0  8011  ltapii  8054  recrecapi  8153  dividapi  8154  div0api  8155  rec11apii  8170  divdiv32api  8176  recgt0ii  8306  ltrecii  8317  ltdiv23ii  8326  nnssre  8364  nnind  8376  nnmulcli  8382  nnsubi  8399  0le2  8450  1lt3  8524  2lt4  8526  1lt4  8527  3lt5  8529  2lt5  8530  1lt5  8531  4lt6  8533  3lt6  8534  2lt6  8535  1lt6  8536  5lt7  8538  4lt7  8539  3lt7  8540  2lt7  8541  1lt7  8542  6lt8  8544  5lt8  8545  4lt8  8546  3lt8  8547  2lt8  8548  1lt8  8549  7lt9  8551  6lt9  8552  5lt9  8553  4lt9  8554  3lt9  8555  2lt9  8556  1lt9  8557  2muline0  8577  nn0addcli  8646  nn0mulcli  8647  nn0addge1i  8657  nn0addge2i  8658  dfz2  8755  halfnz  8778  9p1e10  8814  numnncl  8821  numltc  8837  le9lt10  8838  nummac  8856  8lt10  8943  7lt10  8944  6lt10  8945  5lt10  8946  4lt10  8947  3lt10  8948  2lt10  8949  1lt10  8950  eluzaddi  8980  eluzsubi  8981  eluz2nn  8992  uzuzle23  8994  eluzge3nn  8995  divfnzn  9041  elq  9042  qreccl  9062  xrltnr  9185  mnfltpnf  9190  xrex  9240  elicc2i  9292  ioomax  9301  iccmax  9302  ioopos  9303  elxrge0  9331  iccshftri  9347  iccshftli  9349  iccdili  9351  icccntri  9353  unitssre  9357  fz10  9395  fzpreddisj  9418  fldiv4p1lem1div2  9643  frecfzennn  9764  fnn0nninf  9774  fxnn0nninf  9775  0tonninf  9776  1tonninf  9777  m1expcl2  9879  m1expcl  9880  nn0expcli  9883  sqmuli  9939  cu2  9954  i3  9957  subsqi  9965  binom2subi  9969  bcpasc  10074  4bc2eq6  10082  hashinfom  10086  prhash2ex  10117  hashp1i  10118  rei  10232  imi  10233  readdi  10261  imaddi  10262  remuli  10263  immuli  10264  cjaddi  10265  cjmuli  10266  ipcni  10267  crrei  10269  crimi  10270  rexfiuz  10321  sqrt1  10378  sqrt4  10379  sqrt9  10380  abs1  10404  sqrtmulii  10466  abslti  10470  abslei  10471  abssubi  10482  absmuli  10483  sqabsaddi  10484  sqabssubi  10485  abstrii  10487  fimaxre2  10556  climz  10578  abscn2  10600  recn2  10602  imcn2  10603  climabs  10605  climre  10607  climim  10608  3dvdsdec  10771  3dvds2dec  10772  odd2np1lem  10778  n2dvds1  10818  z4even  10822  ndvdsi  10839  flodddiv4  10840  gcd0val  10858  6gcd4e2  10890  eucialg  10947  3lcm2e6woprm  10974  6lcm4e12  10975  3lcm2e6  11045  sqrt2irrlem  11046  phimullem  11107  xpnnen  11113  xpomen  11114  ex-fl  11122  ex-ceil  11123  ex-bc  11125  ex-dvds  11126  ex-gcd  11127  bj-unex  11279  bj-nn0suc0  11314  bj-nntrans  11315  bj-nnelirr  11317  pw1dom2  11358  nnsf  11364  peano3nninf  11366  nninfex  11370  exmidsbthrlem  11381
  Copyright terms: Public domain W3C validator