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  1271  barbara  2043  eqeq12i  2098  vtocl2  2668  spc2ev  2707  sbc2ie  2899  csbieb  2958  sseq12i  3041  uneq12i  3141  ineq12i  3188  nelpri  3455  ralpr  3480  rexpr  3481  preq12i  3507  dfop  3604  opeq12i  3610  breq12i  3829  mpteq2ia  3899  exmidundif  4009  opex  4030  opi2  4034  opth2  4041  opeqsn  4053  opeqpr  4054  uniop  4056  opelopaba  4067  braba  4068  opelopab  4072  brab  4073  opelopabaf  4074  unex  4240  snnex  4245  op1stb  4273  onun2i  4281  onsucssi  4296  ontr2exmid  4314  onsucsssucexmid  4316  onsucelsucexmid  4319  opthreg  4345  tfis  4371  finds  4388  finds2  4389  nnregexmid  4407  xpeq12i  4433  opelvv  4456  eqrelriiv  4500  eqrelrdv  4502  xpss  4514  xpex  4521  relop  4554  brco  4575  opelcnv  4586  brcnv  4587  asymref  4784  codir  4787  ssrnres  4839  dmprop  4871  dfco2  4896  cossxp  4919  cocnvss  4922  coex  4942  funsn  5027  fnsn  5033  feq23i  5121  resasplitss  5153  fabex  5162  fvex  5288  xpsn  5436  fmptap  5450  opabex  5482  acexmidlemv  5611  oveq12i  5625  oprabid  5638  oprabss  5691  caovcom  5759  opabex3  5850  iunex  5851  oprabex  5856  ofmres  5864  op1st  5874  op2nd  5875  fo1st  5885  fo2nd  5886  mpt2ex  5937  1stconst  5943  2ndconst  5944  algrflem  5951  dftpos4  5982  tpostpos  5983  tpossym  5995  frecex  6113  frecfnom  6120  sucinc  6160  fnoei  6167  oeiexg  6168  nnacli  6197  nnmcli  6198  elec  6283  ecovcom  6351  ecovass  6353  ecovdi  6355  fnmap  6364  mapval  6369  elmap  6386  elpm  6388  elpm2  6389  map0  6398  entri  6455  endisj  6492  xpcomco  6494  phplem2  6521  ssfiexmid  6544  domfiexmid  6546  unfiexmid  6580  unfiin  6588  inresflem  6696  djuin  6700  casefun  6720  caserel  6722  caseinj  6724  djufun  6728  djuinj  6730  fodjuomnilemdc  6743  dju1p1e2  6767  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  1lt2pi  6843  indpi  6845  1nq  6869  rec1nq  6898  1lt2nq  6909  ltaddnq  6910  halfnqq  6913  prarloclemarch2  6922  prarloclemlt  6996  prarloclemcalc  7005  genpelxp  7014  ltexprlempr  7111  recexprlempr  7135  cauappcvgprlemcl  7156  cauappcvgprlemladd  7161  caucvgprlemcl  7179  caucvgprprlemcl  7207  0r  7240  1sr  7241  m1r  7242  m1p1sr  7250  m1m1sr  7251  0lt1sr  7255  1ne0sr  7256  1idsr  7258  recexgt0sr  7263  prsradd  7275  caucvgsrlemoffres  7289  caucvgsr  7291  pitonnlem1p1  7327  pitonnlem2  7328  pitoregt0  7330  peano2nnnn  7334  axi2m1  7354  axprecex  7359  axcnre  7360  nnindnn  7372  nntopi  7373  0cn  7424  addcli  7436  mulcli  7437  mulcomi  7438  readdcli  7445  remulcli  7446  rexpssxrxp  7476  ltrelxr  7491  gtneii  7524  lttri3i  7526  letri3i  7527  ltnsymi  7528  lenlti  7529  ltlei  7530  mulgt0i  7538  mulgt0ii  7539  0lt1  7554  addcomi  7570  pncan3oi  7642  resubcli  7689  subcli  7702  pncan3i  7703  negsubi  7704  subnegi  7705  subeq0i  7706  neg11i  7707  negcon1i  7708  negcon2i  7709  mulneg1i  7826  mulneg2i  7827  mul2negi  7828  addgt0ii  7910  ltnegi  7912  lenegi  7913  ltnegcon2i  7914  lesub0i  7915  ltaddposi  7916  posdifi  7917  ltnegcon1i  7918  lenegcon1i  7919  subge0i  7920  1ap0  8008  ltapii  8051  recrecapi  8150  dividapi  8151  div0api  8152  rec11apii  8167  divdiv32api  8173  recgt0ii  8303  ltrecii  8314  ltdiv23ii  8323  nnssre  8361  nnind  8373  nnmulcli  8379  nnsubi  8396  0le2  8447  1lt3  8521  2lt4  8523  1lt4  8524  3lt5  8526  2lt5  8527  1lt5  8528  4lt6  8530  3lt6  8531  2lt6  8532  1lt6  8533  5lt7  8535  4lt7  8536  3lt7  8537  2lt7  8538  1lt7  8539  6lt8  8541  5lt8  8542  4lt8  8543  3lt8  8544  2lt8  8545  1lt8  8546  7lt9  8548  6lt9  8549  5lt9  8550  4lt9  8551  3lt9  8552  2lt9  8553  1lt9  8554  2muline0  8574  nn0addcli  8643  nn0mulcli  8644  nn0addge1i  8654  nn0addge2i  8655  dfz2  8752  halfnz  8775  9p1e10  8811  numnncl  8818  numltc  8834  le9lt10  8835  nummac  8853  8lt10  8940  7lt10  8941  6lt10  8942  5lt10  8943  4lt10  8944  3lt10  8945  2lt10  8946  1lt10  8947  eluzaddi  8977  eluzsubi  8978  eluz2nn  8989  uzuzle23  8991  eluzge3nn  8992  divfnzn  9038  elq  9039  qreccl  9059  xrltnr  9182  mnfltpnf  9187  xrex  9237  elicc2i  9289  ioomax  9298  iccmax  9299  ioopos  9300  elxrge0  9328  iccshftri  9344  iccshftli  9346  iccdili  9348  icccntri  9350  unitssre  9354  fz10  9392  fzpreddisj  9415  fldiv4p1lem1div2  9640  frecfzennn  9761  fnn0nninf  9771  fxnn0nninf  9772  0tonninf  9773  1tonninf  9774  m1expcl2  9876  m1expcl  9877  nn0expcli  9880  sqmuli  9936  cu2  9951  i3  9954  subsqi  9962  binom2subi  9966  bcpasc  10071  4bc2eq6  10079  hashinfom  10083  prhash2ex  10114  hashp1i  10115  rei  10229  imi  10230  readdi  10258  imaddi  10259  remuli  10260  immuli  10261  cjaddi  10262  cjmuli  10263  ipcni  10264  crrei  10266  crimi  10267  rexfiuz  10318  sqrt1  10375  sqrt4  10376  sqrt9  10377  abs1  10401  sqrtmulii  10463  abslti  10467  abslei  10468  abssubi  10479  absmuli  10480  sqabsaddi  10481  sqabssubi  10482  abstrii  10484  fimaxre2  10553  climz  10575  abscn2  10597  recn2  10599  imcn2  10600  climabs  10602  climre  10604  climim  10605  3dvdsdec  10747  3dvds2dec  10748  odd2np1lem  10754  n2dvds1  10794  z4even  10798  ndvdsi  10815  flodddiv4  10816  gcd0val  10834  6gcd4e2  10866  eucialg  10923  3lcm2e6woprm  10950  6lcm4e12  10951  3lcm2e6  11021  sqrt2irrlem  11022  phimullem  11083  xpnnen  11089  xpomen  11090  ex-fl  11098  ex-ceil  11099  ex-bc  11101  ex-dvds  11102  ex-gcd  11103  bj-unex  11255  bj-nn0suc0  11290  bj-nntrans  11291  bj-nnelirr  11293  pw1dom2  11334  nnsf  11340  peano3nninf  11342  nninfex  11346  exmidsbthrlem  11357
  Copyright terms: Public domain W3C validator