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  1427  ceqsexv2d  2840  dedhb  2972  sbceqal  3084  ssdifeq0  3574  pwidg  3663  elpr2  3688  snidg  3695  exsnrex  3708  rabrsndc  3734  prid1g  3770  tpid1g  3779  tpid2g  3781  sssnr  3831  ssprr  3834  sstpr  3835  preqr1  3846  unimax  3922  intmin3  3950  eqbrtrdi  4122  pwnss  4243  0inp0  4250  bnd2  4257  ss1o0el1  4281  exmidsssn  4286  exmidundif  4290  exmidundifim  4291  euabex  4311  copsexg  4330  euotd  4341  elopab  4346  epelg  4381  sucidg  4507  ifelpwung  4572  regexmidlem1  4625  sucprcreg  4641  onprc  4644  dtruex  4651  omelon2  4700  elvvuni  4783  eqrelriv  4812  relopabi  4847  opabid2  4853  ididg  4875  iss  5051  funopg  5352  fn0  5443  f00  5519  f0bi  5520  f10d  5609  f1o00  5610  fo00  5611  brprcneu  5622  relelfvdm  5661  fvmbr  5664  fsn  5809  funop  5820  eufnfv  5874  f1eqcocnv  5921  riotaprop  5986  acexmidlemb  5999  acexmidlemab  6001  acexmidlem2  6004  oprabid  6039  elrnmpo  6124  ov6g  6149  eqop2  6330  1stconst  6373  2ndconst  6374  dftpos3  6414  dftpos4  6415  2pwuninelg  6435  frecabcl  6551  el2oss1o  6597  ecopover  6788  map0g  6843  mapsn  6845  elixpsn  6890  en0  6955  en1  6959  fiprc  6976  en2m  6982  dom0  7007  nneneq  7026  findcard  7058  findcard2  7059  findcard2s  7060  sbthlem2  7133  sbthlemi4  7135  sbthlemi5  7136  eldju2ndl  7247  updjudhf  7254  enumct  7290  nnnninf  7301  nninfisollem0  7305  fodjuomnilemdc  7319  exmidonfinlem  7379  exmidaclem  7398  pw1ne1  7422  pw1ne3  7423  1ne0sr  7961  00sr  7964  cnm  8027  eqlei2  8249  cnstab  8800  divcanap3  8853  sup3exmid  9112  nn1suc  9137  nn0ge0  9402  xnn0xr  9445  xnn0nemnf  9451  elnn0z  9467  nn0n0n1ge2b  9534  nn0ind-raph  9572  elnn1uz2  9810  indstr2  9812  xrnemnf  9981  xrnepnf  9982  mnfltxr  9990  nn0pnfge0  9995  xrlttr  9999  xrltso  10000  xrlttri3  10001  nltpnft  10018  npnflt  10019  ngtmnft  10021  nmnfgt  10022  xsubge0  10085  xposdif  10086  xleaddadd  10091  fztpval  10287  fseq1p1m1  10298  fz01or  10315  qbtwnxr  10485  xqltnle  10495  fzfig  10660  uzsinds  10674  ser0f  10764  1exp  10798  0exp  10804  bcn1  10988  zfz1iso  11071  hash2en  11073  0wrd0  11105  wrdlen1  11117  wrdl1exs1  11170  swrdspsleq  11207  cats1un  11261  wrdind  11262  wrd2ind  11263  sqrt0rlem  11522  prodf1f  12062  0dvds  12330  nn0o  12426  flodddiv4  12455  bitsp1o  12472  gcddvds  12492  bezoutlemmain  12527  lcmdvds  12609  rpdvds  12629  1nprm  12644  prmind2  12650  nnoddn2prmb  12793  pcpre1  12823  qexpz  12883  4sqlem19  12940  ennnfonelemj0  12980  ennnfonelemhf1o  12992  strslfv  13085  restsspw  13290  xpsfrnel  13385  mgmidcl  13419  mgmlrid  13420  releqgg  13765  islidlm  14451  zrhrhm  14595  psrplusgg  14650  baspartn  14732  eltg3  14739  topnex  14768  discld  14818  cnpfval  14877  cnprcl2k  14888  idcn  14894  xmet0  15045  blfvalps  15067  blfps  15091  blf  15092  limcimolemlt  15346  recnprss  15369  lgsdir2lem2  15716  gausslemma2dlem4  15751  2lgslem2  15779  2lgslem3  15788  2lgs  15791  2sqlem7  15808  uhgr0e  15890  incistruhgr  15898  funmptd  16191  bj-om  16324  bj-nn0suc0  16337  bj-nn0suc  16351  bj-nn0sucALT  16365  bj-findis  16366  2omap  16388  pw1map  16390  nninfall  16405  nnnninfen  16417  trilpolemcl  16435  dceqnconst  16458  dcapnconst  16459