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

Theorem mpbiri 157
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 156 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm5.18im  1273  dedhb  2704  sbceqal  2808  ssdifeq0  3299  pwidg  3364  elpr2  3386  snidg  3392  exsnrex  3404  rabrsndc  3429  prid1g  3465  sssnr  3515  ssprr  3518  sstpr  3519  preqr1  3530  unimax  3605  intmin3  3633  syl6eqbr  3792  pwnss  3903  0inp0  3910  bnd2  3917  euabex  3952  copsexg  3972  euotd  3982  elopab  3986  epelg  4018  sucidg  4119  regexmidlem1  4218  sucprcreg  4227  onprc  4230  dtruex  4237  omelon2  4273  elvvuni  4347  eqrelriv  4376  relopabi  4406  opabid2  4410  ididg  4432  iss  4597  funopg  4877  fn0  4961  f00  5024  f1o00  5104  fo00  5105  brprcneu  5114  relelfvdm  5148  fsn  5278  eufnfv  5332  f1eqcocnv  5374  riotaprop  5434  acexmidlemb  5447  acexmidlemab  5449  acexmidlem2  5452  oprabid  5480  elrnmpt2  5556  ov6g  5580  eqop2  5746  1stconst  5784  2ndconst  5785  dftpos3  5818  dftpos4  5819  2pwuninelg  5839  ecopover  6140  en0  6211  en1  6215  fiprc  6228  1ne0sr  6654  00sr  6657  eqlei2  6869  divcanap3  7417  nn1suc  7674  nn0ge0  7943  elnn0z  7994  nn0n0n1ge2b  8056  nn0ind-raph  8091  elnn1uz2  8280  indstr2  8282  xrnemnf  8429  xrnepnf  8430  mnfltxr  8437  nn0pnfge0  8442  xrlttr  8446  xrltso  8447  xrlttri3  8448  nltpnft  8460  ngtmnft  8461  fztpval  8675  fseq1p1m1  8686  fzfig  8847  1exp  8898  0exp  8904  bj-om  9325  bj-nn0suc0  9338  bj-nn0suc  9348  bj-nn0sucALT  9362  bj-findis  9363
  Copyright terms: Public domain W3C validator