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  6537  dftpos4  6538  2pwuninelg  6558  frecabcl  6674  el2oss1o  6720  ecopover  6911  map0g  6973  mapsnd  6975  mapsn  6977  elixpsn  7022  en0  7087  en1  7091  fiprc  7109  en2m  7118  dom0  7143  nneneq  7163  findcard  7197  findcard2  7198  findcard2s  7199  elssdc  7214  eqsndc  7215  sbthlem2  7281  sbthlemi4  7283  sbthlemi5  7284  2omap  7325  eldju2ndl  7419  updjudhf  7426  enumct  7462  nnnninf  7473  nninfisollem0  7477  fodjuomnilemdc  7491  exmidonfinlem  7552  exmidaclem  7571  pw1ne1  7595  pw1ne3  7596  1ne0sr  8140  00sr  8143  cnm  8206  eqlei2  8428  cnstab  8982  divcanap3  9037  sup3exmid  9296  nn1suc  9333  nn0ge0  9600  xnn0xr  9647  xnn0nemnf  9653  elnn0z  9669  nn0n0n1ge2b  9737  nn0ind-raph  9775  elnn1uz2  10024  indstr2  10026  xrnemnf  10197  xrnepnf  10198  mnfltxr  10206  nn0pnfge0  10211  xrlttr  10215  xrltso  10216  xrlttri3  10217  nltpnft  10234  npnflt  10235  ngtmnft  10237  nmnfgt  10238  xsubge0  10301  xposdif  10302  xleaddadd  10307  fztpval  10508  fseq1p1m1  10519  fz01or  10536  qbtwnxr  10710  xqltnle  10720  fzfig  10889  uzsinds  10903  ser0f  10993  1exp  11027  0exp  11033  bcn1  11219  en1hash  11262  hashfibc  11306  hashf1  11310  zfz1iso  11316  hash2en  11318  0wrd0  11353  wrdlen1  11365  wrdl1exs1  11420  swrdspsleq  11462  cats1un  11516  wrdind  11517  wrd2ind  11518  sq01  11683  sqrt0rlem  11792  fzf1o  12168  prodf1f  12336  0dvds  12604  nn0o  12700  flodddiv4  12729  bitsp1o  12746  gcddvds  12766  bezoutlemmain  12801  lcmdvds  12883  rpdvds  12903  1nprm  12918  prmind2  12924  nnoddn2prmb  13071  pcpre1  13101  qexpz  13161  4sqlem19  13218  prmlem0  13250  ballotfilem8  13339  ennnfonelemj0  13351  ennnfonelemhf1o  13363  strslfv  13456  restsspw  13663  xpsfrnel  13725  mgmidcl  13758  mgmlrid  13759  releqgg  14083  cntzrcl  14160  gzsumgsum1  14244  gsumcom2fi  14276  islidlm  14926  zrhrhm  15068  psrplusgg  15187  psrridmfi  15205  baspartn  15288  eltg3  15295  topnex  15324  discld  15374  cnpfval  15433  cnprcl2k  15444  idcn  15450  xmet0  15601  blfvalps  15623  blfps  15647  blf  15648  limcimolemlt  15902  recnprss  15925  bposlem6  16328  lgsdir2lem2  16365  gausslemma2dlem4  16400  2lgslem2  16428  2lgslem3  16437  2lgs  16440  2sqlem7  16457  uhgr0e  16540  incistruhgr  16548  issubgr2  16716  subgrprop2  16718  egrsubgr  16721  0grsubgr  16722  0uhgrsubgr  16723  uhgrsubgrself  16724  clwwlkn1  16876  funmptd  17048  bj-om  17180  bj-nn0suc0  17193  bj-nn0suc  17207  bj-nn0sucALT  17221  bj-findis  17222  pw1map  17242  wexmiddiffilem  17260  wexmiddifxylem  17262  nninfall  17270  nnnninfen  17282  trilpolemcl  17305  dceqnconst  17329  dcapnconst  17330