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  6694  00sr  6697  eqlei2  6909  divcanap3  7457  nn1suc  7714  nn0ge0  7983  elnn0z  8034  nn0n0n1ge2b  8096  nn0ind-raph  8131  elnn1uz2  8320  indstr2  8322  xrnemnf  8469  xrnepnf  8470  mnfltxr  8477  nn0pnfge0  8482  xrlttr  8486  xrltso  8487  xrlttri3  8488  nltpnft  8500  ngtmnft  8501  fztpval  8715  fseq1p1m1  8726  fzfig  8887  1exp  8938  0exp  8944  sqrt0rlem  9212  bj-om  9396  bj-nn0suc0  9410  bj-nn0suc  9424  bj-nn0sucALT  9438  bj-findis  9439
  Copyright terms: Public domain W3C validator