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  1429  ceqsexv2d  2843  dedhb  2975  sbceqal  3087  ssdifeq0  3577  pwidg  3666  elpr2  3691  snidg  3698  exsnrex  3711  rabrsndc  3739  prid1g  3775  tpid1g  3784  tpid2g  3786  sssnr  3836  ssprr  3839  sstpr  3840  preqr1  3851  unimax  3927  intmin3  3955  eqbrtrdi  4127  pwnss  4249  0inp0  4256  bnd2  4263  ss1o0el1  4287  exmidsssn  4292  exmidundif  4296  exmidundifim  4297  euabex  4317  copsexg  4336  euotd  4347  elopab  4352  epelg  4387  sucidg  4513  ifelpwung  4578  regexmidlem1  4631  sucprcreg  4647  onprc  4650  dtruex  4657  omelon2  4706  elvvuni  4790  eqrelriv  4819  relopabi  4855  opabid2  4861  ididg  4883  iss  5059  funopg  5360  fn0  5452  f00  5528  f0bi  5529  f10d  5619  f1o00  5620  fo00  5621  brprcneu  5632  relelfvdm  5671  fvmbr  5674  fsn  5819  funop  5831  eufnfv  5885  f1eqcocnv  5932  riotaprop  5997  acexmidlemb  6010  acexmidlemab  6012  acexmidlem2  6015  oprabid  6050  elrnmpo  6135  ov6g  6160  eqop2  6341  1stconst  6386  2ndconst  6387  dftpos3  6428  dftpos4  6429  2pwuninelg  6449  frecabcl  6565  el2oss1o  6611  ecopover  6802  map0g  6857  mapsn  6859  elixpsn  6904  en0  6969  en1  6973  fiprc  6990  en2m  6999  dom0  7024  nneneq  7043  findcard  7077  findcard2  7078  findcard2s  7079  elssdc  7094  eqsndc  7095  sbthlem2  7157  sbthlemi4  7159  sbthlemi5  7160  eldju2ndl  7271  updjudhf  7278  enumct  7314  nnnninf  7325  nninfisollem0  7329  fodjuomnilemdc  7343  exmidonfinlem  7404  exmidaclem  7423  pw1ne1  7447  pw1ne3  7448  1ne0sr  7986  00sr  7989  cnm  8052  eqlei2  8274  cnstab  8825  divcanap3  8878  sup3exmid  9137  nn1suc  9162  nn0ge0  9427  xnn0xr  9470  xnn0nemnf  9476  elnn0z  9492  nn0n0n1ge2b  9559  nn0ind-raph  9597  elnn1uz2  9841  indstr2  9843  xrnemnf  10012  xrnepnf  10013  mnfltxr  10021  nn0pnfge0  10026  xrlttr  10030  xrltso  10031  xrlttri3  10032  nltpnft  10049  npnflt  10050  ngtmnft  10052  nmnfgt  10053  xsubge0  10116  xposdif  10117  xleaddadd  10122  fztpval  10318  fseq1p1m1  10329  fz01or  10346  qbtwnxr  10518  xqltnle  10528  fzfig  10693  uzsinds  10707  ser0f  10797  1exp  10831  0exp  10837  bcn1  11021  en1hash  11063  zfz1iso  11106  hash2en  11108  0wrd0  11143  wrdlen1  11155  wrdl1exs1  11210  swrdspsleq  11252  cats1un  11306  wrdind  11307  wrd2ind  11308  sqrt0rlem  11568  fzf1o  11941  prodf1f  12109  0dvds  12377  nn0o  12473  flodddiv4  12502  bitsp1o  12519  gcddvds  12539  bezoutlemmain  12574  lcmdvds  12656  rpdvds  12676  1nprm  12691  prmind2  12697  nnoddn2prmb  12840  pcpre1  12870  qexpz  12930  4sqlem19  12987  ennnfonelemj0  13027  ennnfonelemhf1o  13039  strslfv  13132  restsspw  13337  xpsfrnel  13432  mgmidcl  13466  mgmlrid  13467  releqgg  13812  islidlm  14499  zrhrhm  14643  psrplusgg  14698  baspartn  14780  eltg3  14787  topnex  14816  discld  14866  cnpfval  14925  cnprcl2k  14936  idcn  14942  xmet0  15093  blfvalps  15115  blfps  15139  blf  15140  limcimolemlt  15394  recnprss  15417  lgsdir2lem2  15764  gausslemma2dlem4  15799  2lgslem2  15827  2lgslem3  15836  2lgs  15839  2sqlem7  15856  uhgr0e  15939  incistruhgr  15947  issubgr2  16115  subgrprop2  16117  egrsubgr  16120  0grsubgr  16121  0uhgrsubgr  16122  uhgrsubgrself  16123  clwwlkn1  16275  funmptd  16425  bj-om  16558  bj-nn0suc0  16571  bj-nn0suc  16585  bj-nn0sucALT  16599  bj-findis  16600  2omap  16620  pw1map  16622  nninfall  16637  nnnninfen  16649  trilpolemcl  16667  dceqnconst  16690  dcapnconst  16691  gsumgfsum1  16707