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  1396  ceqsexv2d  2800  dedhb  2930  sbceqal  3042  ssdifeq0  3530  pwidg  3616  elpr2  3641  snidg  3648  exsnrex  3661  rabrsndc  3687  prid1g  3723  tpid1g  3731  tpid2g  3733  sssnr  3780  ssprr  3783  sstpr  3784  preqr1  3795  unimax  3870  intmin3  3898  eqbrtrdi  4069  pwnss  4189  0inp0  4196  bnd2  4203  ss1o0el1  4227  exmidsssn  4232  exmidundif  4236  exmidundifim  4237  euabex  4255  copsexg  4274  euotd  4284  elopab  4289  epelg  4322  sucidg  4448  ifelpwung  4513  regexmidlem1  4566  sucprcreg  4582  onprc  4585  dtruex  4592  omelon2  4641  elvvuni  4724  eqrelriv  4753  relopabi  4788  opabid2  4794  ididg  4816  iss  4989  funopg  5289  fn0  5374  f00  5446  f0bi  5447  f1o00  5536  fo00  5537  brprcneu  5548  relelfvdm  5587  fsn  5731  eufnfv  5790  f1eqcocnv  5835  riotaprop  5898  acexmidlemb  5911  acexmidlemab  5913  acexmidlem2  5916  oprabid  5951  elrnmpo  6033  ov6g  6058  eqop2  6233  1stconst  6276  2ndconst  6277  dftpos3  6317  dftpos4  6318  2pwuninelg  6338  frecabcl  6454  el2oss1o  6498  ecopover  6689  map0g  6744  mapsn  6746  elixpsn  6791  en0  6851  en1  6855  fiprc  6871  dom0  6896  nneneq  6915  findcard  6946  findcard2  6947  findcard2s  6948  sbthlem2  7019  sbthlemi4  7021  sbthlemi5  7022  eldju2ndl  7133  updjudhf  7140  enumct  7176  nnnninf  7187  nninfisollem0  7191  fodjuomnilemdc  7205  exmidonfinlem  7255  exmidaclem  7270  pw1ne1  7291  pw1ne3  7292  1ne0sr  7828  00sr  7831  cnm  7894  eqlei2  8116  cnstab  8666  divcanap3  8719  sup3exmid  8978  nn1suc  9003  nn0ge0  9268  xnn0xr  9311  xnn0nemnf  9317  elnn0z  9333  nn0n0n1ge2b  9399  nn0ind-raph  9437  elnn1uz2  9675  indstr2  9677  xrnemnf  9846  xrnepnf  9847  mnfltxr  9855  nn0pnfge0  9860  xrlttr  9864  xrltso  9865  xrlttri3  9866  nltpnft  9883  npnflt  9884  ngtmnft  9886  nmnfgt  9887  xsubge0  9950  xposdif  9951  xleaddadd  9956  fztpval  10152  fseq1p1m1  10163  fz01or  10180  qbtwnxr  10329  xqltnle  10339  fzfig  10504  uzsinds  10518  ser0f  10608  1exp  10642  0exp  10648  bcn1  10832  zfz1iso  10915  0wrd0  10943  wrdlen1  10954  sqrt0rlem  11150  prodf1f  11689  0dvds  11957  nn0o  12051  flodddiv4  12078  gcddvds  12103  bezoutlemmain  12138  lcmdvds  12220  rpdvds  12240  1nprm  12255  prmind2  12261  nnoddn2prmb  12403  pcpre1  12433  qexpz  12493  4sqlem19  12550  ennnfonelemj0  12561  ennnfonelemhf1o  12573  strslfv  12666  restsspw  12863  xpsfrnel  12930  mgmidcl  12964  mgmlrid  12965  releqgg  13293  islidlm  13978  zrhrhm  14122  psrplusgg  14173  baspartn  14229  eltg3  14236  topnex  14265  discld  14315  lmreltop  14372  cnpfval  14374  cnprcl2k  14385  idcn  14391  xmet0  14542  blfvalps  14564  blfps  14588  blf  14589  limcimolemlt  14843  recnprss  14866  lgsdir2lem2  15186  gausslemma2dlem4  15221  2lgslem2  15249  2lgslem3  15258  2lgs  15261  2sqlem7  15278  funmptd  15365  bj-om  15499  bj-nn0suc0  15512  bj-nn0suc  15526  bj-nn0sucALT  15540  bj-findis  15541  nninfall  15569  nnnninfen  15581  trilpolemcl  15597  dceqnconst  15620  dcapnconst  15621