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  10517  xqltnle  10527  fzfig  10692  uzsinds  10706  ser0f  10796  1exp  10830  0exp  10836  bcn1  11020  en1hash  11062  zfz1iso  11105  hash2en  11107  0wrd0  11139  wrdlen1  11151  wrdl1exs1  11206  swrdspsleq  11248  cats1un  11302  wrdind  11303  wrd2ind  11304  sqrt0rlem  11564  fzf1o  11937  prodf1f  12105  0dvds  12373  nn0o  12469  flodddiv4  12498  bitsp1o  12515  gcddvds  12535  bezoutlemmain  12570  lcmdvds  12652  rpdvds  12672  1nprm  12687  prmind2  12693  nnoddn2prmb  12836  pcpre1  12866  qexpz  12926  4sqlem19  12983  ennnfonelemj0  13023  ennnfonelemhf1o  13035  strslfv  13128  restsspw  13333  xpsfrnel  13428  mgmidcl  13462  mgmlrid  13463  releqgg  13808  islidlm  14495  zrhrhm  14639  psrplusgg  14694  baspartn  14776  eltg3  14783  topnex  14812  discld  14862  cnpfval  14921  cnprcl2k  14932  idcn  14938  xmet0  15089  blfvalps  15111  blfps  15135  blf  15136  limcimolemlt  15390  recnprss  15413  lgsdir2lem2  15760  gausslemma2dlem4  15795  2lgslem2  15823  2lgslem3  15832  2lgs  15835  2sqlem7  15852  uhgr0e  15935  incistruhgr  15943  issubgr2  16111  subgrprop2  16113  egrsubgr  16116  0grsubgr  16117  0uhgrsubgr  16118  uhgrsubgrself  16119  clwwlkn1  16271  funmptd  16402  bj-om  16535  bj-nn0suc0  16548  bj-nn0suc  16562  bj-nn0sucALT  16576  bj-findis  16577  2omap  16597  pw1map  16599  nninfall  16614  nnnninfen  16626  trilpolemcl  16644  dceqnconst  16667  dcapnconst  16668  gsumgfsum1  16684