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	|- ch
mpbiri.maj	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mpbiri	|- ( ph -> ps )

Proof of Theorem mpbiri

Step	Hyp	Ref	Expression
1		mpbiri.min	. . 3 |- ch
2	1	a1i 9	. 2 |- ( ph -> ch )
3		mpbiri.maj	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	mpbird 156	1 |- ( ph -> ps )

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  1276  dedhb  2710  sbceqal  2814  ssdifeq0  3305  pwidg  3372  elpr2  3397  snidg  3400  exsnrex  3413  rabrsndc  3438  prid1g  3474  sssnr  3524  ssprr  3527  sstpr  3528  preqr1  3539  unimax  3614  intmin3  3642  syl6eqbr  3801  pwnss  3912  0inp0  3919  bnd2  3926  euabex  3961  copsexg  3981  euotd  3991  elopab  3995  epelg  4027  sucidg  4153  regexmidlem1  4258  sucprcreg  4273  onprc  4276  dtruex  4283  omelon2  4330  elvvuni  4404  eqrelriv  4433  relopabi  4463  opabid2  4467  ididg  4489  iss  4654  funopg  4934  fn0  5018  f00  5081  f1o00  5161  fo00  5162  brprcneu  5171  relelfvdm  5205  fsn  5335  eufnfv  5389  f1eqcocnv  5431  riotaprop  5491  acexmidlemb  5504  acexmidlemab  5506  acexmidlem2  5509  oprabid  5537  elrnmpt2  5614  ov6g  5638  eqop2  5804  1stconst  5842  2ndconst  5843  dftpos3  5877  dftpos4  5878  2pwuninelg  5898  ecopover  6204  en0  6275  en1  6279  fiprc  6292  nneneq  6320  findcard  6345  findcard2  6346  findcard2s  6347  1ne0sr  6851  00sr  6854  eqlei2  7112  divcanap3  7675  nn1suc  7933  nn0ge0  8207  elnn0z  8258  nn0n0n1ge2b  8320  nn0ind-raph  8355  elnn1uz2  8544  indstr2  8546  xrnemnf  8699  xrnepnf  8700  mnfltxr  8707  nn0pnfge0  8712  xrlttr  8716  xrltso  8717  xrlttri3  8718  nltpnft  8730  ngtmnft  8731  fztpval  8945  fseq1p1m1  8956  fzfig  9206  iser0f  9251  1exp  9284  0exp  9290  sqrt0rlem  9601  bj-om  10061  bj-nn0suc0  10075  bj-nn0suc  10089  bj-nn0sucALT  10103  bj-findis  10104