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  1405  ceqsexv2d  2813  dedhb  2943  sbceqal  3055  ssdifeq0  3544  pwidg  3631  elpr2  3656  snidg  3663  exsnrex  3676  rabrsndc  3702  prid1g  3738  tpid1g  3746  tpid2g  3748  sssnr  3796  ssprr  3799  sstpr  3800  preqr1  3811  unimax  3886  intmin3  3914  eqbrtrdi  4086  pwnss  4207  0inp0  4214  bnd2  4221  ss1o0el1  4245  exmidsssn  4250  exmidundif  4254  exmidundifim  4255  euabex  4273  copsexg  4292  euotd  4303  elopab  4308  epelg  4341  sucidg  4467  ifelpwung  4532  regexmidlem1  4585  sucprcreg  4601  onprc  4604  dtruex  4611  omelon2  4660  elvvuni  4743  eqrelriv  4772  relopabi  4807  opabid2  4813  ididg  4835  iss  5010  funopg  5310  fn0  5401  f00  5474  f0bi  5475  f1o00  5564  fo00  5565  brprcneu  5576  relelfvdm  5615  fsn  5759  funop  5770  eufnfv  5822  f1eqcocnv  5867  riotaprop  5930  acexmidlemb  5943  acexmidlemab  5945  acexmidlem2  5948  oprabid  5983  elrnmpo  6066  ov6g  6091  eqop2  6271  1stconst  6314  2ndconst  6315  dftpos3  6355  dftpos4  6356  2pwuninelg  6376  frecabcl  6492  el2oss1o  6536  ecopover  6727  map0g  6782  mapsn  6784  elixpsn  6829  en0  6894  en1  6898  fiprc  6914  dom0  6942  nneneq  6961  findcard  6992  findcard2  6993  findcard2s  6994  sbthlem2  7067  sbthlemi4  7069  sbthlemi5  7070  eldju2ndl  7181  updjudhf  7188  enumct  7224  nnnninf  7235  nninfisollem0  7239  fodjuomnilemdc  7253  exmidonfinlem  7308  exmidaclem  7327  pw1ne1  7348  pw1ne3  7349  1ne0sr  7886  00sr  7889  cnm  7952  eqlei2  8174  cnstab  8725  divcanap3  8778  sup3exmid  9037  nn1suc  9062  nn0ge0  9327  xnn0xr  9370  xnn0nemnf  9376  elnn0z  9392  nn0n0n1ge2b  9459  nn0ind-raph  9497  elnn1uz2  9735  indstr2  9737  xrnemnf  9906  xrnepnf  9907  mnfltxr  9915  nn0pnfge0  9920  xrlttr  9924  xrltso  9925  xrlttri3  9926  nltpnft  9943  npnflt  9944  ngtmnft  9946  nmnfgt  9947  xsubge0  10010  xposdif  10011  xleaddadd  10016  fztpval  10212  fseq1p1m1  10223  fz01or  10240  qbtwnxr  10407  xqltnle  10417  fzfig  10582  uzsinds  10596  ser0f  10686  1exp  10720  0exp  10726  bcn1  10910  zfz1iso  10993  hash2en  10995  0wrd0  11027  wrdlen1  11038  wrdl1exs1  11091  swrdspsleq  11128  sqrt0rlem  11358  prodf1f  11898  0dvds  12166  nn0o  12262  flodddiv4  12291  bitsp1o  12308  gcddvds  12328  bezoutlemmain  12363  lcmdvds  12445  rpdvds  12465  1nprm  12480  prmind2  12486  nnoddn2prmb  12629  pcpre1  12659  qexpz  12719  4sqlem19  12776  ennnfonelemj0  12816  ennnfonelemhf1o  12828  strslfv  12921  restsspw  13125  xpsfrnel  13220  mgmidcl  13254  mgmlrid  13255  releqgg  13600  islidlm  14285  zrhrhm  14429  psrplusgg  14484  baspartn  14566  eltg3  14573  topnex  14602  discld  14652  lmreltop  14709  cnpfval  14711  cnprcl2k  14722  idcn  14728  xmet0  14879  blfvalps  14901  blfps  14925  blf  14926  limcimolemlt  15180  recnprss  15203  lgsdir2lem2  15550  gausslemma2dlem4  15585  2lgslem2  15613  2lgslem3  15622  2lgs  15625  2sqlem7  15642  uhgr0e  15722  incistruhgr  15730  funmptd  15813  bj-om  15947  bj-nn0suc0  15960  bj-nn0suc  15974  bj-nn0sucALT  15988  bj-findis  15989  2omap  16006  nninfall  16020  nnnninfen  16032  trilpolemcl  16050  dceqnconst  16073  dcapnconst  16074