Theorem mpbii 148

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
mpbii.min	⊢ 𝜓
mpbii.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbii	⊢ (𝜑 → 𝜒)

Proof of Theorem mpbii

Step	Hyp	Ref	Expression
1		mpbii.min	. . 3 ⊢ 𝜓
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜓)
3		mpbii.maj	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	mpbid 147	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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.26dc  912  orandc  945  19.9ht  1687  ax11v2  1866  ax11v  1873  ax11ev  1874  equs5or  1876  nfsbxy  1993  nfsbxyt  1994  nfabdw  2391  eqvisset  2810  vtoclgf  2859  vtoclg1f  2860  eueq3dc  2977  mo2icl  2982  csbiegf  3168  un00  3538  sneqr  3838  preqr1  3846  preq12b  3848  prel12  3849  nfopd  3874  ssex  4221  exmidundif  4291  iunpw  4572  nfimad  5080  dfrel2  5182  funsng  5370  cnvresid  5398  nffvd  5644  fnbrfvb  5677  funfvop  5752  acexmidlema  6001  tposf12  6426  supsnti  7188  pr2cv1  7384  exmidonfinlem  7387  sucpw1ne3  7433  sucpw1nel3  7434  recidnq  7596  ltaddnq  7610  ltadd1sr  7979  suplocsrlempr  8010  pncan3  8370  divcanap2  8843  ltp1  9007  ltm1  9009  recreclt  9063  nn0ind-raph  9580  2tnp1ge0ge0  10538  iswrdiz  11096  fsumcnv  11969  fprodcnv  12157  ef01bndlem  12288  sin01gt0  12294  cos01gt0  12295  ltoddhalfle  12425  bezoutlemnewy  12538  isprm5  12685  4sqlem12  12946  gsumval2  13451  nmznsg  13771  tangtx  15533  gausslemma2dlem1a  15758  lgseisenlem4  15773  2lgslem3a  15793  2lgslem3b  15794  2lgslem3c  15795  2lgslem3d  15796  bdsepnft  16359  bdssex  16374  bj-inex  16379  bj-d0clsepcl  16397  bj-2inf  16410  bj-inf2vnlem2  16443