Theorem mpbii 136

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 135	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm2.26dc  813  19.9ht  1532  ax11v2  1701  ax11v  1708  ax11ev  1709  equs5or  1711  nfsbxy  1818  nfsbxyt  1819  eqvisset  2565  vtoclgf  2612  eueq3dc  2715  mo2icl  2720  csbiegf  2890  un00  3263  sneqr  3531  preqr1  3539  preq12b  3541  prel12  3542  nfopd  3566  ssex  3894  iunpw  4211  nfimad  4677  dfrel2  4771  elxp5  4809  funsng  4946  cnvresid  4973  nffvd  5187  fnbrfvb  5214  funfvop  5279  acexmidlema  5503  tposf12  5884  recidnq  6489  ltaddnq  6503  ltadd1sr  6859  pncan3  7217  divcanap2  7657  ltp1  7808  ltm1  7810  recreclt  7864  nn0ind-raph  8353  2tnp1ge0ge0  9141  bdsepnft  10005  bdssex  10020  bj-inex  10025  bj-d0clsepcl  10047  bj-2inf  10060  bj-inf2vnlem2  10094