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  2913  eueq3  3011  moeq3  3013  mo2icl  3015  sbc2or  3054  csbiegf  3176  un00  3586  elimhyp  3710  elimhyp2v  3711  elimhyp3v  3712  elimhyp4v  3713  elimdhyp  3715  keephyp2v  3717  keephyp3v  3718  sneqr  3872  unsneqsn  3887  preqr1  4124  preq12b  4127  lefinlteq  4463  proj2op  4601  nfopd  4605  phiall  4618  nfimad  4954  cnvresid  5166  nffvd  5335  tz6.12i  5348  fvelrnb  5365  fvelimab  5370  funfvop  5400  opbr1st  5501  opbr2nd  5502  bren  6030  idssen  6040  enadj  6060  ncvsq  6256