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  1430  ceqsexv2d  2856  dedhb  2989  sbceqal  3101  ssdifeq0  3596  pwidg  3691  elpr2  3716  snidg  3723  exsnrex  3736  rabrsndc  3764  prid1g  3800  tpid1g  3809  tpid2g  3811  sssnr  3862  ssprr  3865  sstpr  3866  preqr1  3877  unimax  3953  intmin3  3981  eqbrtrdi  4153  if0elpw  4276  pwnss  4277  0inp0  4284  bnd2  4291  ss1o0el1  4315  exmidsssn  4320  exmidundif  4324  exmidundifim  4325  euabex  4346  copsexg  4365  euotd  4376  elopab  4381  epelg  4416  sucidg  4542  ifelpwung  4607  regexmidlem1  4660  sucprcreg  4676  onprc  4679  dtruex  4686  omelon2  4735  elvvuni  4819  eqrelriv  4848  relopabi  4885  opabid2  4891  ididg  4913  iss  5089  funopg  5391  fn0  5483  f00  5564  f0bi  5565  f10d  5655  f1o00  5656  fo00  5657  brprcneu  5668  relelfvdm  5707  fvmbr  5710  fsn  5854  funop  5866  eufnfv  5922  f1eqcocnv  5970  riotaprop  6037  acexmidlemb  6050  acexmidlemab  6052  acexmidlem2  6055  oprabid  6090  elrnmpo  6175  ov6g  6200  eqop2  6385  1stconst  6430  2ndconst  6431  dftpos3  6506  dftpos4  6507  2pwuninelg  6527  frecabcl  6643  el2oss1o  6689  ecopover  6880  map0g  6935  mapsnd  6936  mapsn  6938  elixpsn  6983  en0  7048  en1  7052  fiprc  7070  en2m  7079  dom0  7104  nneneq  7124  findcard  7158  findcard2  7159  findcard2s  7160  elssdc  7175  eqsndc  7176  sbthlem2  7241  sbthlemi4  7243  sbthlemi5  7244  2omap  7282  eldju2ndl  7376  updjudhf  7383  enumct  7419  nnnninf  7430  nninfisollem0  7434  fodjuomnilemdc  7448  exmidonfinlem  7509  exmidaclem  7528  pw1ne1  7552  pw1ne3  7553  1ne0sr  8097  00sr  8100  cnm  8163  eqlei2  8384  cnstab  8937  divcanap3  8992  sup3exmid  9251  nn1suc  9276  nn0ge0  9541  xnn0xr  9588  xnn0nemnf  9594  elnn0z  9610  nn0n0n1ge2b  9678  nn0ind-raph  9716  elnn1uz2  9960  indstr2  9962  xrnemnf  10132  xrnepnf  10133  mnfltxr  10141  nn0pnfge0  10146  xrlttr  10150  xrltso  10151  xrlttri3  10152  nltpnft  10169  npnflt  10170  ngtmnft  10172  nmnfgt  10173  xsubge0  10236  xposdif  10237  xleaddadd  10242  fztpval  10442  fseq1p1m1  10453  fz01or  10470  qbtwnxr  10644  xqltnle  10654  fzfig  10819  uzsinds  10833  ser0f  10923  1exp  10957  0exp  10963  bcn1  11148  en1hash  11191  hashfibc  11235  zfz1iso  11241  hash2en  11243  0wrd0  11278  wrdlen1  11290  wrdl1exs1  11345  swrdspsleq  11387  cats1un  11441  wrdind  11442  wrd2ind  11443  sqrt0rlem  11716  fzf1o  12089  prodf1f  12257  0dvds  12525  nn0o  12621  flodddiv4  12650  bitsp1o  12667  gcddvds  12687  bezoutlemmain  12722  lcmdvds  12804  rpdvds  12824  1nprm  12839  prmind2  12845  nnoddn2prmb  12988  pcpre1  13018  qexpz  13078  4sqlem19  13135  ballotfilem8  13227  ennnfonelemj0  13239  ennnfonelemhf1o  13251  strslfv  13344  restsspw  13549  xpsfrnel  13611  mgmidcl  13644  mgmlrid  13645  releqgg  13976  gsumgfsum1  14106  islidlm  14756  zrhrhm  14900  psrplusgg  14962  baspartn  15044  eltg3  15051  topnex  15080  discld  15130  cnpfval  15189  cnprcl2k  15200  idcn  15206  xmet0  15357  blfvalps  15379  blfps  15403  blf  15404  limcimolemlt  15658  recnprss  15681  lgsdir2lem2  16031  gausslemma2dlem4  16066  2lgslem2  16094  2lgslem3  16103  2lgs  16106  2sqlem7  16123  uhgr0e  16206  incistruhgr  16214  issubgr2  16382  subgrprop2  16384  egrsubgr  16387  0grsubgr  16388  0uhgrsubgr  16389  uhgrsubgrself  16390  clwwlkn1  16542  funmptd  16714  bj-om  16846  bj-nn0suc0  16859  bj-nn0suc  16873  bj-nn0sucALT  16887  bj-findis  16888  pw1map  16908  nninfall  16926  nnnninfen  16938  trilpolemcl  16960  dceqnconst  16985  dcapnconst  16986