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

Theorem mp2an 417
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 415 . 2 (𝜓𝜒)
51, 4ax-mp 7 1 𝜒
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  1269  barbara  2040  eqeq12i  2095  vtocl2  2655  spc2ev  2694  sbc2ie  2886  csbieb  2945  sseq12i  3026  uneq12i  3125  ineq12i  3172  nelpri  3430  ralpr  3455  rexpr  3456  preq12i  3482  dfop  3577  opeq12i  3583  breq12i  3802  mpteq2ia  3872  opex  3992  opi2  3996  opth2  4003  opeqsn  4015  opeqpr  4016  uniop  4018  opelopaba  4029  braba  4030  opelopab  4034  brab  4035  opelopabaf  4036  unex  4202  snnex  4207  op1stb  4235  onun2i  4243  onsucssi  4258  ontr2exmid  4276  onsucsssucexmid  4278  onsucelsucexmid  4281  opthreg  4307  tfis  4332  finds  4349  finds2  4350  nnregexmid  4368  xpeq12i  4393  opelvv  4416  eqrelriiv  4460  eqrelrdv  4462  xpss  4474  xpex  4481  relop  4514  brco  4534  opelcnv  4545  brcnv  4546  asymref  4740  codir  4743  ssrnres  4793  dmprop  4825  dfco2  4850  cossxp  4873  coex  4893  funsn  4978  fnsn  4984  feq23i  5072  resasplitss  5100  fabex  5109  fvex  5226  xpsn  5371  fmptap  5385  opabex  5417  acexmidlemv  5541  oveq12i  5555  oprabid  5568  oprabss  5621  caovcom  5689  opabex3  5780  iunex  5781  oprabex  5786  ofmres  5794  op1st  5804  op2nd  5805  fo1st  5815  fo2nd  5816  mpt2ex  5867  1stconst  5873  2ndconst  5874  algrflem  5881  dftpos4  5912  tpostpos  5913  tpossym  5925  frecex  6043  frecfnom  6050  sucinc  6089  fnoei  6096  oeiexg  6097  nnacli  6126  nnmcli  6127  elec  6211  ecovcom  6279  ecovass  6281  ecovdi  6283  entri  6333  endisj  6368  xpcomco  6370  phplem2  6388  ssfiexmid  6411  domfiexmid  6413  unfiexmid  6438  unfiin  6444  1lt2pi  6592  indpi  6594  1nq  6618  rec1nq  6647  1lt2nq  6658  ltaddnq  6659  halfnqq  6662  prarloclemarch2  6671  prarloclemlt  6745  prarloclemcalc  6754  genpelxp  6763  ltexprlempr  6860  recexprlempr  6884  cauappcvgprlemcl  6905  cauappcvgprlemladd  6910  caucvgprlemcl  6928  caucvgprprlemcl  6956  0r  6989  1sr  6990  m1r  6991  m1p1sr  6999  m1m1sr  7000  0lt1sr  7004  1ne0sr  7005  1idsr  7007  recexgt0sr  7012  prsradd  7024  caucvgsrlemoffres  7038  caucvgsr  7040  pitonnlem1p1  7076  pitonnlem2  7077  pitoregt0  7079  peano2nnnn  7083  axi2m1  7103  axprecex  7108  axcnre  7109  nnindnn  7121  nntopi  7122  0cn  7173  addcli  7185  mulcli  7186  mulcomi  7187  readdcli  7194  remulcli  7195  rexpssxrxp  7225  ltrelxr  7240  gtneii  7273  lttri3i  7275  letri3i  7276  ltnsymi  7277  lenlti  7278  ltlei  7279  mulgt0i  7287  mulgt0ii  7288  0lt1  7303  addcomi  7319  pncan3oi  7391  resubcli  7438  subcli  7451  pncan3i  7452  negsubi  7453  subnegi  7454  subeq0i  7455  neg11i  7456  negcon1i  7457  negcon2i  7458  mulneg1i  7575  mulneg2i  7576  mul2negi  7577  addgt0ii  7659  ltnegi  7661  lenegi  7662  ltnegcon2i  7663  lesub0i  7664  ltaddposi  7665  posdifi  7666  ltnegcon1i  7667  lenegcon1i  7668  subge0i  7669  1ap0  7757  ltapii  7800  recrecapi  7899  dividapi  7900  div0api  7901  rec11apii  7916  divdiv32api  7922  recgt0ii  8052  ltrecii  8063  ltdiv23ii  8072  nnssre  8110  nnind  8122  nnmulcli  8128  nnsubi  8145  0le2  8196  1lt3  8270  2lt4  8272  1lt4  8273  3lt5  8275  2lt5  8276  1lt5  8277  4lt6  8279  3lt6  8280  2lt6  8281  1lt6  8282  5lt7  8284  4lt7  8285  3lt7  8286  2lt7  8287  1lt7  8288  6lt8  8290  5lt8  8291  4lt8  8292  3lt8  8293  2lt8  8294  1lt8  8295  7lt9  8297  6lt9  8298  5lt9  8299  4lt9  8300  3lt9  8301  2lt9  8302  1lt9  8303  2muline0  8323  nn0addcli  8392  nn0mulcli  8393  nn0addge1i  8403  nn0addge2i  8404  dfz2  8501  halfnz  8524  9p1e10  8560  numnncl  8567  numltc  8583  le9lt10  8584  nummac  8602  8lt10  8689  7lt10  8690  6lt10  8691  5lt10  8692  4lt10  8693  3lt10  8694  2lt10  8695  1lt10  8696  eluzaddi  8726  eluzsubi  8727  eluz2nn  8738  uzuzle23  8740  eluzge3nn  8741  divfnzn  8787  elq  8788  qreccl  8808  xrltnr  8931  mnfltpnf  8936  xrex  8986  elicc2i  9038  ioomax  9047  iccmax  9048  ioopos  9049  elxrge0  9077  iccshftri  9093  iccshftli  9095  iccdili  9097  icccntri  9099  unitssre  9103  fz10  9141  fzpreddisj  9164  fldiv4p1lem1div2  9387  frecfzennn  9508  m1expcl2  9595  m1expcl  9596  nn0expcli  9599  sqmuli  9655  cu2  9670  i3  9673  subsqi  9681  binom2subi  9685  bcpasc  9790  4bc2eq6  9798  sizeinf  9802  prsize2ex  9833  sizep1i  9834  rei  9924  imi  9925  readdi  9953  imaddi  9954  remuli  9955  immuli  9956  cjaddi  9957  cjmuli  9958  ipcni  9959  crrei  9961  crimi  9962  rexfiuz  10013  sqrt1  10070  sqrt4  10071  sqrt9  10072  abs1  10096  sqrtmulii  10158  abslti  10162  abslei  10163  abssubi  10174  absmuli  10175  sqabsaddi  10176  sqabssubi  10177  abstrii  10179  fimaxre2  10247  climz  10269  abscn2  10291  recn2  10293  imcn2  10294  climabs  10296  climre  10298  climim  10299  3dvdsdec  10409  3dvds2dec  10410  odd2np1lem  10416  n2dvds1  10456  z4even  10460  ndvdsi  10477  flodddiv4  10478  gcd0val  10496  6gcd4e2  10528  eucialg  10585  3lcm2e6woprm  10612  6lcm4e12  10613  3lcm2e6  10683  sqrt2irrlem  10684  xpnnen  10705  xpomen  10706  ex-fl  10714  ex-ceil  10715  ex-bc  10717  ex-dvds  10718  ex-gcd  10719  bj-unex  10868  bj-nn0suc0  10903  bj-nntrans  10904  bj-nnelirr  10906
  Copyright terms: Public domain W3C validator