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

Theorem mpan2 421
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 417 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  mpanr12  435  mp3an23  1292  equs4  1688  sb4bor  1791  elvd  2665  eueq2dc  2830  sbcgf  2948  csbconstgf  2986  sbcnestg  3023  csbnestg  3024  csbnest1g  3025  ssindif0im  3392  mpteq1  3982  iinexgm  4049  mss  4118  eusv2nf  4347  eldifpw  4368  ordtriexmid  4407  onsucsssucexmid  4412  ordsucunielexmid  4416  nn0suc  4488  xpss1  4619  xpiindim  4646  reldm0  4727  elrnmpt1s  4759  resdm  4828  resid  4845  eliniseg  4879  trinxp  4902  inimasn  4926  ssrnres  4951  cnveq0  4965  coi2  5025  relrelss  5035  funcnvres  5166  funimaex  5178  fnresin1  5207  fnresin2  5208  fresin  5271  dffv3g  5385  ssimaex  5450  dmfco  5457  fvmpt  5466  fsn  5560  fsn2  5562  elabrex  5627  f1elima  5642  2ndconst  6087  tposfun  6125  tpostpos2  6130  tfrexlem  6199  tfri3  6232  rdgruledefgg  6240  rdgss  6248  frecsuclem  6271  frecrdg  6273  oa0  6321  om0  6322  oei0  6323  oav2  6327  oa1suc  6331  nnmsucr  6352  nnm1  6388  nnm2  6389  ecelqsg  6450  ecidg  6461  xpider  6468  qsel  6474  mapdm0  6525  map0e  6548  mapsnconst  6556  ixpsnf1o  6598  map1  6674  xp1en  6685  xpcomco  6688  xpmapenlem  6711  findcard2s  6752  findcard2d  6753  findcard2sd  6754  exmidpw  6770  fidcenumlemr  6811  sbthlem7  6819  eqinfti  6875  djueq1  6893  omp1eomlem  6947  endjusym  6949  eninl  6950  eninr  6951  difinfsn  6953  finomni  6980  pm54.43  7014  exmidonfinlem  7017  mulidpi  7094  nlt1pig  7117  indpi  7118  halfnqq  7186  archnqq  7193  prarloclemarch  7194  prarloclemarch2  7195  nnnq  7198  nq0a0  7233  addpinq1  7240  prarloclemlt  7269  prarloclemlo  7270  prarloclem3  7273  prarloclemcalc  7278  nqprm  7318  addnqpr1  7338  1idprl  7366  1idpru  7367  1idpr  7368  recexprlem1ssl  7409  recexprlem1ssu  7410  ltmprr  7418  0idsr  7543  1idsr  7544  00sr  7545  pn0sr  7547  negexsr  7548  recexgt0sr  7549  ltm1sr  7553  archsr  7558  prsrcl  7560  prsradd  7562  mappsrprg  7580  map2psrprg  7581  elrealeu  7605  pitonnlem1p1  7622  peano2nnnn  7629  ax1rid  7653  axcnre  7657  peano5nnnn  7668  peano2cn  7865  peano2re  7866  addid2  7869  subid  7949  subid1  7950  negid  7977  negeq0  7984  peano2cnm  7996  peano2rem  7997  mul01  8119  lt0neg1  8198  le0neg1  8200  recexre  8307  inelr  8313  rimul  8314  reapmul1  8324  apsqgt0  8330  mulge0  8348  negap0  8359  divvalap  8401  rerecclap  8457  div2negap  8462  divgt0i2i  8639  peano5nni  8687  nnge1  8707  times2  8807  addltmul  8914  nn0p1nn  8974  peano2nn0  8975  nn0lele2xi  8986  znnnlt1  9060  nn0lt10b  9089  prime  9108  msqznn  9109  zeo  9114  elnn1uz2  9357  qreccl  9390  qdivcl  9391  irrmul  9395  rphalfcl  9424  rpnegap  9429  ltpnf  9522  nltmnf  9529  pnfge  9530  xlt0neg1  9576  xle0neg1  9578  xaddpnf1  9584  xaddmnf1  9586  xaddid1  9600  xsubge0  9619  xleaddadd  9625  elioopnf  9705  elicopnf  9707  iccshftri  9733  iccshftli  9735  iccdili  9737  icccntri  9739  fzprval  9817  fzofzp1  9959  fzostep1  9969  flqge0nn0  10021  flqge1nn  10022  fldiv4p1lem1div2  10033  exp1  10254  qexpclz  10269  nn0sqcl  10275  expeq0  10279  expubnd  10305  sqval  10306  sqeq0  10311  resqcl  10315  zsqcl  10318  iexpcyc  10352  binom21  10359  bcnn  10458  bcn2  10465  bcn2p1  10471  bcnm1  10473  fihasheq0  10495  hashsng  10499  fihashen1  10500  fimaxq  10528  shftfibg  10547  shftfib  10550  reim0  10588  imval2  10621  cjap0  10634  cjne0  10635  rexuz3  10717  resqrexlemover  10737  abssq  10808  nn0abscl  10812  nnabscl  10827  abs2dif  10833  max0addsup  10946  climshft  11028  bcxmas  11213  efgt1p2  11315  efgt1p  11316  efi4p  11338  resin4p  11339  recos4p  11340  sinbnd  11373  cosbnd  11374  dvdsval2  11408  zdvdsdc  11426  dvdsmul2  11428  dvdsmulcr  11435  dvdsabseq  11457  divconjdvds  11459  alzdvds  11464  fzo0dvdseq  11467  odd2np1lem  11481  mod2eq1n2dvds  11488  flodddiv4  11543  flodddiv4t2lthalf  11546  gcdmndc  11549  gcd0id  11579  gcd1  11587  dfgcd2  11614  gcdmultiple  11620  gcdmultiplez  11621  dvdssq  11631  lcmmndc  11655  lcm0val  11658  dvdslcm  11662  lcmeq0  11664  lcmgcd  11671  lcmdvds  11672  lcmid  11673  lcm1  11674  cncongr2  11697  isprm3  11711  prm2orodd  11719  sqrt2irrap  11769  phiprm  11810  unennn  11821  ennnfonelemim  11848  ctinfom  11852  ctinf  11854  enctlem  11856  ressid  11931  elrestr  12039  0opn  12084  topopn  12086  tgval  12129  tgvalex  12130  0cld  12192  ntropn  12197  ntrtop  12208  ntr0  12214  neipsm  12234  rest0  12259  xmetres  12462  metres  12463  mopnex  12585  tgioo  12626  cnlimcim  12720  cnlimc  12721  dvfre  12754  dveflem  12766  dvef  12767  efcn  12768  sin2pim  12805  cos2pim  12806  sinmpi  12807  cosmpi  12808  sinppi  12809  cosppi  12810  efimpi  12811  sincosq1lem  12817  sincosq2sgn  12819  sincosq3sgn  12820  sincosq4sgn  12821  sinq12gt0  12822  sinq34lt0t  12823  bj-inf2vnlem1  13064  pwle2  13089  pwf1oexmid  13090  exmid1stab  13091  nninfsellemeqinf  13108  sbthom  13117
  Copyright terms: Public domain W3C validator