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  2841  dedhb  2973  sbceqal  3085  ssdifeq0  3575  pwidg  3664  elpr2  3689  snidg  3696  exsnrex  3709  rabrsndc  3737  prid1g  3773  tpid1g  3782  tpid2g  3784  sssnr  3834  ssprr  3837  sstpr  3838  preqr1  3849  unimax  3925  intmin3  3953  eqbrtrdi  4125  pwnss  4247  0inp0  4254  bnd2  4261  ss1o0el1  4285  exmidsssn  4290  exmidundif  4294  exmidundifim  4295  euabex  4315  copsexg  4334  euotd  4345  elopab  4350  epelg  4385  sucidg  4511  ifelpwung  4576  regexmidlem1  4629  sucprcreg  4645  onprc  4648  dtruex  4655  omelon2  4704  elvvuni  4788  eqrelriv  4817  relopabi  4853  opabid2  4859  ididg  4881  iss  5057  funopg  5358  fn0  5449  f00  5525  f0bi  5526  f10d  5615  f1o00  5616  fo00  5617  brprcneu  5628  relelfvdm  5667  fvmbr  5670  fsn  5815  funop  5826  eufnfv  5880  f1eqcocnv  5927  riotaprop  5992  acexmidlemb  6005  acexmidlemab  6007  acexmidlem2  6010  oprabid  6045  elrnmpo  6130  ov6g  6155  eqop2  6336  1stconst  6381  2ndconst  6382  dftpos3  6423  dftpos4  6424  2pwuninelg  6444  frecabcl  6560  el2oss1o  6606  ecopover  6797  map0g  6852  mapsn  6854  elixpsn  6899  en0  6964  en1  6968  fiprc  6985  en2m  6994  dom0  7019  nneneq  7038  findcard  7072  findcard2  7073  findcard2s  7074  elssdc  7089  eqsndc  7090  sbthlem2  7151  sbthlemi4  7153  sbthlemi5  7154  eldju2ndl  7265  updjudhf  7272  enumct  7308  nnnninf  7319  nninfisollem0  7323  fodjuomnilemdc  7337  exmidonfinlem  7397  exmidaclem  7416  pw1ne1  7440  pw1ne3  7441  1ne0sr  7979  00sr  7982  cnm  8045  eqlei2  8267  cnstab  8818  divcanap3  8871  sup3exmid  9130  nn1suc  9155  nn0ge0  9420  xnn0xr  9463  xnn0nemnf  9469  elnn0z  9485  nn0n0n1ge2b  9552  nn0ind-raph  9590  elnn1uz2  9834  indstr2  9836  xrnemnf  10005  xrnepnf  10006  mnfltxr  10014  nn0pnfge0  10019  xrlttr  10023  xrltso  10024  xrlttri3  10025  nltpnft  10042  npnflt  10043  ngtmnft  10045  nmnfgt  10046  xsubge0  10109  xposdif  10110  xleaddadd  10115  fztpval  10311  fseq1p1m1  10322  fz01or  10339  qbtwnxr  10510  xqltnle  10520  fzfig  10685  uzsinds  10699  ser0f  10789  1exp  10823  0exp  10829  bcn1  11013  en1hash  11055  zfz1iso  11098  hash2en  11100  0wrd0  11132  wrdlen1  11144  wrdl1exs1  11199  swrdspsleq  11241  cats1un  11295  wrdind  11296  wrd2ind  11297  sqrt0rlem  11557  prodf1f  12097  0dvds  12365  nn0o  12461  flodddiv4  12490  bitsp1o  12507  gcddvds  12527  bezoutlemmain  12562  lcmdvds  12644  rpdvds  12664  1nprm  12679  prmind2  12685  nnoddn2prmb  12828  pcpre1  12858  qexpz  12918  4sqlem19  12975  ennnfonelemj0  13015  ennnfonelemhf1o  13027  strslfv  13120  restsspw  13325  xpsfrnel  13420  mgmidcl  13454  mgmlrid  13455  releqgg  13800  islidlm  14486  zrhrhm  14630  psrplusgg  14685  baspartn  14767  eltg3  14774  topnex  14803  discld  14853  cnpfval  14912  cnprcl2k  14923  idcn  14929  xmet0  15080  blfvalps  15102  blfps  15126  blf  15127  limcimolemlt  15381  recnprss  15404  lgsdir2lem2  15751  gausslemma2dlem4  15786  2lgslem2  15814  2lgslem3  15823  2lgs  15826  2sqlem7  15843  uhgr0e  15926  incistruhgr  15934  clwwlkn1  16227  funmptd  16349  bj-om  16482  bj-nn0suc0  16495  bj-nn0suc  16509  bj-nn0sucALT  16523  bj-findis  16524  2omap  16544  pw1map  16546  nninfall  16561  nnnninfen  16573  trilpolemcl  16591  dceqnconst  16614  dcapnconst  16615  gsumgfsum1  16631