Theorem mpbiri 167

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

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.18im  1346  dedhb  2822  sbceqal  2932  ssdifeq0  3411  pwidg  3490  elpr2  3515  snidg  3520  exsnrex  3532  rabrsndc  3557  prid1g  3593  tpid1g  3601  tpid2g  3603  sssnr  3646  ssprr  3649  sstpr  3650  preqr1  3661  unimax  3736  intmin3  3764  syl6eqbr  3932  pwnss  4043  0inp0  4050  bnd2  4057  exmid01  4081  exmidsssn  4085  exmidundif  4089  exmidundifim  4090  euabex  4107  copsexg  4126  euotd  4136  elopab  4140  epelg  4172  sucidg  4298  regexmidlem1  4408  sucprcreg  4424  onprc  4427  dtruex  4434  omelon2  4481  elvvuni  4563  eqrelriv  4592  relopabi  4625  opabid2  4630  ididg  4652  iss  4823  funopg  5115  fn0  5200  f00  5272  f0bi  5273  f1o00  5358  fo00  5359  brprcneu  5368  relelfvdm  5407  fsn  5546  eufnfv  5602  f1eqcocnv  5646  riotaprop  5707  acexmidlemb  5720  acexmidlemab  5722  acexmidlem2  5725  oprabid  5757  elrnmpo  5838  ov6g  5862  eqop2  6030  1stconst  6072  2ndconst  6073  dftpos3  6113  dftpos4  6114  2pwuninelg  6134  frecabcl  6250  ecopover  6481  map0g  6536  mapsn  6538  elixpsn  6583  en0  6643  en1  6647  fiprc  6663  dom0  6685  nneneq  6704  findcard  6735  findcard2  6736  findcard2s  6737  sbthlem2  6798  sbthlemi4  6800  sbthlemi5  6801  eldju2ndl  6909  updjudhf  6916  enumct  6952  fodjuomnilemdc  6966  nnnninf  6973  exmidaclem  7012  1ne0sr  7509  00sr  7512  cnm  7567  eqlei2  7781  divcanap3  8371  sup3exmid  8625  nn1suc  8649  nn0ge0  8906  xnn0xr  8949  xnn0nemnf  8955  elnn0z  8971  nn0n0n1ge2b  9034  nn0ind-raph  9072  elnn1uz2  9303  indstr2  9305  xrnemnf  9457  xrnepnf  9458  mnfltxr  9465  nn0pnfge0  9470  xrlttr  9474  xrltso  9475  xrlttri3  9476  nltpnft  9490  npnflt  9491  ngtmnft  9493  nmnfgt  9494  xsubge0  9557  xposdif  9558  xleaddadd  9563  fztpval  9756  fseq1p1m1  9767  fz01or  9784  qbtwnxr  9928  fzfig  10096  uzsinds  10108  ser0f  10181  1exp  10215  0exp  10221  bcn1  10397  zfz1iso  10477  sqrt0rlem  10667  0dvds  11361  nn0o  11452  flodddiv4  11479  gcddvds  11500  bezoutlemmain  11532  lcmdvds  11606  rpdvds  11626  1nprm  11641  prmind2  11647  ennnfonelemj0  11759  ennnfonelemhf1o  11771  strslfv  11846  restsspw  11973  baspartn  12060  eltg3  12069  topnex  12098  discld  12148  lmreltop  12205  cnpfval  12207  cnprcl2k  12217  idcn  12223  xmet0  12352  blfvalps  12374  blfps  12398  blf  12399  limcimolemlt  12589  recnprss  12611  bj-om  12827  bj-nn0suc0  12840  bj-nn0suc  12854  bj-nn0sucALT  12868  bj-findis  12869  el2oss1o  12880  nninfall  12896  trilpolemcl  12922