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

Theorem mpbiri 161
Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
Hypotheses
Ref Expression
mpbiri.min 𝜒
mpbiri.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpbiri (𝜑𝜓)

Proof of Theorem mpbiri
StepHypRef Expression
1 mpbiri.min . . 3 𝜒
21a1i 9 . 2 (𝜑𝜒)
3 mpbiri.maj . 2 (𝜑 → (𝜓𝜒))
42, 3mpbird 160 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  pm5.18im  1290  dedhb  2730  sbceqal  2838  ssdifeq0  3330  pwidg  3397  elpr2  3422  snidg  3425  exsnrex  3438  rabrsndc  3463  prid1g  3499  sssnr  3549  ssprr  3552  sstpr  3553  preqr1  3564  unimax  3639  intmin3  3667  syl6eqbr  3826  pwnss  3937  0inp0  3944  bnd2  3951  euabex  3986  copsexg  4006  euotd  4016  elopab  4020  epelg  4052  sucidg  4178  regexmidlem1  4283  sucprcreg  4298  onprc  4301  dtruex  4308  omelon2  4355  elvvuni  4429  eqrelriv  4458  relopabi  4488  opabid2  4492  ididg  4514  iss  4679  funopg  4959  fn0  5043  f00  5106  f1o00  5186  fo00  5187  brprcneu  5196  relelfvdm  5230  fsn  5360  eufnfv  5414  f1eqcocnv  5456  riotaprop  5516  acexmidlemb  5529  acexmidlemab  5531  acexmidlem2  5534  oprabid  5562  elrnmpt2  5639  ov6g  5663  eqop2  5829  1stconst  5867  2ndconst  5868  dftpos3  5905  dftpos4  5906  2pwuninelg  5926  ecopover  6232  en0  6303  en1  6307  fiprc  6320  nneneq  6348  findcard  6373  findcard2  6374  findcard2s  6375  1ne0sr  6879  00sr  6882  eqlei2  7141  divcanap3  7719  nn1suc  7979  nn0ge0  8234  elnn0z  8285  nn0n0n1ge2b  8348  nn0ind-raph  8384  elnn1uz2  8611  indstr2  8613  xrnemnf  8770  xrnepnf  8771  mnfltxr  8778  nn0pnfge0  8783  xrlttr  8787  xrltso  8788  xrlttri3  8789  nltpnft  8801  ngtmnft  8802  fztpval  9017  fseq1p1m1  9028  fzfig  9335  iser0f  9381  1exp  9414  0exp  9420  bcn1  9590  sqrt0rlem  9793  0dvds  10091  fz01or  10153  nn0o  10182  bj-om  10391  bj-nn0suc0  10405  bj-nn0suc  10419  bj-nn0sucALT  10433  bj-findis  10434
  Copyright terms: Public domain W3C validator