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  907  orandc  939  19.9ht  1641  ax11v2  1820  ax11v  1827  ax11ev  1828  equs5or  1830  nfsbxy  1942  nfsbxyt  1943  nfabdw  2338  eqvisset  2747  vtoclgf  2795  vtoclg1f  2796  eueq3dc  2911  mo2icl  2916  csbiegf  3100  un00  3469  sneqr  3760  preqr1  3768  preq12b  3770  prel12  3771  nfopd  3795  ssex  4140  exmidundif  4206  iunpw  4480  nfimad  4979  dfrel2  5079  funsng  5262  cnvresid  5290  nffvd  5527  fnbrfvb  5556  funfvop  5628  acexmidlema  5865  tposf12  6269  supsnti  7003  exmidonfinlem  7191  sucpw1ne3  7230  sucpw1nel3  7231  recidnq  7391  ltaddnq  7405  ltadd1sr  7774  suplocsrlempr  7805  pncan3  8163  divcanap2  8635  ltp1  8799  ltm1  8801  recreclt  8855  nn0ind-raph  9368  2tnp1ge0ge0  10298  fsumcnv  11440  fprodcnv  11628  ef01bndlem  11759  sin01gt0  11764  cos01gt0  11765  ltoddhalfle  11892  bezoutlemnewy  11991  isprm5  12136  nmznsg  13026  tangtx  14152  bdsepnft  14521  bdssex  14536  bj-inex  14541  bj-d0clsepcl  14559  bj-2inf  14572  bj-inf2vnlem2  14605