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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.18im  1434  ceqsexv2d  2862  dedhb  2995  sbceqal  3107  ssdifeq0  3610  pwidg  3706  elpr2  3731  snidg  3738  exsnrex  3751  rabrsndc  3779  prid1g  3815  tpid1g  3825  tpid2g  3827  sssnr  3878  ssprr  3881  sstpr  3882  preqr1  3893  unimax  3969  intmin3  3997  eqbrtrdi  4169  if0elpw  4295  pwnss  4296  0inp0  4303  bnd2  4310  ss1o0el1  4334  exmidsssn  4339  exmidundif  4343  exmidundifim  4344  euabex  4365  copsexg  4384  euotd  4395  elopab  4400  epelg  4435  sucidg  4561  ifelpwung  4627  regexmidlem1  4680  sucprcreg  4696  onprc  4699  dtruex  4706  omelon2  4755  elvvuni  4839  eqrelriv  4868  relopabi  4905  opabid2  4911  ididg  4933  iss  5109  funopg  5411  fn0  5503  f00  5584  f0bi  5585  f10d  5675  f1o00  5676  fo00  5677  brprcneu  5688  relelfvdm  5727  fvmbr  5731  fsn  5880  funop  5892  eufnfv  5949  f1eqcocnv  5997  riotaprop  6064  acexmidlemb  6077  acexmidlemab  6079  acexmidlem2  6082  oprabid  6117  elrnmpo  6202  ov6g  6227  eqop2  6412  1stconst  6457  2ndconst  6458  dftpos3  6533  dftpos4  6534  2pwuninelg  6554  frecabcl  6670  el2oss1o  6716  ecopover  6907  map0g  6969  mapsnd  6970  mapsn  6972  elixpsn  7017  en0  7082  en1  7086  fiprc  7104  en2m  7113  dom0  7138  nneneq  7158  findcard  7192  findcard2  7193  findcard2s  7194  elssdc  7209  eqsndc  7210  sbthlem2  7275  sbthlemi4  7277  sbthlemi5  7278  2omap  7319  eldju2ndl  7413  updjudhf  7420  enumct  7456  nnnninf  7467  nninfisollem0  7471  fodjuomnilemdc  7485  exmidonfinlem  7546  exmidaclem  7565  pw1ne1  7589  pw1ne3  7590  1ne0sr  8134  00sr  8137  cnm  8200  eqlei2  8422  cnstab  8976  divcanap3  9031  sup3exmid  9290  nn1suc  9326  nn0ge0  9593  xnn0xr  9640  xnn0nemnf  9646  elnn0z  9662  nn0n0n1ge2b  9730  nn0ind-raph  9768  elnn1uz2  10017  indstr2  10019  xrnemnf  10190  xrnepnf  10191  mnfltxr  10199  nn0pnfge0  10204  xrlttr  10208  xrltso  10209  xrlttri3  10210  nltpnft  10227  npnflt  10228  ngtmnft  10230  nmnfgt  10231  xsubge0  10294  xposdif  10295  xleaddadd  10300  fztpval  10501  fseq1p1m1  10512  fz01or  10529  qbtwnxr  10703  xqltnle  10713  fzfig  10882  uzsinds  10896  ser0f  10986  1exp  11020  0exp  11026  bcn1  11212  en1hash  11255  hashfibc  11299  hashf1  11303  zfz1iso  11309  hash2en  11311  0wrd0  11346  wrdlen1  11358  wrdl1exs1  11413  swrdspsleq  11455  cats1un  11509  wrdind  11510  wrd2ind  11511  sq01  11676  sqrt0rlem  11785  fzf1o  12161  prodf1f  12329  0dvds  12597  nn0o  12693  flodddiv4  12722  bitsp1o  12739  gcddvds  12759  bezoutlemmain  12794  lcmdvds  12876  rpdvds  12896  1nprm  12911  prmind2  12917  nnoddn2prmb  13064  pcpre1  13094  qexpz  13154  4sqlem19  13211  prmlem0  13243  ballotfilem8  13332  ennnfonelemj0  13344  ennnfonelemhf1o  13356  strslfv  13449  restsspw  13656  xpsfrnel  13718  mgmidcl  13751  mgmlrid  13752  releqgg  14076  cntzrcl  14153  gzsumgsum1  14237  islidlm  14900  zrhrhm  15042  psrplusgg  15154  baspartn  15242  eltg3  15249  topnex  15278  discld  15328  cnpfval  15387  cnprcl2k  15398  idcn  15404  xmet0  15555  blfvalps  15577  blfps  15601  blf  15602  limcimolemlt  15856  recnprss  15879  bposlem6  16282  lgsdir2lem2  16319  gausslemma2dlem4  16354  2lgslem2  16382  2lgslem3  16391  2lgs  16394  2sqlem7  16411  uhgr0e  16494  incistruhgr  16502  issubgr2  16670  subgrprop2  16672  egrsubgr  16675  0grsubgr  16676  0uhgrsubgr  16677  uhgrsubgrself  16678  clwwlkn1  16830  funmptd  17002  bj-om  17134  bj-nn0suc0  17147  bj-nn0suc  17161  bj-nn0sucALT  17175  bj-findis  17176  pw1map  17196  wexmiddiffilem  17214  wexmiddifxylem  17216  nninfall  17223  nnnninfen  17235  trilpolemcl  17258  dceqnconst  17282  dcapnconst  17283