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  1427  ceqsexv2d  2840  dedhb  2972  sbceqal  3084  ssdifeq0  3574  pwidg  3663  elpr2  3688  snidg  3695  exsnrex  3708  rabrsndc  3734  prid1g  3770  tpid1g  3778  tpid2g  3780  sssnr  3830  ssprr  3833  sstpr  3834  preqr1  3845  unimax  3921  intmin3  3949  eqbrtrdi  4121  pwnss  4242  0inp0  4249  bnd2  4256  ss1o0el1  4280  exmidsssn  4285  exmidundif  4289  exmidundifim  4290  euabex  4310  copsexg  4329  euotd  4340  elopab  4345  epelg  4378  sucidg  4504  ifelpwung  4569  regexmidlem1  4622  sucprcreg  4638  onprc  4641  dtruex  4648  omelon2  4697  elvvuni  4780  eqrelriv  4809  relopabi  4844  opabid2  4850  ididg  4872  iss  5047  funopg  5348  fn0  5439  f00  5513  f0bi  5514  f10d  5603  f1o00  5604  fo00  5605  brprcneu  5616  relelfvdm  5655  fsn  5800  funop  5811  eufnfv  5863  f1eqcocnv  5908  riotaprop  5973  acexmidlemb  5986  acexmidlemab  5988  acexmidlem2  5991  oprabid  6026  elrnmpo  6109  ov6g  6134  eqop2  6314  1stconst  6357  2ndconst  6358  dftpos3  6398  dftpos4  6399  2pwuninelg  6419  frecabcl  6535  el2oss1o  6579  ecopover  6770  map0g  6825  mapsn  6827  elixpsn  6872  en0  6937  en1  6941  fiprc  6958  en2m  6964  dom0  6987  nneneq  7006  findcard  7038  findcard2  7039  findcard2s  7040  sbthlem2  7113  sbthlemi4  7115  sbthlemi5  7116  eldju2ndl  7227  updjudhf  7234  enumct  7270  nnnninf  7281  nninfisollem0  7285  fodjuomnilemdc  7299  exmidonfinlem  7359  exmidaclem  7378  pw1ne1  7402  pw1ne3  7403  1ne0sr  7941  00sr  7944  cnm  8007  eqlei2  8229  cnstab  8780  divcanap3  8833  sup3exmid  9092  nn1suc  9117  nn0ge0  9382  xnn0xr  9425  xnn0nemnf  9431  elnn0z  9447  nn0n0n1ge2b  9514  nn0ind-raph  9552  elnn1uz2  9790  indstr2  9792  xrnemnf  9961  xrnepnf  9962  mnfltxr  9970  nn0pnfge0  9975  xrlttr  9979  xrltso  9980  xrlttri3  9981  nltpnft  9998  npnflt  9999  ngtmnft  10001  nmnfgt  10002  xsubge0  10065  xposdif  10066  xleaddadd  10071  fztpval  10267  fseq1p1m1  10278  fz01or  10295  qbtwnxr  10464  xqltnle  10474  fzfig  10639  uzsinds  10653  ser0f  10743  1exp  10777  0exp  10783  bcn1  10967  zfz1iso  11050  hash2en  11052  0wrd0  11084  wrdlen1  11095  wrdl1exs1  11148  swrdspsleq  11185  cats1un  11239  wrdind  11240  wrd2ind  11241  sqrt0rlem  11500  prodf1f  12040  0dvds  12308  nn0o  12404  flodddiv4  12433  bitsp1o  12450  gcddvds  12470  bezoutlemmain  12505  lcmdvds  12587  rpdvds  12607  1nprm  12622  prmind2  12628  nnoddn2prmb  12771  pcpre1  12801  qexpz  12861  4sqlem19  12918  ennnfonelemj0  12958  ennnfonelemhf1o  12970  strslfv  13063  restsspw  13268  xpsfrnel  13363  mgmidcl  13397  mgmlrid  13398  releqgg  13743  islidlm  14428  zrhrhm  14572  psrplusgg  14627  baspartn  14709  eltg3  14716  topnex  14745  discld  14795  lmreltop  14852  cnpfval  14854  cnprcl2k  14865  idcn  14871  xmet0  15022  blfvalps  15044  blfps  15068  blf  15069  limcimolemlt  15323  recnprss  15346  lgsdir2lem2  15693  gausslemma2dlem4  15728  2lgslem2  15756  2lgslem3  15765  2lgs  15768  2sqlem7  15785  uhgr0e  15867  incistruhgr  15875  funmptd  16097  bj-om  16230  bj-nn0suc0  16243  bj-nn0suc  16257  bj-nn0sucALT  16271  bj-findis  16272  2omap  16290  pw1map  16292  nninfall  16306  nnnninfen  16318  trilpolemcl  16336  dceqnconst  16359  dcapnconst  16360