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  1407  ceqsexv2d  2820  dedhb  2952  sbceqal  3064  ssdifeq0  3554  pwidg  3643  elpr2  3668  snidg  3675  exsnrex  3688  rabrsndc  3714  prid1g  3750  tpid1g  3758  tpid2g  3760  sssnr  3810  ssprr  3813  sstpr  3814  preqr1  3825  unimax  3901  intmin3  3929  eqbrtrdi  4101  pwnss  4222  0inp0  4229  bnd2  4236  ss1o0el1  4260  exmidsssn  4265  exmidundif  4269  exmidundifim  4270  euabex  4290  copsexg  4309  euotd  4320  elopab  4325  epelg  4358  sucidg  4484  ifelpwung  4549  regexmidlem1  4602  sucprcreg  4618  onprc  4621  dtruex  4628  omelon2  4677  elvvuni  4760  eqrelriv  4789  relopabi  4824  opabid2  4830  ididg  4852  iss  5027  funopg  5328  fn0  5419  f00  5493  f0bi  5494  f10d  5583  f1o00  5584  fo00  5585  brprcneu  5596  relelfvdm  5635  fsn  5780  funop  5791  eufnfv  5843  f1eqcocnv  5888  riotaprop  5953  acexmidlemb  5966  acexmidlemab  5968  acexmidlem2  5971  oprabid  6006  elrnmpo  6089  ov6g  6114  eqop2  6294  1stconst  6337  2ndconst  6338  dftpos3  6378  dftpos4  6379  2pwuninelg  6399  frecabcl  6515  el2oss1o  6559  ecopover  6750  map0g  6805  mapsn  6807  elixpsn  6852  en0  6917  en1  6921  fiprc  6938  en2m  6944  dom0  6967  nneneq  6986  findcard  7018  findcard2  7019  findcard2s  7020  sbthlem2  7093  sbthlemi4  7095  sbthlemi5  7096  eldju2ndl  7207  updjudhf  7214  enumct  7250  nnnninf  7261  nninfisollem0  7265  fodjuomnilemdc  7279  exmidonfinlem  7339  exmidaclem  7358  pw1ne1  7382  pw1ne3  7383  1ne0sr  7921  00sr  7924  cnm  7987  eqlei2  8209  cnstab  8760  divcanap3  8813  sup3exmid  9072  nn1suc  9097  nn0ge0  9362  xnn0xr  9405  xnn0nemnf  9411  elnn0z  9427  nn0n0n1ge2b  9494  nn0ind-raph  9532  elnn1uz2  9770  indstr2  9772  xrnemnf  9941  xrnepnf  9942  mnfltxr  9950  nn0pnfge0  9955  xrlttr  9959  xrltso  9960  xrlttri3  9961  nltpnft  9978  npnflt  9979  ngtmnft  9981  nmnfgt  9982  xsubge0  10045  xposdif  10046  xleaddadd  10051  fztpval  10247  fseq1p1m1  10258  fz01or  10275  qbtwnxr  10444  xqltnle  10454  fzfig  10619  uzsinds  10633  ser0f  10723  1exp  10757  0exp  10763  bcn1  10947  zfz1iso  11030  hash2en  11032  0wrd0  11064  wrdlen1  11075  wrdl1exs1  11128  swrdspsleq  11165  cats1un  11219  wrdind  11220  wrd2ind  11221  sqrt0rlem  11480  prodf1f  12020  0dvds  12288  nn0o  12384  flodddiv4  12413  bitsp1o  12430  gcddvds  12450  bezoutlemmain  12485  lcmdvds  12567  rpdvds  12587  1nprm  12602  prmind2  12608  nnoddn2prmb  12751  pcpre1  12781  qexpz  12841  4sqlem19  12898  ennnfonelemj0  12938  ennnfonelemhf1o  12950  strslfv  13043  restsspw  13248  xpsfrnel  13343  mgmidcl  13377  mgmlrid  13378  releqgg  13723  islidlm  14408  zrhrhm  14552  psrplusgg  14607  baspartn  14689  eltg3  14696  topnex  14725  discld  14775  lmreltop  14832  cnpfval  14834  cnprcl2k  14845  idcn  14851  xmet0  15002  blfvalps  15024  blfps  15048  blf  15049  limcimolemlt  15303  recnprss  15326  lgsdir2lem2  15673  gausslemma2dlem4  15708  2lgslem2  15736  2lgslem3  15745  2lgs  15748  2sqlem7  15765  uhgr0e  15847  incistruhgr  15855  funmptd  16077  bj-om  16210  bj-nn0suc0  16223  bj-nn0suc  16237  bj-nn0sucALT  16251  bj-findis  16252  2omap  16270  pw1map  16272  nninfall  16286  nnnninfen  16298  trilpolemcl  16316  dceqnconst  16339  dcapnconst  16340