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

Theorem mp2an 402
Description: An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
Hypotheses
Ref Expression
mp2an.1 𝜑
mp2an.2 𝜓
mp2an.3 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
mp2an 𝜒

Proof of Theorem mp2an
StepHypRef Expression
1 mp2an.2 . 2 𝜓
2 mp2an.1 . . 3 𝜑
3 mp2an.3 . . 3 ((𝜑𝜓) → 𝜒)
42, 3mpan 400 . 2 (𝜓𝜒)
51, 4ax-mp 7 1 𝜒
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  mp4an  403  jaoi  636  mp3an  1232  barbara  1998  eqeq12i  2053  vtocl2  2609  spc2ev  2648  sbc2ie  2829  csbieb  2888  sseq12i  2971  uneq12i  3095  ineq12i  3136  nelpri  3399  ralpr  3425  rexpr  3426  preq12i  3452  dfop  3548  opeq12i  3554  breq12i  3773  mpteq2ia  3843  opex  3966  opi2  3970  opth2  3977  otth2  3978  opeqsn  3989  opeqpr  3990  uniop  3992  opelopaba  4003  braba  4004  opelopab  4008  brab  4009  opelopabaf  4010  unex  4176  snnex  4181  op1stb  4209  onun2i  4217  onsucssi  4232  ontr2exmid  4250  onsucsssucexmid  4252  onsucelsucexmid  4255  opthreg  4280  tfis  4306  finds  4323  finds2  4324  nnregexmid  4342  xpeq12i  4367  opelvv  4390  eqrelriiv  4434  eqrelrdv  4436  relsnop  4444  xpss  4446  xpex  4453  relop  4486  brco  4506  opelcnv  4517  brcnv  4518  asymref  4710  codir  4713  ssrnres  4763  dmprop  4795  op2ndb  4804  dfco2  4820  cossxp  4843  coex  4863  funsn  4948  fnsn  4953  feq23i  5041  resasplitss  5069  fabex  5078  fvex  5195  xpsn  5339  fmptap  5353  fvsn  5358  opabex  5385  acexmidlemv  5510  oveq12i  5524  oprabid  5537  oprabss  5590  caovcom  5658  opabex3  5749  iunex  5750  oprabex  5755  ofmres  5763  op1st  5773  op2nd  5774  fo1st  5784  fo2nd  5785  mpt2ex  5836  1stconst  5842  2ndconst  5843  algrflem  5850  dftpos4  5878  tpostpos  5879  tpossym  5891  frecex  5981  frecfnom  5986  sucinc  6025  fnoei  6032  oeiexg  6033  nnacli  6061  nnmcli  6062  elec  6145  ecovcom  6213  ecovass  6215  ecovdi  6217  entri  6266  endisj  6298  xpcomco  6300  phplem2  6316  ssfiexmid  6336  1lt2pi  6438  indpi  6440  1nq  6464  rec1nq  6493  1lt2nq  6504  ltaddnq  6505  halfnqq  6508  prarloclemarch2  6517  prarloclemlt  6591  prarloclemcalc  6600  genpelxp  6609  ltexprlempr  6706  recexprlempr  6730  cauappcvgprlemcl  6751  cauappcvgprlemladd  6756  caucvgprlemcl  6774  caucvgprprlemcl  6802  0r  6835  1sr  6836  m1r  6837  m1p1sr  6845  m1m1sr  6846  0lt1sr  6850  1ne0sr  6851  1idsr  6853  recexgt0sr  6858  prsradd  6870  caucvgsrlemoffres  6884  caucvgsr  6886  pitonnlem1p1  6922  pitonnlem2  6923  pitoregt0  6925  peano2nnnn  6929  axi2m1  6949  axprecex  6954  axcnre  6955  nnindnn  6967  nntopi  6968  0cn  7019  addcli  7031  mulcli  7032  mulcomi  7033  readdcli  7040  remulcli  7041  rexpssxrxp  7070  ltrelxr  7080  gtneii  7113  lttri3i  7115  letri3i  7116  ltnsymi  7117  lenlti  7118  ltlei  7119  mulgt0i  7127  mulgt0ii  7128  0lt1  7141  addcomi  7157  pncan3oi  7227  resubcli  7274  subcli  7287  pncan3i  7288  negsubi  7289  subnegi  7290  subeq0i  7291  neg11i  7292  negcon1i  7293  negcon2i  7294  mulneg1i  7401  mulneg2i  7402  mul2negi  7403  addgt0ii  7483  ltnegi  7485  lenegi  7486  ltnegcon2i  7487  lesub0i  7488  ltaddposi  7489  posdifi  7490  ltnegcon1i  7491  lenegcon1i  7492  subge0i  7493  1ap0  7581  ltapii  7624  recrecapi  7720  dividapi  7721  div0api  7722  rec11apii  7737  divdiv32api  7743  recgt0ii  7873  ltrecii  7884  ltdiv23ii  7893  nnssre  7918  nnind  7930  nnmulcli  7936  nnsubi  7953  0le2  8006  1lt3  8088  2lt4  8090  1lt4  8091  3lt5  8093  2lt5  8094  1lt5  8095  4lt6  8097  3lt6  8098  2lt6  8099  1lt6  8100  5lt7  8102  4lt7  8103  3lt7  8104  2lt7  8105  1lt7  8106  6lt8  8108  5lt8  8109  4lt8  8110  3lt8  8111  2lt8  8112  1lt8  8113  7lt9  8115  6lt9  8116  5lt9  8117  4lt9  8118  3lt9  8119  2lt9  8120  1lt9  8121  8lt10  8123  7lt10  8124  6lt10  8125  5lt10  8126  4lt10  8127  3lt10  8128  2lt10  8129  1lt10  8130  2muline0  8150  nn0addcli  8219  nn0mulcli  8220  nn0addge1i  8230  nn0addge2i  8231  dfz2  8313  halfnz  8336  numnncl  8375  numltc  8387  nummac  8399  eluzaddi  8499  eluzsubi  8500  eluz2nn  8511  uzuzle23  8513  eluzge3nn  8514  divfnzn  8556  elq  8557  qreccl  8576  xrltnr  8701  mnfltpnf  8706  xrex  8756  elicc2i  8808  ioomax  8817  iccmax  8818  ioopos  8819  elxrge0  8847  iccshftri  8863  iccshftli  8865  iccdili  8867  icccntri  8869  unitssre  8873  fz10  8910  fzpreddisj  8933  fldiv4p1lem1div2  9147  frecfzennn  9203  m1expcl2  9277  m1expcl  9278  nn0expcli  9281  sqmuli  9336  cu2  9351  i3  9354  subsqi  9361  binom2subi  9365  rei  9499  imi  9500  readdi  9528  imaddi  9529  remuli  9530  immuli  9531  cjaddi  9532  cjmuli  9533  ipcni  9534  crrei  9536  crimi  9537  sqrt1  9644  sqrt4  9645  sqrt9  9646  abs1  9670  sqrtmulii  9730  abslti  9734  abslei  9735  abssubi  9746  absmuli  9747  sqabsaddi  9748  sqabssubi  9749  abstrii  9751  climz  9813  abscn2  9835  recn2  9837  imcn2  9838  climabs  9840  climre  9842  climim  9843  sqr2irrlem  9877  ex-fl  9895  ex-ceil  9896  bj-unex  10039  bj-nn0suc0  10075  bj-nntrans  10076  bj-nnelirr  10078
  Copyright terms: Public domain W3C validator