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  1259  dedhb  2687  sbceqal  2791  ssdifeq0  3282  pwidg  3347  elpr2  3369  snidg  3375  exsnrex  3387  rabrsndc  3412  prid1g  3448  sssnr  3498  ssprr  3501  sstpr  3502  preqr1  3513  unimax  3588  intmin3  3616  syl6eqbr  3775  pwnss  3886  0inp0  3893  bnd2  3900  euabex  3935  copsexg  3955  euotd  3965  elopab  3969  epelg  4001  sucidg  4102  regexmidlem1  4202  sucprcreg  4211  onprc  4214  dtruex  4221  omelon2  4257  elvvuni  4331  eqrelriv  4360  relopabi  4390  opabid2  4394  ididg  4416  iss  4581  funopg  4860  fn0  4944  f00  5006  f1o00  5086  fo00  5087  brprcneu  5096  relelfvdm  5130  fsn  5260  eufnfv  5314  f1eqcocnv  5356  riotaprop  5415  acexmidlemb  5428  acexmidlemab  5430  acexmidlem2  5433  oprabid  5461  elrnmpt2  5537  ov6g  5561  eqop2  5727  1stconst  5765  2ndconst  5766  dftpos3  5799  dftpos4  5800  2pwuninelg  5820  ecopover  6115  1ne0sr  6513  00sr  6516  eqlei2  6708  bj-om  7159  bj-nn0suc0  7172  bj-nn0suc  7182  bj-nn0sucALT  7196  bj-findis  7197
  Copyright terms: Public domain W3C validator