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  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  11140  wrdlen1  11152  wrdl1exs1  11207  swrdspsleq  11249  cats1un  11303  wrdind  11304  wrd2ind  11305  sqrt0rlem  11565  fzf1o  11938  prodf1f  12106  0dvds  12374  nn0o  12470  flodddiv4  12499  bitsp1o  12516  gcddvds  12536  bezoutlemmain  12571  lcmdvds  12653  rpdvds  12673  1nprm  12688  prmind2  12694  nnoddn2prmb  12837  pcpre1  12867  qexpz  12927  4sqlem19  12984  ennnfonelemj0  13024  ennnfonelemhf1o  13036  strslfv  13129  restsspw  13334  xpsfrnel  13429  mgmidcl  13463  mgmlrid  13464  releqgg  13809  islidlm  14496  zrhrhm  14640  psrplusgg  14695  baspartn  14777  eltg3  14784  topnex  14813  discld  14863  cnpfval  14922  cnprcl2k  14933  idcn  14939  xmet0  15090  blfvalps  15112  blfps  15136  blf  15137  limcimolemlt  15391  recnprss  15414  lgsdir2lem2  15761  gausslemma2dlem4  15796  2lgslem2  15824  2lgslem3  15833  2lgs  15836  2sqlem7  15853  uhgr0e  15936  incistruhgr  15944  issubgr2  16112  subgrprop2  16114  egrsubgr  16117  0grsubgr  16118  0uhgrsubgr  16119  uhgrsubgrself  16120  clwwlkn1  16272  funmptd  16420  bj-om  16553  bj-nn0suc0  16566  bj-nn0suc  16580  bj-nn0sucALT  16594  bj-findis  16595  2omap  16615  pw1map  16617  nninfall  16632  nnnninfen  16644  trilpolemcl  16662  dceqnconst  16685  dcapnconst  16686  gsumgfsum1  16702