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-mp 5  ax-1 6  ax-2 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  1375  dedhb  2895  sbceqal  3006  ssdifeq0  3491  pwidg  3573  elpr2  3598  snidg  3605  exsnrex  3618  rabrsndc  3644  prid1g  3680  tpid1g  3688  tpid2g  3690  sssnr  3733  ssprr  3736  sstpr  3737  preqr1  3748  unimax  3823  intmin3  3851  eqbrtrdi  4021  pwnss  4138  0inp0  4145  bnd2  4152  ss1o0el1  4176  exmidsssn  4181  exmidundif  4185  exmidundifim  4186  euabex  4203  copsexg  4222  euotd  4232  elopab  4236  epelg  4268  sucidg  4394  ifelpwung  4459  regexmidlem1  4510  sucprcreg  4526  onprc  4529  dtruex  4536  omelon2  4585  elvvuni  4668  eqrelriv  4697  relopabi  4730  opabid2  4735  ididg  4757  iss  4930  funopg  5222  fn0  5307  f00  5379  f0bi  5380  f1o00  5467  fo00  5468  brprcneu  5479  relelfvdm  5518  fsn  5657  eufnfv  5715  f1eqcocnv  5759  riotaprop  5821  acexmidlemb  5834  acexmidlemab  5836  acexmidlem2  5839  oprabid  5874  elrnmpo  5955  ov6g  5979  eqop2  6146  1stconst  6189  2ndconst  6190  dftpos3  6230  dftpos4  6231  2pwuninelg  6251  frecabcl  6367  el2oss1o  6411  ecopover  6599  map0g  6654  mapsn  6656  elixpsn  6701  en0  6761  en1  6765  fiprc  6781  dom0  6804  nneneq  6823  findcard  6854  findcard2  6855  findcard2s  6856  sbthlem2  6923  sbthlemi4  6925  sbthlemi5  6926  eldju2ndl  7037  updjudhf  7044  enumct  7080  nnnninf  7090  nninfisollem0  7094  fodjuomnilemdc  7108  exmidonfinlem  7149  exmidaclem  7164  pw1ne1  7185  pw1ne3  7186  1ne0sr  7707  00sr  7710  cnm  7773  eqlei2  7993  cnstab  8543  divcanap3  8594  sup3exmid  8852  nn1suc  8876  nn0ge0  9139  xnn0xr  9182  xnn0nemnf  9188  elnn0z  9204  nn0n0n1ge2b  9270  nn0ind-raph  9308  elnn1uz2  9545  indstr2  9547  xrnemnf  9713  xrnepnf  9714  mnfltxr  9722  nn0pnfge0  9727  xrlttr  9731  xrltso  9732  xrlttri3  9733  nltpnft  9750  npnflt  9751  ngtmnft  9753  nmnfgt  9754  xsubge0  9817  xposdif  9818  xleaddadd  9823  fztpval  10018  fseq1p1m1  10029  fz01or  10046  qbtwnxr  10193  fzfig  10365  uzsinds  10377  ser0f  10450  1exp  10484  0exp  10490  bcn1  10671  zfz1iso  10754  sqrt0rlem  10945  prodf1f  11484  0dvds  11751  nn0o  11844  flodddiv4  11871  gcddvds  11896  bezoutlemmain  11931  lcmdvds  12011  rpdvds  12031  1nprm  12046  prmind2  12052  nnoddn2prmb  12194  pcpre1  12224  qexpz  12282  ennnfonelemj0  12334  ennnfonelemhf1o  12346  strslfv  12438  restsspw  12566  mgmidcl  12609  mgmlrid  12610  baspartn  12698  eltg3  12707  topnex  12736  discld  12786  lmreltop  12843  cnpfval  12845  cnprcl2k  12856  idcn  12862  xmet0  13013  blfvalps  13035  blfps  13059  blf  13060  limcimolemlt  13283  recnprss  13306  lgsdir2lem2  13580  2sqlem7  13607  funmptd  13695  bj-om  13829  bj-nn0suc0  13842  bj-nn0suc  13856  bj-nn0sucALT  13870  bj-findis  13871  nninfall  13899  trilpolemcl  13926  dceqnconst  13948  dcapnconst  13949