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  1385  dedhb  2904  sbceqal  3016  ssdifeq0  3503  pwidg  3586  elpr2  3611  snidg  3618  exsnrex  3631  rabrsndc  3657  prid1g  3693  tpid1g  3701  tpid2g  3703  sssnr  3749  ssprr  3752  sstpr  3753  preqr1  3764  unimax  3839  intmin3  3867  eqbrtrdi  4037  pwnss  4154  0inp0  4161  bnd2  4168  ss1o0el1  4192  exmidsssn  4197  exmidundif  4201  exmidundifim  4202  euabex  4219  copsexg  4238  euotd  4248  elopab  4252  epelg  4284  sucidg  4410  ifelpwung  4475  regexmidlem1  4526  sucprcreg  4542  onprc  4545  dtruex  4552  omelon2  4601  elvvuni  4684  eqrelriv  4713  relopabi  4746  opabid2  4751  ididg  4773  iss  4946  funopg  5242  fn0  5327  f00  5399  f0bi  5400  f1o00  5488  fo00  5489  brprcneu  5500  relelfvdm  5539  fsn  5680  eufnfv  5738  f1eqcocnv  5782  riotaprop  5844  acexmidlemb  5857  acexmidlemab  5859  acexmidlem2  5862  oprabid  5897  elrnmpo  5978  ov6g  6002  eqop2  6169  1stconst  6212  2ndconst  6213  dftpos3  6253  dftpos4  6254  2pwuninelg  6274  frecabcl  6390  el2oss1o  6434  ecopover  6623  map0g  6678  mapsn  6680  elixpsn  6725  en0  6785  en1  6789  fiprc  6805  dom0  6828  nneneq  6847  findcard  6878  findcard2  6879  findcard2s  6880  sbthlem2  6947  sbthlemi4  6949  sbthlemi5  6950  eldju2ndl  7061  updjudhf  7068  enumct  7104  nnnninf  7114  nninfisollem0  7118  fodjuomnilemdc  7132  exmidonfinlem  7182  exmidaclem  7197  pw1ne1  7218  pw1ne3  7219  1ne0sr  7740  00sr  7743  cnm  7806  eqlei2  8026  cnstab  8576  divcanap3  8627  sup3exmid  8885  nn1suc  8909  nn0ge0  9172  xnn0xr  9215  xnn0nemnf  9221  elnn0z  9237  nn0n0n1ge2b  9303  nn0ind-raph  9341  elnn1uz2  9578  indstr2  9580  xrnemnf  9746  xrnepnf  9747  mnfltxr  9755  nn0pnfge0  9760  xrlttr  9764  xrltso  9765  xrlttri3  9766  nltpnft  9783  npnflt  9784  ngtmnft  9786  nmnfgt  9787  xsubge0  9850  xposdif  9851  xleaddadd  9856  fztpval  10051  fseq1p1m1  10062  fz01or  10079  qbtwnxr  10226  fzfig  10398  uzsinds  10410  ser0f  10483  1exp  10517  0exp  10523  bcn1  10704  zfz1iso  10787  sqrt0rlem  10978  prodf1f  11517  0dvds  11784  nn0o  11877  flodddiv4  11904  gcddvds  11929  bezoutlemmain  11964  lcmdvds  12044  rpdvds  12064  1nprm  12079  prmind2  12085  nnoddn2prmb  12227  pcpre1  12257  qexpz  12315  ennnfonelemj0  12367  ennnfonelemhf1o  12379  strslfv  12471  restsspw  12618  mgmidcl  12661  mgmlrid  12662  baspartn  13099  eltg3  13108  topnex  13137  discld  13187  lmreltop  13244  cnpfval  13246  cnprcl2k  13257  idcn  13263  xmet0  13414  blfvalps  13436  blfps  13460  blf  13461  limcimolemlt  13684  recnprss  13707  lgsdir2lem2  13981  2sqlem7  14008  funmptd  14095  bj-om  14229  bj-nn0suc0  14242  bj-nn0suc  14256  bj-nn0sucALT  14270  bj-findis  14271  nninfall  14299  trilpolemcl  14326  dceqnconst  14348  dcapnconst  14349