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	⊢ 𝜒
mpbiri.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbiri	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbiri

Step	Hyp	Ref	Expression
1		mpbiri.min	. . 3 ⊢ 𝜒
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜒)
3		mpbiri.maj	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	mpbird 167	1 ⊢ (𝜑 → 𝜓)

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  1434  ceqsexv2d  2862  dedhb  2995  sbceqal  3107  ssdifeq0  3610  pwidg  3705  elpr2  3730  snidg  3737  exsnrex  3750  rabrsndc  3778  prid1g  3814  tpid1g  3823  tpid2g  3825  sssnr  3876  ssprr  3879  sstpr  3880  preqr1  3891  unimax  3967  intmin3  3995  eqbrtrdi  4167  if0elpw  4293  pwnss  4294  0inp0  4301  bnd2  4308  ss1o0el1  4332  exmidsssn  4337  exmidundif  4341  exmidundifim  4342  euabex  4363  copsexg  4382  euotd  4393  elopab  4398  epelg  4433  sucidg  4559  ifelpwung  4625  regexmidlem1  4678  sucprcreg  4694  onprc  4697  dtruex  4704  omelon2  4753  elvvuni  4837  eqrelriv  4866  relopabi  4903  opabid2  4909  ididg  4931  iss  5107  funopg  5409  fn0  5501  f00  5582  f0bi  5583  f10d  5673  f1o00  5674  fo00  5675  brprcneu  5686  relelfvdm  5725  fvmbr  5728  fsn  5874  funop  5886  eufnfv  5943  f1eqcocnv  5991  riotaprop  6058  acexmidlemb  6071  acexmidlemab  6073  acexmidlem2  6076  oprabid  6111  elrnmpo  6196  ov6g  6221  eqop2  6406  1stconst  6451  2ndconst  6452  dftpos3  6527  dftpos4  6528  2pwuninelg  6548  frecabcl  6664  el2oss1o  6710  ecopover  6901  map0g  6963  mapsnd  6964  mapsn  6966  elixpsn  7011  en0  7076  en1  7080  fiprc  7098  en2m  7107  dom0  7132  nneneq  7152  findcard  7186  findcard2  7187  findcard2s  7188  elssdc  7203  eqsndc  7204  sbthlem2  7269  sbthlemi4  7271  sbthlemi5  7272  2omap  7312  eldju2ndl  7406  updjudhf  7413  enumct  7449  nnnninf  7460  nninfisollem0  7464  fodjuomnilemdc  7478  exmidonfinlem  7539  exmidaclem  7558  pw1ne1  7582  pw1ne3  7583  1ne0sr  8127  00sr  8130  cnm  8193  eqlei2  8414  cnstab  8967  divcanap3  9022  sup3exmid  9281  nn1suc  9306  nn0ge0  9571  xnn0xr  9618  xnn0nemnf  9624  elnn0z  9640  nn0n0n1ge2b  9708  nn0ind-raph  9746  elnn1uz2  9990  indstr2  9992  xrnemnf  10162  xrnepnf  10163  mnfltxr  10171  nn0pnfge0  10176  xrlttr  10180  xrltso  10181  xrlttri3  10182  nltpnft  10199  npnflt  10200  ngtmnft  10202  nmnfgt  10203  xsubge0  10266  xposdif  10267  xleaddadd  10272  fztpval  10473  fseq1p1m1  10484  fz01or  10501  qbtwnxr  10675  xqltnle  10685  fzfig  10850  uzsinds  10864  ser0f  10954  1exp  10988  0exp  10994  bcn1  11179  en1hash  11222  hashfibc  11266  hashf1  11270  zfz1iso  11276  hash2en  11278  0wrd0  11313  wrdlen1  11325  wrdl1exs1  11380  swrdspsleq  11422  cats1un  11476  wrdind  11477  wrd2ind  11478  sq01  11643  sqrt0rlem  11752  fzf1o  12125  prodf1f  12293  0dvds  12561  nn0o  12657  flodddiv4  12686  bitsp1o  12703  gcddvds  12723  bezoutlemmain  12758  lcmdvds  12840  rpdvds  12860  1nprm  12875  prmind2  12881  nnoddn2prmb  13024  pcpre1  13054  qexpz  13114  4sqlem19  13171  ballotfilem8  13263  ennnfonelemj0  13275  ennnfonelemhf1o  13287  strslfv  13380  restsspw  13586  xpsfrnel  13648  mgmidcl  13681  mgmlrid  13682  releqgg  14006  gzsumgsum1  14136  islidlm  14799  zrhrhm  14941  psrplusgg  15052  baspartn  15134  eltg3  15141  topnex  15170  discld  15220  cnpfval  15279  cnprcl2k  15290  idcn  15296  xmet0  15447  blfvalps  15469  blfps  15493  blf  15494  limcimolemlt  15748  recnprss  15771  lgsdir2lem2  16131  gausslemma2dlem4  16166  2lgslem2  16194  2lgslem3  16203  2lgs  16206  2sqlem7  16223  uhgr0e  16306  incistruhgr  16314  issubgr2  16482  subgrprop2  16484  egrsubgr  16487  0grsubgr  16488  0uhgrsubgr  16489  uhgrsubgrself  16490  clwwlkn1  16642  funmptd  16814  bj-om  16946  bj-nn0suc0  16959  bj-nn0suc  16973  bj-nn0sucALT  16987  bj-findis  16988  pw1map  17008  nninfall  17026  nnnninfen  17038  trilpolemcl  17060  dceqnconst  17084  dcapnconst  17085