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  7318  eldju2ndl  7412  updjudhf  7419  enumct  7455  nnnninf  7466  nninfisollem0  7470  fodjuomnilemdc  7484  exmidonfinlem  7545  exmidaclem  7564  pw1ne1  7588  pw1ne3  7589  1ne0sr  8133  00sr  8136  cnm  8199  eqlei2  8420  cnstab  8974  divcanap3  9029  sup3exmid  9288  nn1suc  9324  nn0ge0  9590  xnn0xr  9637  xnn0nemnf  9643  elnn0z  9659  nn0n0n1ge2b  9727  nn0ind-raph  9765  elnn1uz2  10009  indstr2  10011  xrnemnf  10181  xrnepnf  10182  mnfltxr  10190  nn0pnfge0  10195  xrlttr  10199  xrltso  10200  xrlttri3  10201  nltpnft  10218  npnflt  10219  ngtmnft  10221  nmnfgt  10222  xsubge0  10285  xposdif  10286  xleaddadd  10291  fztpval  10492  fseq1p1m1  10503  fz01or  10520  qbtwnxr  10694  xqltnle  10704  fzfig  10869  uzsinds  10883  ser0f  10973  1exp  11007  0exp  11013  bcn1  11198  en1hash  11241  hashfibc  11285  hashf1  11289  zfz1iso  11295  hash2en  11297  0wrd0  11332  wrdlen1  11344  wrdl1exs1  11399  swrdspsleq  11441  cats1un  11495  wrdind  11496  wrd2ind  11497  sq01  11662  sqrt0rlem  11771  fzf1o  12144  prodf1f  12312  0dvds  12580  nn0o  12676  flodddiv4  12705  bitsp1o  12722  gcddvds  12742  bezoutlemmain  12777  lcmdvds  12859  rpdvds  12879  1nprm  12894  prmind2  12900  nnoddn2prmb  13043  pcpre1  13073  qexpz  13133  4sqlem19  13190  ballotfilem8  13282  ennnfonelemj0  13294  ennnfonelemhf1o  13306  strslfv  13399  restsspw  13605  xpsfrnel  13667  mgmidcl  13700  mgmlrid  13701  releqgg  14025  gzsumgsum1  14155  islidlm  14818  zrhrhm  14960  psrplusgg  15071  baspartn  15153  eltg3  15160  topnex  15189  discld  15239  cnpfval  15298  cnprcl2k  15309  idcn  15315  xmet0  15466  blfvalps  15488  blfps  15512  blf  15513  limcimolemlt  15767  recnprss  15790  lgsdir2lem2  16160  gausslemma2dlem4  16195  2lgslem2  16223  2lgslem3  16232  2lgs  16235  2sqlem7  16252  uhgr0e  16335  incistruhgr  16343  issubgr2  16511  subgrprop2  16513  egrsubgr  16516  0grsubgr  16517  0uhgrsubgr  16518  uhgrsubgrself  16519  clwwlkn1  16671  funmptd  16843  bj-om  16975  bj-nn0suc0  16988  bj-nn0suc  17002  bj-nn0sucALT  17016  bj-findis  17017  pw1map  17037  wexmiddiffilem  17055  wexmiddifxylem  17057  nninfall  17064  nnnninfen  17076  trilpolemcl  17098  dceqnconst  17122  dcapnconst  17123