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

Theorem mpan2 409
Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
Hypotheses
Ref Expression
mpan2.1 𝜓
mpan2.2 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
mpan2 (𝜑𝜒)

Proof of Theorem mpan2
StepHypRef Expression
1 mpan2.1 . . 3 𝜓
21a1i 9 . 2 (𝜑𝜓)
3 mpan2.2 . 2 ((𝜑𝜓) → 𝜒)
42, 3mpdan 406 1 (𝜑𝜒)
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:  mpanr12  423  mp3an23  1233  equs4  1627  sb4bor  1730  eueq2dc  2734  sbcgf  2850  csbconstgf  2888  sbcnestg  2924  csbnestg  2925  csbnest1g  2926  ssindif0im  3306  mpteq1  3866  iinexgm  3933  mss  3987  eusv2nf  4213  eldifpw  4233  ordtriexmid  4272  onsucsssucexmid  4277  ordsucunielexmid  4281  nn0suc  4352  xpss1  4473  xpiindim  4498  reldm0  4578  elrnmpt1s  4609  resdm  4674  resid  4687  eliniseg  4720  trinxp  4743  inimasn  4766  ssrnres  4788  cnveq0  4802  coi2  4862  relrelss  4869  funcnvres  4997  funimaex  5009  fnresin1  5038  fnresin2  5039  fresin  5093  dffv3g  5199  ssimaex  5259  dmfco  5266  fvmpt  5274  fsn  5360  fsn2  5362  elabrex  5422  f1elima  5437  2ndconst  5868  tposfun  5903  tpostpos2  5908  tfrexlem  5976  tfri3  5981  rdgruledefgg  5990  rdgss  5998  frecsuclem3  6018  frecrdg  6020  oa0  6065  om0  6066  oei0  6067  oav2  6071  oa1suc  6075  nnmsucr  6095  nnm1  6125  nnm2  6126  ecelqsg  6187  ecidg  6198  xpiderm  6205  qsel  6211  xp1en  6325  xpcomco  6328  findcard2s  6375  findcard2d  6376  findcard2sd  6377  mulidpi  6444  nlt1pig  6467  indpi  6468  halfnqq  6536  archnqq  6543  prarloclemarch  6544  prarloclemarch2  6545  nnnq  6548  nq0a0  6583  addpinq1  6590  prarloclemlt  6619  prarloclemlo  6620  prarloclem3  6623  prarloclemcalc  6628  nqprm  6668  addnqpr1  6688  1idprl  6716  1idpru  6717  1idpr  6718  recexprlem1ssl  6759  recexprlem1ssu  6760  ltmprr  6768  0idsr  6880  1idsr  6881  00sr  6882  pn0sr  6884  negexsr  6885  recexgt0sr  6886  archsr  6894  prsrcl  6896  prsradd  6898  elrealeu  6934  pitonnlem1p1  6950  peano2nnnn  6957  ax1rid  6979  axcnre  6983  peano5nnnn  6994  peano2cn  7179  peano2re  7180  addid2  7183  subid  7263  subid1  7264  negid  7291  negeq0  7298  peano2cnm  7310  peano2rem  7311  mul01  7428  lt0neg1  7507  le0neg1  7509  recexre  7613  inelr  7619  rimul  7620  reapmul1  7630  apsqgt0  7636  mulge0  7654  negap0  7664  divvalap  7697  rerecclap  7751  div2negap  7756  divgt0i2i  7928  peano5nni  7963  nnge1  7983  times2  8082  addltmul  8188  nn0p1nn  8248  peano2nn0  8249  nn0lele2xi  8260  znnnlt1  8320  nn0lt10b  8349  prime  8366  msqznn  8367  zeo  8372  elnn1uz2  8611  qreccl  8644  qdivcl  8645  irrmul  8649  rphalfcl  8678  rpnegap  8683  ltpnf  8773  nltmnf  8780  pnfge  8781  xlt0neg1  8822  xle0neg1  8824  elioopnf  8907  elicopnf  8909  iccshftri  8934  iccshftli  8936  iccdili  8938  icccntri  8940  fzprval  9016  fzofzp1  9155  fzostep1  9165  flqge0nn0  9208  flqge1nn  9209  fldiv4p1lem1div2  9220  frecuzrdgsuc  9330  expivallem  9386  expival  9387  exp1  9391  qexpclz  9406  nn0sqcl  9412  expeq0  9416  expubnd  9442  sqval  9443  sqeq0  9448  resqcl  9452  zsqcl  9455  binom21  9494  bcnn  9589  bcn2  9596  bcn2p1  9602  bcnm1  9604  shftfibg  9613  shftfib  9616  reim0  9653  imval2  9686  cjap0  9699  cjne0  9700  rexuz3  9780  resqrexlemover  9800  abs00  9854  abssq  9871  nn0abscl  9875  nnabscl  9890  abs2dif  9896  climshft  10019  dvdsval2  10074  dvdsmul2  10093  dvdsmulcr  10100  dvdsabseq  10122  divconjdvds  10124  alzdvds  10129  fzo0dvdseq  10132  odd2np1lem  10146  mod2eq1n2dvds  10154  bj-inf2vnlem1  10425
  Copyright terms: Public domain W3C validator