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  1375  dedhb  2894  sbceqal  3005  ssdifeq0  3490  pwidg  3572  elpr2  3597  snidg  3604  exsnrex  3617  rabrsndc  3643  prid1g  3679  tpid1g  3687  tpid2g  3689  sssnr  3732  ssprr  3735  sstpr  3736  preqr1  3747  unimax  3822  intmin3  3850  eqbrtrdi  4020  pwnss  4137  0inp0  4144  bnd2  4151  ss1o0el1  4175  exmidsssn  4180  exmidundif  4184  exmidundifim  4185  euabex  4202  copsexg  4221  euotd  4231  elopab  4235  epelg  4267  sucidg  4393  ifelpwung  4458  regexmidlem1  4509  sucprcreg  4525  onprc  4528  dtruex  4535  omelon2  4584  elvvuni  4667  eqrelriv  4696  relopabi  4729  opabid2  4734  ididg  4756  iss  4929  funopg  5221  fn0  5306  f00  5378  f0bi  5379  f1o00  5466  fo00  5467  brprcneu  5478  relelfvdm  5517  fsn  5656  eufnfv  5714  f1eqcocnv  5758  riotaprop  5820  acexmidlemb  5833  acexmidlemab  5835  acexmidlem2  5838  oprabid  5870  elrnmpo  5951  ov6g  5975  eqop2  6143  1stconst  6185  2ndconst  6186  dftpos3  6226  dftpos4  6227  2pwuninelg  6247  frecabcl  6363  el2oss1o  6407  ecopover  6595  map0g  6650  mapsn  6652  elixpsn  6697  en0  6757  en1  6761  fiprc  6777  dom0  6800  nneneq  6819  findcard  6850  findcard2  6851  findcard2s  6852  sbthlem2  6919  sbthlemi4  6921  sbthlemi5  6922  eldju2ndl  7033  updjudhf  7040  enumct  7076  nnnninf  7086  nninfisollem0  7090  fodjuomnilemdc  7104  exmidonfinlem  7145  exmidaclem  7160  pw1ne1  7181  pw1ne3  7182  1ne0sr  7703  00sr  7706  cnm  7769  eqlei2  7989  cnstab  8539  divcanap3  8590  sup3exmid  8848  nn1suc  8872  nn0ge0  9135  xnn0xr  9178  xnn0nemnf  9184  elnn0z  9200  nn0n0n1ge2b  9266  nn0ind-raph  9304  elnn1uz2  9541  indstr2  9543  xrnemnf  9709  xrnepnf  9710  mnfltxr  9718  nn0pnfge0  9723  xrlttr  9727  xrltso  9728  xrlttri3  9729  nltpnft  9746  npnflt  9747  ngtmnft  9749  nmnfgt  9750  xsubge0  9813  xposdif  9814  xleaddadd  9819  fztpval  10014  fseq1p1m1  10025  fz01or  10042  qbtwnxr  10189  fzfig  10361  uzsinds  10373  ser0f  10446  1exp  10480  0exp  10486  bcn1  10667  zfz1iso  10750  sqrt0rlem  10941  prodf1f  11480  0dvds  11747  nn0o  11840  flodddiv4  11867  gcddvds  11892  bezoutlemmain  11927  lcmdvds  12007  rpdvds  12027  1nprm  12042  prmind2  12048  nnoddn2prmb  12190  pcpre1  12220  qexpz  12278  ennnfonelemj0  12330  ennnfonelemhf1o  12342  strslfv  12434  restsspw  12561  baspartn  12648  eltg3  12657  topnex  12686  discld  12736  lmreltop  12793  cnpfval  12795  cnprcl2k  12806  idcn  12812  xmet0  12963  blfvalps  12985  blfps  13009  blf  13010  limcimolemlt  13233  recnprss  13256  lgsdir2lem2  13530  2sqlem7  13557  funmptd  13645  bj-om  13779  bj-nn0suc0  13792  bj-nn0suc  13806  bj-nn0sucALT  13820  bj-findis  13821  nninfall  13849  trilpolemcl  13876  dceqnconst  13898  dcapnconst  13899