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  1429  ceqsexv2d  2842  dedhb  2974  sbceqal  3086  ssdifeq0  3576  pwidg  3667  elpr2  3692  snidg  3699  exsnrex  3712  rabrsndc  3740  prid1g  3776  tpid1g  3785  tpid2g  3787  sssnr  3837  ssprr  3840  sstpr  3841  preqr1  3852  unimax  3928  intmin3  3956  eqbrtrdi  4128  if0elpw  4250  pwnss  4251  0inp0  4258  bnd2  4265  ss1o0el1  4289  exmidsssn  4294  exmidundif  4298  exmidundifim  4299  euabex  4319  copsexg  4338  euotd  4349  elopab  4354  epelg  4389  sucidg  4515  ifelpwung  4580  regexmidlem1  4633  sucprcreg  4649  onprc  4652  dtruex  4659  omelon2  4708  elvvuni  4792  eqrelriv  4821  relopabi  4857  opabid2  4863  ididg  4885  iss  5061  funopg  5362  fn0  5454  f00  5531  f0bi  5532  f10d  5622  f1o00  5623  fo00  5624  brprcneu  5635  relelfvdm  5674  fvmbr  5677  fsn  5822  funop  5834  eufnfv  5890  f1eqcocnv  5937  riotaprop  6002  acexmidlemb  6015  acexmidlemab  6017  acexmidlem2  6020  oprabid  6055  elrnmpo  6140  ov6g  6165  eqop2  6346  1stconst  6391  2ndconst  6392  dftpos3  6433  dftpos4  6434  2pwuninelg  6454  frecabcl  6570  el2oss1o  6616  ecopover  6807  map0g  6862  mapsn  6864  elixpsn  6909  en0  6974  en1  6978  fiprc  6995  en2m  7004  dom0  7029  nneneq  7048  findcard  7082  findcard2  7083  findcard2s  7084  elssdc  7099  eqsndc  7100  sbthlem2  7162  sbthlemi4  7164  sbthlemi5  7165  eldju2ndl  7276  updjudhf  7283  enumct  7319  nnnninf  7330  nninfisollem0  7334  fodjuomnilemdc  7348  exmidonfinlem  7409  exmidaclem  7428  pw1ne1  7452  pw1ne3  7453  1ne0sr  7991  00sr  7994  cnm  8057  eqlei2  8279  cnstab  8830  divcanap3  8883  sup3exmid  9142  nn1suc  9167  nn0ge0  9432  xnn0xr  9475  xnn0nemnf  9481  elnn0z  9497  nn0n0n1ge2b  9564  nn0ind-raph  9602  elnn1uz2  9846  indstr2  9848  xrnemnf  10017  xrnepnf  10018  mnfltxr  10026  nn0pnfge0  10031  xrlttr  10035  xrltso  10036  xrlttri3  10037  nltpnft  10054  npnflt  10055  ngtmnft  10057  nmnfgt  10058  xsubge0  10121  xposdif  10122  xleaddadd  10127  fztpval  10323  fseq1p1m1  10334  fz01or  10351  qbtwnxr  10523  xqltnle  10533  fzfig  10698  uzsinds  10712  ser0f  10802  1exp  10836  0exp  10842  bcn1  11026  en1hash  11068  zfz1iso  11111  hash2en  11113  0wrd0  11148  wrdlen1  11160  wrdl1exs1  11215  swrdspsleq  11257  cats1un  11311  wrdind  11312  wrd2ind  11313  sqrt0rlem  11586  fzf1o  11959  prodf1f  12127  0dvds  12395  nn0o  12491  flodddiv4  12520  bitsp1o  12537  gcddvds  12557  bezoutlemmain  12592  lcmdvds  12674  rpdvds  12694  1nprm  12709  prmind2  12715  nnoddn2prmb  12858  pcpre1  12888  qexpz  12948  4sqlem19  13005  ennnfonelemj0  13045  ennnfonelemhf1o  13057  strslfv  13150  restsspw  13355  xpsfrnel  13450  mgmidcl  13484  mgmlrid  13485  releqgg  13830  islidlm  14517  zrhrhm  14661  psrplusgg  14721  baspartn  14803  eltg3  14810  topnex  14839  discld  14889  cnpfval  14948  cnprcl2k  14959  idcn  14965  xmet0  15116  blfvalps  15138  blfps  15162  blf  15163  limcimolemlt  15417  recnprss  15440  lgsdir2lem2  15787  gausslemma2dlem4  15822  2lgslem2  15850  2lgslem3  15859  2lgs  15862  2sqlem7  15879  uhgr0e  15962  incistruhgr  15970  issubgr2  16138  subgrprop2  16140  egrsubgr  16143  0grsubgr  16144  0uhgrsubgr  16145  uhgrsubgrself  16146  clwwlkn1  16298  funmptd  16460  bj-om  16592  bj-nn0suc0  16605  bj-nn0suc  16619  bj-nn0sucALT  16633  bj-findis  16634  2omap  16654  pw1map  16656  nninfall  16674  nnnninfen  16686  trilpolemcl  16708  dceqnconst  16732  dcapnconst  16733  gsumgfsum1  16749