Theorem mpbiri 167

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.18im  1363  dedhb  2853  sbceqal  2964  ssdifeq0  3445  pwidg  3524  elpr2  3549  snidg  3554  exsnrex  3566  rabrsndc  3591  prid1g  3627  tpid1g  3635  tpid2g  3637  sssnr  3680  ssprr  3683  sstpr  3684  preqr1  3695  unimax  3770  intmin3  3798  eqbrtrdi  3967  pwnss  4083  0inp0  4090  bnd2  4097  exmid01  4121  exmidsssn  4125  exmidundif  4129  exmidundifim  4130  euabex  4147  copsexg  4166  euotd  4176  elopab  4180  epelg  4212  sucidg  4338  regexmidlem1  4448  sucprcreg  4464  onprc  4467  dtruex  4474  omelon2  4521  elvvuni  4603  eqrelriv  4632  relopabi  4665  opabid2  4670  ididg  4692  iss  4865  funopg  5157  fn0  5242  f00  5314  f0bi  5315  f1o00  5402  fo00  5403  brprcneu  5414  relelfvdm  5453  fsn  5592  eufnfv  5648  f1eqcocnv  5692  riotaprop  5753  acexmidlemb  5766  acexmidlemab  5768  acexmidlem2  5771  oprabid  5803  elrnmpo  5884  ov6g  5908  eqop2  6076  1stconst  6118  2ndconst  6119  dftpos3  6159  dftpos4  6160  2pwuninelg  6180  frecabcl  6296  ecopover  6527  map0g  6582  mapsn  6584  elixpsn  6629  en0  6689  en1  6693  fiprc  6709  dom0  6732  nneneq  6751  findcard  6782  findcard2  6783  findcard2s  6784  sbthlem2  6846  sbthlemi4  6848  sbthlemi5  6849  eldju2ndl  6957  updjudhf  6964  enumct  7000  fodjuomnilemdc  7016  nnnninf  7023  exmidonfinlem  7049  exmidaclem  7064  1ne0sr  7574  00sr  7577  cnm  7640  eqlei2  7858  divcanap3  8458  sup3exmid  8715  nn1suc  8739  nn0ge0  9002  xnn0xr  9045  xnn0nemnf  9051  elnn0z  9067  nn0n0n1ge2b  9130  nn0ind-raph  9168  elnn1uz2  9401  indstr2  9403  xrnemnf  9564  xrnepnf  9565  mnfltxr  9572  nn0pnfge0  9577  xrlttr  9581  xrltso  9582  xrlttri3  9583  nltpnft  9597  npnflt  9598  ngtmnft  9600  nmnfgt  9601  xsubge0  9664  xposdif  9665  xleaddadd  9670  fztpval  9863  fseq1p1m1  9874  fz01or  9891  qbtwnxr  10035  fzfig  10203  uzsinds  10215  ser0f  10288  1exp  10322  0exp  10328  bcn1  10504  zfz1iso  10584  sqrt0rlem  10775  prodf1f  11312  0dvds  11513  nn0o  11604  flodddiv4  11631  gcddvds  11652  bezoutlemmain  11686  lcmdvds  11760  rpdvds  11780  1nprm  11795  prmind2  11801  ennnfonelemj0  11914  ennnfonelemhf1o  11926  strslfv  12003  restsspw  12130  baspartn  12217  eltg3  12226  topnex  12255  discld  12305  lmreltop  12362  cnpfval  12364  cnprcl2k  12375  idcn  12381  xmet0  12532  blfvalps  12554  blfps  12578  blf  12579  limcimolemlt  12802  recnprss  12825  bj-om  13135  bj-nn0suc0  13148  bj-nn0suc  13162  bj-nn0sucALT  13176  bj-findis  13177  el2oss1o  13188  nninfall  13204  trilpolemcl  13230