Theorem mpbii 202

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 10	. 2 ⊢ (φ → ψ)
3		mpbii.maj	. 2 ⊢ (φ → (ψ ↔ χ))
4	2, 3	mpbid 201	1 ⊢ (φ → χ)

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  elimh  922  ax11v2  1992  sbft  2025  ax11vALT  2097  ax11eq  2193  ax11el  2194  ax11inda  2200  ax11v2-o  2201  vtoclgf  2914  eueq3  3012  moeq3  3014  mo2icl  3016  sbc2or  3055  csbiegf  3177  un00  3587  elimhyp  3711  elimhyp2v  3712  elimhyp3v  3713  elimhyp4v  3714  elimdhyp  3716  keephyp2v  3718  keephyp3v  3719  sneqr  3873  unsneqsn  3888  preqr1  4125  preq12b  4128  lefinlteq  4464  proj2op  4602  nfopd  4606  phiall  4619  nfimad  4955  cnvresid  5167  nffvd  5336  tz6.12i  5349  fvelrnb  5366  fvelimab  5371  funfvop  5401  opbr1st  5502  opbr2nd  5503  bren  6031  idssen  6041  enadj  6061  ncvsq  6257