ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbiri Unicode 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  |-  ch
mpbiri.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mpbiri  |-  ( ph  ->  ps )

Proof of Theorem mpbiri
StepHypRef Expression
1 mpbiri.min . . 3  |-  ch
21a1i 9 . 2  |-  ( ph  ->  ch )
3 mpbiri.maj . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3mpbird 160 1  |-  ( ph  ->  ps )
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  1292  dedhb  2733  sbceqal  2841  ssdifeq0  3333  pwidg  3400  elpr2  3425  snidg  3428  exsnrex  3441  rabrsndc  3466  prid1g  3502  sssnr  3552  ssprr  3555  sstpr  3556  preqr1  3567  unimax  3642  intmin3  3670  syl6eqbr  3829  pwnss  3940  0inp0  3947  bnd2  3954  euabex  3989  copsexg  4009  euotd  4019  elopab  4023  epelg  4055  sucidg  4181  regexmidlem1  4286  sucprcreg  4301  onprc  4304  dtruex  4311  omelon2  4358  elvvuni  4432  eqrelriv  4461  relopabi  4491  opabid2  4495  ididg  4517  iss  4682  funopg  4962  fn0  5046  f00  5109  f1o00  5189  fo00  5190  brprcneu  5199  relelfvdm  5233  fsn  5363  eufnfv  5417  f1eqcocnv  5459  riotaprop  5519  acexmidlemb  5532  acexmidlemab  5534  acexmidlem2  5537  oprabid  5565  elrnmpt2  5642  ov6g  5666  eqop2  5832  1stconst  5870  2ndconst  5871  dftpos3  5908  dftpos4  5909  2pwuninelg  5929  ecopover  6235  en0  6306  en1  6310  fiprc  6323  nneneq  6351  findcard  6376  findcard2  6377  findcard2s  6378  1ne0sr  6909  00sr  6912  eqlei2  7171  divcanap3  7749  nn1suc  8009  nn0ge0  8264  elnn0z  8315  nn0n0n1ge2b  8378  nn0ind-raph  8414  elnn1uz2  8641  indstr2  8643  xrnemnf  8800  xrnepnf  8801  mnfltxr  8808  nn0pnfge0  8813  xrlttr  8817  xrltso  8818  xrlttri3  8819  nltpnft  8831  ngtmnft  8832  fztpval  9047  fseq1p1m1  9058  qbtwnxr  9214  fzfig  9370  iser0f  9416  1exp  9449  0exp  9455  bcn1  9626  sqrt0rlem  9830  0dvds  10128  fz01or  10190  nn0o  10219  flodddiv4  10246  bj-om  10448  bj-nn0suc0  10462  bj-nn0suc  10476  bj-nn0sucALT  10490  bj-findis  10491
  Copyright terms: Public domain W3C validator