Theorem mpbiri 168

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.18im  1405  ceqsexv2d  2814  dedhb  2944  sbceqal  3056  ssdifeq0  3545  pwidg  3632  elpr2  3657  snidg  3664  exsnrex  3677  rabrsndc  3703  prid1g  3739  tpid1g  3747  tpid2g  3749  sssnr  3797  ssprr  3800  sstpr  3801  preqr1  3812  unimax  3887  intmin3  3915  eqbrtrdi  4087  pwnss  4208  0inp0  4215  bnd2  4222  ss1o0el1  4246  exmidsssn  4251  exmidundif  4255  exmidundifim  4256  euabex  4274  copsexg  4293  euotd  4304  elopab  4309  epelg  4342  sucidg  4468  ifelpwung  4533  regexmidlem1  4586  sucprcreg  4602  onprc  4605  dtruex  4612  omelon2  4661  elvvuni  4744  eqrelriv  4773  relopabi  4808  opabid2  4814  ididg  4836  iss  5011  funopg  5311  fn0  5402  f00  5476  f0bi  5477  f10d  5566  f1o00  5567  fo00  5568  brprcneu  5579  relelfvdm  5618  fsn  5762  funop  5773  eufnfv  5825  f1eqcocnv  5870  riotaprop  5933  acexmidlemb  5946  acexmidlemab  5948  acexmidlem2  5951  oprabid  5986  elrnmpo  6069  ov6g  6094  eqop2  6274  1stconst  6317  2ndconst  6318  dftpos3  6358  dftpos4  6359  2pwuninelg  6379  frecabcl  6495  el2oss1o  6539  ecopover  6730  map0g  6785  mapsn  6787  elixpsn  6832  en0  6897  en1  6901  fiprc  6918  en2m  6924  dom0  6947  nneneq  6966  findcard  6997  findcard2  6998  findcard2s  6999  sbthlem2  7072  sbthlemi4  7074  sbthlemi5  7075  eldju2ndl  7186  updjudhf  7193  enumct  7229  nnnninf  7240  nninfisollem0  7244  fodjuomnilemdc  7258  exmidonfinlem  7314  exmidaclem  7333  pw1ne1  7354  pw1ne3  7355  1ne0sr  7892  00sr  7895  cnm  7958  eqlei2  8180  cnstab  8731  divcanap3  8784  sup3exmid  9043  nn1suc  9068  nn0ge0  9333  xnn0xr  9376  xnn0nemnf  9382  elnn0z  9398  nn0n0n1ge2b  9465  nn0ind-raph  9503  elnn1uz2  9741  indstr2  9743  xrnemnf  9912  xrnepnf  9913  mnfltxr  9921  nn0pnfge0  9926  xrlttr  9930  xrltso  9931  xrlttri3  9932  nltpnft  9949  npnflt  9950  ngtmnft  9952  nmnfgt  9953  xsubge0  10016  xposdif  10017  xleaddadd  10022  fztpval  10218  fseq1p1m1  10229  fz01or  10246  qbtwnxr  10413  xqltnle  10423  fzfig  10588  uzsinds  10602  ser0f  10692  1exp  10726  0exp  10732  bcn1  10916  zfz1iso  10999  hash2en  11001  0wrd0  11033  wrdlen1  11044  wrdl1exs1  11097  swrdspsleq  11134  sqrt0rlem  11364  prodf1f  11904  0dvds  12172  nn0o  12268  flodddiv4  12297  bitsp1o  12314  gcddvds  12334  bezoutlemmain  12369  lcmdvds  12451  rpdvds  12471  1nprm  12486  prmind2  12492  nnoddn2prmb  12635  pcpre1  12665  qexpz  12725  4sqlem19  12782  ennnfonelemj0  12822  ennnfonelemhf1o  12834  strslfv  12927  restsspw  13131  xpsfrnel  13226  mgmidcl  13260  mgmlrid  13261  releqgg  13606  islidlm  14291  zrhrhm  14435  psrplusgg  14490  baspartn  14572  eltg3  14579  topnex  14608  discld  14658  lmreltop  14715  cnpfval  14717  cnprcl2k  14728  idcn  14734  xmet0  14885  blfvalps  14907  blfps  14931  blf  14932  limcimolemlt  15186  recnprss  15209  lgsdir2lem2  15556  gausslemma2dlem4  15591  2lgslem2  15619  2lgslem3  15628  2lgs  15631  2sqlem7  15648  uhgr0e  15728  incistruhgr  15736  funmptd  15853  bj-om  15987  bj-nn0suc0  16000  bj-nn0suc  16014  bj-nn0sucALT  16028  bj-findis  16029  2omap  16047  nninfall  16061  nnnninfen  16073  trilpolemcl  16091  dceqnconst  16114  dcapnconst  16115