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  4170  if0elpw  4297  pwnss  4298  0inp0  4305  bnd2  4312  ss1o0el1  4336  exmidsssn  4341  exmidundif  4345  exmidundifim  4346  euabex  4367  copsexg  4386  euotd  4397  elopab  4402  epelg  4437  sucidg  4563  ifelpwung  4629  regexmidlem1  4682  sucprcreg  4698  onprc  4701  dtruex  4708  omelon2  4757  elvvuni  4841  eqrelriv  4870  relopabi  4907  opabid2  4913  ididg  4935  iss  5112  funopg  5414  fn0  5506  f00  5587  f0bi  5588  f10d  5678  f1o00  5679  fo00  5680  brprcneu  5691  relelfvdm  5730  fvmbr  5734  fsn  5883  funop  5895  eufnfv  5952  f1eqcocnv  6000  riotaprop  6067  acexmidlemb  6080  acexmidlemab  6082  acexmidlem2  6085  oprabid  6120  elrnmpo  6205  ov6g  6230  eqop2  6416  1stconst  6461  2ndconst  6462  dftpos3  6538  dftpos4  6539  2pwuninelg  6559  frecabcl  6675  el2oss1o  6721  ecopover  6912  map0g  6974  mapsnd  6976  mapsn  6978  elixpsn  7023  en0  7088  en1  7092  fiprc  7110  en2m  7119  dom0  7144  nneneq  7164  findcard  7198  findcard2  7199  findcard2s  7200  elssdc  7215  eqsndc  7216  sbthlem2  7282  sbthlemi4  7284  sbthlemi5  7285  2omap  7324  eldju2ndl  7418  updjudhf  7425  enumct  7461  nnnninf  7472  nninfisollem0  7476  fodjuomnilemdc  7490  exmidonfinlem  7551  exmidaclem  7570  pw1ne1  7594  pw1ne3  7595  1ne0sr  8139  00sr  8142  cnm  8205  eqlei2  8427  cnstab  8981  divcanap3  9036  sup3exmid  9295  nn1suc  9332  nn0ge0  9599  xnn0xr  9644  xnn0nemnf  9650  elnn0z  9666  nn0n0n1ge2b  9734  nn0ind-raph  9773  elnn1uz2  10022  indstr2  10024  xrnemnf  10195  xrnepnf  10196  mnfltxr  10204  nn0pnfge0  10209  xrlttr  10213  xrltso  10214  xrlttri3  10215  nltpnft  10232  npnflt  10233  ngtmnft  10235  nmnfgt  10236  xsubge0  10299  xposdif  10300  xleaddadd  10305  fztpval  10506  fseq1p1m1  10517  fz01or  10534  qbtwnxr  10708  xqltnle  10718  fzfig  10887  uzsinds  10901  ser0f  10991  1exp  11025  0exp  11031  bcn1  11217  en1hash  11260  hashfibc  11304  hashf1  11308  zfz1iso  11314  hash2en  11316  0wrd0  11351  wrdlen1  11363  wrdl1exs1  11418  swrdspsleq  11460  cats1un  11514  wrdind  11515  wrd2ind  11516  sq01  11681  sqrt0rlem  11790  fzf1o  12166  prodf1f  12334  0dvds  12602  nn0o  12698  flodddiv4  12727  bitsp1o  12744  gcddvds  12764  bezoutlemmain  12799  lcmdvds  12881  rpdvds  12901  1nprm  12916  prmind2  12922  nnoddn2prmb  13069  pcpre1  13099  qexpz  13159  4sqlem19  13216  prmlem0  13248  ballotfilem8  13337  ennnfonelemj0  13349  ennnfonelemhf1o  13361  strslfv  13454  restsspw  13661  xpsfrnel  13723  mgmidcl  13756  mgmlrid  13757  releqgg  14081  cntzrcl  14158  gzsumgsum1  14242  gsumcom2fi  14274  islidlm  14924  zrhrhm  15066  psrplusgg  15191  psrridmfi  15209  baspartn  15293  eltg3  15300  topnex  15329  discld  15379  cnpfval  15438  cnprcl2k  15449  idcn  15455  xmet0  15606  blfvalps  15628  blfps  15652  blf  15653  limcimolemlt  15907  recnprss  15930  bposlem6  16333  lgsdir2lem2  16370  gausslemma2dlem4  16405  2lgslem2  16433  2lgslem3  16442  2lgs  16445  2sqlem7  16462  uhgr0e  16545  incistruhgr  16553  issubgr2  16721  subgrprop2  16723  egrsubgr  16726  0grsubgr  16727  0uhgrsubgr  16728  uhgrsubgrself  16729  clwwlkn1  16881  funmptd  17053  bj-om  17185  bj-nn0suc0  17198  bj-nn0suc  17212  bj-nn0sucALT  17226  bj-findis  17227  pw1map  17247  wexmiddiffilem  17265  wexmiddifxylem  17267  nninfall  17275  nnnninfen  17287  trilpolemcl  17310  dceqnconst  17334  dcapnconst  17335