ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbiri Structured version   GIF 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  6674  00sr  6677  eqlei2  6889  divcanap3  7437  nn1suc  7694  nn0ge0  7963  elnn0z  8014  nn0n0n1ge2b  8076  nn0ind-raph  8111  elnn1uz2  8300  indstr2  8302  xrnemnf  8449  xrnepnf  8450  mnfltxr  8457  nn0pnfge0  8462  xrlttr  8466  xrltso  8467  xrlttri3  8468  nltpnft  8480  ngtmnft  8481  fztpval  8695  fseq1p1m1  8706  fzfig  8867  1exp  8918  0exp  8924  sqrt0rlem  9192  bj-om  9371  bj-nn0suc0  9384  bj-nn0suc  9394  bj-nn0sucALT  9408  bj-findis  9409
  Copyright terms: Public domain W3C validator