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  1396  dedhb  2921  sbceqal  3033  ssdifeq0  3520  pwidg  3604  elpr2  3629  snidg  3636  exsnrex  3649  rabrsndc  3675  prid1g  3711  tpid1g  3719  tpid2g  3721  sssnr  3768  ssprr  3771  sstpr  3772  preqr1  3783  unimax  3858  intmin3  3886  eqbrtrdi  4057  pwnss  4177  0inp0  4184  bnd2  4191  ss1o0el1  4215  exmidsssn  4220  exmidundif  4224  exmidundifim  4225  euabex  4243  copsexg  4262  euotd  4272  elopab  4276  epelg  4308  sucidg  4434  ifelpwung  4499  regexmidlem1  4550  sucprcreg  4566  onprc  4569  dtruex  4576  omelon2  4625  elvvuni  4708  eqrelriv  4737  relopabi  4770  opabid2  4776  ididg  4798  iss  4971  funopg  5269  fn0  5354  f00  5426  f0bi  5427  f1o00  5515  fo00  5516  brprcneu  5527  relelfvdm  5566  fsn  5708  eufnfv  5767  f1eqcocnv  5812  riotaprop  5874  acexmidlemb  5887  acexmidlemab  5889  acexmidlem2  5892  oprabid  5927  elrnmpo  6009  ov6g  6033  eqop2  6202  1stconst  6245  2ndconst  6246  dftpos3  6286  dftpos4  6287  2pwuninelg  6307  frecabcl  6423  el2oss1o  6467  ecopover  6658  map0g  6713  mapsn  6715  elixpsn  6760  en0  6820  en1  6824  fiprc  6840  dom0  6865  nneneq  6884  findcard  6915  findcard2  6916  findcard2s  6917  sbthlem2  6986  sbthlemi4  6988  sbthlemi5  6989  eldju2ndl  7100  updjudhf  7107  enumct  7143  nnnninf  7153  nninfisollem0  7157  fodjuomnilemdc  7171  exmidonfinlem  7221  exmidaclem  7236  pw1ne1  7257  pw1ne3  7258  1ne0sr  7794  00sr  7797  cnm  7860  eqlei2  8081  cnstab  8631  divcanap3  8684  sup3exmid  8943  nn1suc  8967  nn0ge0  9230  xnn0xr  9273  xnn0nemnf  9279  elnn0z  9295  nn0n0n1ge2b  9361  nn0ind-raph  9399  elnn1uz2  9636  indstr2  9638  xrnemnf  9806  xrnepnf  9807  mnfltxr  9815  nn0pnfge0  9820  xrlttr  9824  xrltso  9825  xrlttri3  9826  nltpnft  9843  npnflt  9844  ngtmnft  9846  nmnfgt  9847  xsubge0  9910  xposdif  9911  xleaddadd  9916  fztpval  10112  fseq1p1m1  10123  fz01or  10140  qbtwnxr  10287  xqltnle  10297  fzfig  10460  uzsinds  10472  ser0f  10545  1exp  10579  0exp  10585  bcn1  10769  zfz1iso  10852  sqrt0rlem  11043  prodf1f  11582  0dvds  11849  nn0o  11943  flodddiv4  11970  gcddvds  11995  bezoutlemmain  12030  lcmdvds  12110  rpdvds  12130  1nprm  12145  prmind2  12151  nnoddn2prmb  12293  pcpre1  12323  qexpz  12383  4sqlem19  12440  ennnfonelemj0  12451  ennnfonelemhf1o  12463  strslfv  12556  restsspw  12751  xpsfrnel  12817  mgmidcl  12851  mgmlrid  12852  releqgg  13156  islidlm  13792  zrhrhm  13917  baspartn  14002  eltg3  14009  topnex  14038  discld  14088  lmreltop  14145  cnpfval  14147  cnprcl2k  14158  idcn  14164  xmet0  14315  blfvalps  14337  blfps  14361  blf  14362  limcimolemlt  14585  recnprss  14608  lgsdir2lem2  14883  2sqlem7  14921  funmptd  15008  bj-om  15142  bj-nn0suc0  15155  bj-nn0suc  15169  bj-nn0sucALT  15183  bj-findis  15184  nninfall  15212  trilpolemcl  15239  dceqnconst  15262  dcapnconst  15263