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  2853  dedhb  2985  sbceqal  3097  ssdifeq0  3591  pwidg  3685  elpr2  3710  snidg  3717  exsnrex  3730  rabrsndc  3758  prid1g  3794  tpid1g  3803  tpid2g  3805  sssnr  3856  ssprr  3859  sstpr  3860  preqr1  3871  unimax  3947  intmin3  3975  eqbrtrdi  4147  if0elpw  4270  pwnss  4271  0inp0  4278  bnd2  4285  ss1o0el1  4309  exmidsssn  4314  exmidundif  4318  exmidundifim  4319  euabex  4340  copsexg  4359  euotd  4370  elopab  4375  epelg  4410  sucidg  4536  ifelpwung  4601  regexmidlem1  4654  sucprcreg  4670  onprc  4673  dtruex  4680  omelon2  4729  elvvuni  4813  eqrelriv  4842  relopabi  4879  opabid2  4885  ididg  4907  iss  5083  funopg  5385  fn0  5477  f00  5558  f0bi  5559  f10d  5649  f1o00  5650  fo00  5651  brprcneu  5662  relelfvdm  5701  fvmbr  5704  fsn  5848  funop  5860  eufnfv  5916  f1eqcocnv  5963  riotaprop  6028  acexmidlemb  6041  acexmidlemab  6043  acexmidlem2  6046  oprabid  6081  elrnmpo  6166  ov6g  6191  eqop2  6371  1stconst  6416  2ndconst  6417  dftpos3  6492  dftpos4  6493  2pwuninelg  6513  frecabcl  6629  el2oss1o  6675  ecopover  6866  map0g  6921  mapsnd  6922  mapsn  6924  elixpsn  6969  en0  7034  en1  7038  fiprc  7056  en2m  7065  dom0  7090  nneneq  7110  findcard  7144  findcard2  7145  findcard2s  7146  elssdc  7161  eqsndc  7162  sbthlem2  7227  sbthlemi4  7229  sbthlemi5  7230  2omap  7268  eldju2ndl  7362  updjudhf  7369  enumct  7405  nnnninf  7416  nninfisollem0  7420  fodjuomnilemdc  7434  exmidonfinlem  7495  exmidaclem  7514  pw1ne1  7538  pw1ne3  7539  1ne0sr  8077  00sr  8080  cnm  8143  eqlei2  8364  cnstab  8915  divcanap3  8968  sup3exmid  9227  nn1suc  9252  nn0ge0  9517  xnn0xr  9564  xnn0nemnf  9570  elnn0z  9586  nn0n0n1ge2b  9653  nn0ind-raph  9691  elnn1uz2  9935  indstr2  9937  xrnemnf  10106  xrnepnf  10107  mnfltxr  10115  nn0pnfge0  10120  xrlttr  10124  xrltso  10125  xrlttri3  10126  nltpnft  10143  npnflt  10144  ngtmnft  10146  nmnfgt  10147  xsubge0  10210  xposdif  10211  xleaddadd  10216  fztpval  10413  fseq1p1m1  10424  fz01or  10441  qbtwnxr  10613  xqltnle  10623  fzfig  10788  uzsinds  10802  ser0f  10892  1exp  10926  0exp  10932  bcn1  11116  en1hash  11158  hashfibc  11200  zfz1iso  11206  hash2en  11208  0wrd0  11243  wrdlen1  11255  wrdl1exs1  11310  swrdspsleq  11352  cats1un  11406  wrdind  11407  wrd2ind  11408  sqrt0rlem  11681  fzf1o  12054  prodf1f  12222  0dvds  12490  nn0o  12586  flodddiv4  12615  bitsp1o  12632  gcddvds  12652  bezoutlemmain  12687  lcmdvds  12769  rpdvds  12789  1nprm  12804  prmind2  12810  nnoddn2prmb  12953  pcpre1  12983  qexpz  13043  4sqlem19  13100  ennnfonelemj0  13141  ennnfonelemhf1o  13153  strslfv  13246  restsspw  13451  xpsfrnel  13546  mgmidcl  13580  mgmlrid  13581  releqgg  13926  islidlm  14614  zrhrhm  14758  psrplusgg  14820  baspartn  14902  eltg3  14909  topnex  14938  discld  14988  cnpfval  15047  cnprcl2k  15058  idcn  15064  xmet0  15215  blfvalps  15237  blfps  15261  blf  15262  limcimolemlt  15516  recnprss  15539  lgsdir2lem2  15889  gausslemma2dlem4  15924  2lgslem2  15952  2lgslem3  15961  2lgs  15964  2sqlem7  15981  uhgr0e  16064  incistruhgr  16072  issubgr2  16240  subgrprop2  16242  egrsubgr  16245  0grsubgr  16246  0uhgrsubgr  16247  uhgrsubgrself  16248  clwwlkn1  16400  funmptd  16562  bj-om  16694  bj-nn0suc0  16707  bj-nn0suc  16721  bj-nn0sucALT  16735  bj-findis  16736  pw1map  16756  nninfall  16774  nnnninfen  16786  trilpolemcl  16808  dceqnconst  16832  dcapnconst  16833  gsumgfsum1  16849