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  2906  sbceqal  3018  ssdifeq0  3505  pwidg  3589  elpr2  3614  snidg  3621  exsnrex  3634  rabrsndc  3660  prid1g  3696  tpid1g  3704  tpid2g  3706  sssnr  3753  ssprr  3756  sstpr  3757  preqr1  3768  unimax  3843  intmin3  3871  eqbrtrdi  4042  pwnss  4159  0inp0  4166  bnd2  4173  ss1o0el1  4197  exmidsssn  4202  exmidundif  4206  exmidundifim  4207  euabex  4225  copsexg  4244  euotd  4254  elopab  4258  epelg  4290  sucidg  4416  ifelpwung  4481  regexmidlem1  4532  sucprcreg  4548  onprc  4551  dtruex  4558  omelon2  4607  elvvuni  4690  eqrelriv  4719  relopabi  4752  opabid2  4758  ididg  4780  iss  4953  funopg  5250  fn0  5335  f00  5407  f0bi  5408  f1o00  5496  fo00  5497  brprcneu  5508  relelfvdm  5547  fsn  5688  eufnfv  5747  f1eqcocnv  5791  riotaprop  5853  acexmidlemb  5866  acexmidlemab  5868  acexmidlem2  5871  oprabid  5906  elrnmpo  5987  ov6g  6011  eqop2  6178  1stconst  6221  2ndconst  6222  dftpos3  6262  dftpos4  6263  2pwuninelg  6283  frecabcl  6399  el2oss1o  6443  ecopover  6632  map0g  6687  mapsn  6689  elixpsn  6734  en0  6794  en1  6798  fiprc  6814  dom0  6837  nneneq  6856  findcard  6887  findcard2  6888  findcard2s  6889  sbthlem2  6956  sbthlemi4  6958  sbthlemi5  6959  eldju2ndl  7070  updjudhf  7077  enumct  7113  nnnninf  7123  nninfisollem0  7127  fodjuomnilemdc  7141  exmidonfinlem  7191  exmidaclem  7206  pw1ne1  7227  pw1ne3  7228  1ne0sr  7764  00sr  7767  cnm  7830  eqlei2  8051  cnstab  8601  divcanap3  8654  sup3exmid  8913  nn1suc  8937  nn0ge0  9200  xnn0xr  9243  xnn0nemnf  9249  elnn0z  9265  nn0n0n1ge2b  9331  nn0ind-raph  9369  elnn1uz2  9606  indstr2  9608  xrnemnf  9776  xrnepnf  9777  mnfltxr  9785  nn0pnfge0  9790  xrlttr  9794  xrltso  9795  xrlttri3  9796  nltpnft  9813  npnflt  9814  ngtmnft  9816  nmnfgt  9817  xsubge0  9880  xposdif  9881  xleaddadd  9886  fztpval  10082  fseq1p1m1  10093  fz01or  10110  qbtwnxr  10257  fzfig  10429  uzsinds  10441  ser0f  10514  1exp  10548  0exp  10554  bcn1  10737  zfz1iso  10820  sqrt0rlem  11011  prodf1f  11550  0dvds  11817  nn0o  11911  flodddiv4  11938  gcddvds  11963  bezoutlemmain  11998  lcmdvds  12078  rpdvds  12098  1nprm  12113  prmind2  12119  nnoddn2prmb  12261  pcpre1  12291  qexpz  12349  ennnfonelemj0  12401  ennnfonelemhf1o  12413  strslfv  12506  restsspw  12697  xpsfrnel  12762  mgmidcl  12796  mgmlrid  12797  releqgg  13078  baspartn  13520  eltg3  13527  topnex  13556  discld  13606  lmreltop  13663  cnpfval  13665  cnprcl2k  13676  idcn  13682  xmet0  13833  blfvalps  13855  blfps  13879  blf  13880  limcimolemlt  14103  recnprss  14126  lgsdir2lem2  14400  2sqlem7  14438  funmptd  14525  bj-om  14659  bj-nn0suc0  14672  bj-nn0suc  14686  bj-nn0sucALT  14700  bj-findis  14701  nninfall  14728  trilpolemcl  14755  dceqnconst  14777  dcapnconst  14778