Theorem mpbiri 166

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 165	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm5.18im  1316  dedhb  2761  sbceqal  2869  ssdifeq0  3325  pwidg  3395  elpr2  3420  snidg  3423  exsnrex  3435  rabrsndc  3460  prid1g  3496  sssnr  3545  ssprr  3548  sstpr  3549  preqr1  3560  unimax  3635  intmin3  3663  syl6eqbr  3822  pwnss  3933  0inp0  3940  bnd2  3947  euabex  3980  copsexg  3999  euotd  4009  elopab  4013  epelg  4045  sucidg  4171  regexmidlem1  4276  sucprcreg  4292  onprc  4295  dtruex  4302  omelon2  4348  elvvuni  4422  eqrelriv  4451  relopabi  4481  opabid2  4485  ididg  4507  iss  4674  funopg  4954  fn0  5038  f00  5101  f1o00  5181  fo00  5182  brprcneu  5191  relelfvdm  5226  fsn  5356  eufnfv  5410  f1eqcocnv  5451  riotaprop  5511  acexmidlemb  5524  acexmidlemab  5526  acexmidlem2  5529  oprabid  5557  elrnmpt2  5634  ov6g  5658  eqop2  5824  1stconst  5862  2ndconst  5863  dftpos3  5900  dftpos4  5901  2pwuninelg  5921  ecopover  6227  en0  6298  en1  6302  fiprc  6315  nneneq  6343  findcard  6372  findcard2  6373  findcard2s  6374  1ne0sr  6943  00sr  6946  eqlei2  7205  divcanap3  7786  nn1suc  8058  nn0ge0  8313  elnn0z  8364  nn0n0n1ge2b  8427  nn0ind-raph  8464  elnn1uz2  8694  indstr2  8696  xrnemnf  8853  xrnepnf  8854  mnfltxr  8861  nn0pnfge0  8866  xrlttr  8870  xrltso  8871  xrlttri3  8872  nltpnft  8884  ngtmnft  8885  fztpval  9100  fseq1p1m1  9111  qbtwnxr  9266  fzfig  9422  uzsinds  9428  iser0f  9472  1exp  9505  0exp  9511  bcn1  9685  sqrt0rlem  9889  0dvds  10215  fz01or  10278  nn0o  10307  flodddiv4  10334  gcddvds  10355  bezoutlemmain  10387  lcmdvds  10461  rpdvds  10481  1nprm  10496  prmind2  10502  bj-om  10732  bj-nn0suc0  10745  bj-nn0suc  10759  bj-nn0sucALT  10773  bj-findis  10774