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  8421  cnstab  8975  divcanap3  9030  sup3exmid  9289  nn1suc  9325  nn0ge0  9592  xnn0xr  9639  xnn0nemnf  9645  elnn0z  9661  nn0n0n1ge2b  9729  nn0ind-raph  9767  elnn1uz2  10016  indstr2  10018  xrnemnf  10189  xrnepnf  10190  mnfltxr  10198  nn0pnfge0  10203  xrlttr  10207  xrltso  10208  xrlttri3  10209  nltpnft  10226  npnflt  10227  ngtmnft  10229  nmnfgt  10230  xsubge0  10293  xposdif  10294  xleaddadd  10299  fztpval  10500  fseq1p1m1  10511  fz01or  10528  qbtwnxr  10702  xqltnle  10712  fzfig  10880  uzsinds  10894  ser0f  10984  1exp  11018  0exp  11024  bcn1  11210  en1hash  11253  hashfibc  11297  hashf1  11301  zfz1iso  11307  hash2en  11309  0wrd0  11344  wrdlen1  11356  wrdl1exs1  11411  swrdspsleq  11453  cats1un  11507  wrdind  11508  wrd2ind  11509  sq01  11674  sqrt0rlem  11783  fzf1o  12158  prodf1f  12326  0dvds  12594  nn0o  12690  flodddiv4  12719  bitsp1o  12736  gcddvds  12756  bezoutlemmain  12791  lcmdvds  12873  rpdvds  12893  1nprm  12908  prmind2  12914  nnoddn2prmb  13061  pcpre1  13091  qexpz  13151  4sqlem19  13208  prmlem0  13240  ballotfilem8  13329  ennnfonelemj0  13341  ennnfonelemhf1o  13353  strslfv  13446  restsspw  13652  xpsfrnel  13714  mgmidcl  13747  mgmlrid  13748  releqgg  14072  gzsumgsum1  14202  islidlm  14865  zrhrhm  15007  psrplusgg  15118  baspartn  15200  eltg3  15207  topnex  15236  discld  15286  cnpfval  15345  cnprcl2k  15356  idcn  15362  xmet0  15513  blfvalps  15535  blfps  15559  blf  15560  limcimolemlt  15814  recnprss  15837  lgsdir2lem2  16267  gausslemma2dlem4  16302  2lgslem2  16330  2lgslem3  16339  2lgs  16342  2sqlem7  16359  uhgr0e  16442  incistruhgr  16450  issubgr2  16618  subgrprop2  16620  egrsubgr  16623  0grsubgr  16624  0uhgrsubgr  16625  uhgrsubgrself  16626  clwwlkn1  16778  funmptd  16950  bj-om  17082  bj-nn0suc0  17095  bj-nn0suc  17109  bj-nn0sucALT  17123  bj-findis  17124  pw1map  17144  wexmiddiffilem  17162  wexmiddifxylem  17164  nninfall  17171  nnnninfen  17183  trilpolemcl  17205  dceqnconst  17229  dcapnconst  17230