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  2988  sbceqal  3100  ssdifeq0  3594  pwidg  3688  elpr2  3713  snidg  3720  exsnrex  3733  rabrsndc  3761  prid1g  3797  tpid1g  3806  tpid2g  3808  sssnr  3859  ssprr  3862  sstpr  3863  preqr1  3874  unimax  3950  intmin3  3978  eqbrtrdi  4150  if0elpw  4273  pwnss  4274  0inp0  4281  bnd2  4288  ss1o0el1  4312  exmidsssn  4317  exmidundif  4321  exmidundifim  4322  euabex  4343  copsexg  4362  euotd  4373  elopab  4378  epelg  4413  sucidg  4539  ifelpwung  4604  regexmidlem1  4657  sucprcreg  4673  onprc  4676  dtruex  4683  omelon2  4732  elvvuni  4816  eqrelriv  4845  relopabi  4882  opabid2  4888  ididg  4910  iss  5086  funopg  5388  fn0  5480  f00  5561  f0bi  5562  f10d  5652  f1o00  5653  fo00  5654  brprcneu  5665  relelfvdm  5704  fvmbr  5707  fsn  5851  funop  5863  eufnfv  5919  f1eqcocnv  5966  riotaprop  6031  acexmidlemb  6044  acexmidlemab  6046  acexmidlem2  6049  oprabid  6084  elrnmpo  6169  ov6g  6194  eqop2  6374  1stconst  6419  2ndconst  6420  dftpos3  6495  dftpos4  6496  2pwuninelg  6516  frecabcl  6632  el2oss1o  6678  ecopover  6869  map0g  6924  mapsnd  6925  mapsn  6927  elixpsn  6972  en0  7037  en1  7041  fiprc  7059  en2m  7068  dom0  7093  nneneq  7113  findcard  7147  findcard2  7148  findcard2s  7149  elssdc  7164  eqsndc  7165  sbthlem2  7230  sbthlemi4  7232  sbthlemi5  7233  2omap  7271  eldju2ndl  7365  updjudhf  7372  enumct  7408  nnnninf  7419  nninfisollem0  7423  fodjuomnilemdc  7437  exmidonfinlem  7498  exmidaclem  7517  pw1ne1  7541  pw1ne3  7542  1ne0sr  8086  00sr  8089  cnm  8152  eqlei2  8373  cnstab  8924  divcanap3  8977  sup3exmid  9236  nn1suc  9261  nn0ge0  9526  xnn0xr  9573  xnn0nemnf  9579  elnn0z  9595  nn0n0n1ge2b  9663  nn0ind-raph  9701  elnn1uz2  9945  indstr2  9947  xrnemnf  10116  xrnepnf  10117  mnfltxr  10125  nn0pnfge0  10130  xrlttr  10134  xrltso  10135  xrlttri3  10136  nltpnft  10153  npnflt  10154  ngtmnft  10156  nmnfgt  10157  xsubge0  10220  xposdif  10221  xleaddadd  10226  fztpval  10424  fseq1p1m1  10435  fz01or  10452  qbtwnxr  10624  xqltnle  10634  fzfig  10799  uzsinds  10813  ser0f  10903  1exp  10937  0exp  10943  bcn1  11128  en1hash  11171  hashfibc  11215  zfz1iso  11221  hash2en  11223  0wrd0  11258  wrdlen1  11270  wrdl1exs1  11325  swrdspsleq  11367  cats1un  11421  wrdind  11422  wrd2ind  11423  sqrt0rlem  11696  fzf1o  12069  prodf1f  12237  0dvds  12505  nn0o  12601  flodddiv4  12630  bitsp1o  12647  gcddvds  12667  bezoutlemmain  12702  lcmdvds  12784  rpdvds  12804  1nprm  12819  prmind2  12825  nnoddn2prmb  12968  pcpre1  12998  qexpz  13058  4sqlem19  13115  ennnfonelemj0  13173  ennnfonelemhf1o  13185  strslfv  13278  restsspw  13483  xpsfrnel  13578  mgmidcl  13612  mgmlrid  13613  releqgg  13958  islidlm  14676  zrhrhm  14820  psrplusgg  14882  baspartn  14964  eltg3  14971  topnex  15000  discld  15050  cnpfval  15109  cnprcl2k  15120  idcn  15126  xmet0  15277  blfvalps  15299  blfps  15323  blf  15324  limcimolemlt  15578  recnprss  15601  lgsdir2lem2  15951  gausslemma2dlem4  15986  2lgslem2  16014  2lgslem3  16023  2lgs  16026  2sqlem7  16043  uhgr0e  16126  incistruhgr  16134  issubgr2  16302  subgrprop2  16304  egrsubgr  16307  0grsubgr  16308  0uhgrsubgr  16309  uhgrsubgrself  16310  clwwlkn1  16462  funmptd  16624  bj-om  16756  bj-nn0suc0  16769  bj-nn0suc  16783  bj-nn0sucALT  16797  bj-findis  16798  pw1map  16818  nninfall  16836  nnnninfen  16848  trilpolemcl  16870  dceqnconst  16895  dcapnconst  16896  gsumgfsum1  16912