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  908  orandc  941  19.9ht  1655  ax11v2  1834  ax11v  1841  ax11ev  1842  equs5or  1844  nfsbxy  1961  nfsbxyt  1962  nfabdw  2358  eqvisset  2773  vtoclgf  2822  vtoclg1f  2823  eueq3dc  2938  mo2icl  2943  csbiegf  3128  un00  3498  sneqr  3791  preqr1  3799  preq12b  3801  prel12  3802  nfopd  3826  ssex  4171  exmidundif  4240  iunpw  4516  nfimad  5019  dfrel2  5121  funsng  5305  cnvresid  5333  nffvd  5573  fnbrfvb  5604  funfvop  5677  acexmidlema  5916  tposf12  6336  supsnti  7080  exmidonfinlem  7274  sucpw1ne3  7317  sucpw1nel3  7318  recidnq  7479  ltaddnq  7493  ltadd1sr  7862  suplocsrlempr  7893  pncan3  8253  divcanap2  8726  ltp1  8890  ltm1  8892  recreclt  8946  nn0ind-raph  9462  2tnp1ge0ge0  10410  iswrdiz  10961  fsumcnv  11621  fprodcnv  11809  ef01bndlem  11940  sin01gt0  11946  cos01gt0  11947  ltoddhalfle  12077  bezoutlemnewy  12190  isprm5  12337  4sqlem12  12598  gsumval2  13101  nmznsg  13421  tangtx  15182  gausslemma2dlem1a  15407  lgseisenlem4  15422  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  bdsepnft  15641  bdssex  15656  bj-inex  15661  bj-d0clsepcl  15679  bj-2inf  15692  bj-inf2vnlem2  15725