Theorem mpbiri 167

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 166	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.18im  1374  dedhb  2890  sbceqal  3001  ssdifeq0  3486  pwidg  3567  elpr2  3592  snidg  3599  exsnrex  3612  rabrsndc  3638  prid1g  3674  tpid1g  3682  tpid2g  3684  sssnr  3727  ssprr  3730  sstpr  3731  preqr1  3742  unimax  3817  intmin3  3845  eqbrtrdi  4015  pwnss  4132  0inp0  4139  bnd2  4146  ss1o0el1  4170  exmidsssn  4175  exmidundif  4179  exmidundifim  4180  euabex  4197  copsexg  4216  euotd  4226  elopab  4230  epelg  4262  sucidg  4388  ifelpwung  4453  regexmidlem1  4504  sucprcreg  4520  onprc  4523  dtruex  4530  omelon2  4579  elvvuni  4662  eqrelriv  4691  relopabi  4724  opabid2  4729  ididg  4751  iss  4924  funopg  5216  fn0  5301  f00  5373  f0bi  5374  f1o00  5461  fo00  5462  brprcneu  5473  relelfvdm  5512  fsn  5651  eufnfv  5709  f1eqcocnv  5753  riotaprop  5815  acexmidlemb  5828  acexmidlemab  5830  acexmidlem2  5833  oprabid  5865  elrnmpo  5946  ov6g  5970  eqop2  6138  1stconst  6180  2ndconst  6181  dftpos3  6221  dftpos4  6222  2pwuninelg  6242  frecabcl  6358  el2oss1o  6402  ecopover  6590  map0g  6645  mapsn  6647  elixpsn  6692  en0  6752  en1  6756  fiprc  6772  dom0  6795  nneneq  6814  findcard  6845  findcard2  6846  findcard2s  6847  sbthlem2  6914  sbthlemi4  6916  sbthlemi5  6917  eldju2ndl  7028  updjudhf  7035  enumct  7071  nnnninf  7081  nninfisollem0  7085  fodjuomnilemdc  7099  exmidonfinlem  7140  exmidaclem  7155  pw1ne1  7176  pw1ne3  7177  1ne0sr  7698  00sr  7701  cnm  7764  eqlei2  7984  cnstab  8534  divcanap3  8585  sup3exmid  8843  nn1suc  8867  nn0ge0  9130  xnn0xr  9173  xnn0nemnf  9179  elnn0z  9195  nn0n0n1ge2b  9261  nn0ind-raph  9299  elnn1uz2  9536  indstr2  9538  xrnemnf  9704  xrnepnf  9705  mnfltxr  9713  nn0pnfge0  9718  xrlttr  9722  xrltso  9723  xrlttri3  9724  nltpnft  9741  npnflt  9742  ngtmnft  9744  nmnfgt  9745  xsubge0  9808  xposdif  9809  xleaddadd  9814  fztpval  10008  fseq1p1m1  10019  fz01or  10036  qbtwnxr  10183  fzfig  10355  uzsinds  10367  ser0f  10440  1exp  10474  0exp  10480  bcn1  10660  zfz1iso  10740  sqrt0rlem  10931  prodf1f  11470  0dvds  11737  nn0o  11829  flodddiv4  11856  gcddvds  11881  bezoutlemmain  11916  lcmdvds  11990  rpdvds  12010  1nprm  12025  prmind2  12031  nnoddn2prmb  12171  pcpre1  12201  qexpz  12259  ennnfonelemj0  12271  ennnfonelemhf1o  12283  strslfv  12375  restsspw  12502  baspartn  12589  eltg3  12598  topnex  12627  discld  12677  lmreltop  12734  cnpfval  12736  cnprcl2k  12747  idcn  12753  xmet0  12904  blfvalps  12926  blfps  12950  blf  12951  limcimolemlt  13174  recnprss  13197  funmptd  13520  bj-om  13654  bj-nn0suc0  13667  bj-nn0suc  13681  bj-nn0sucALT  13695  bj-findis  13696  nninfall  13723  trilpolemcl  13750  dceqnconst  13772  dcapnconst  13773