Theorem mpbii 146

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	|- ps
mpbii.maj	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mpbii	|- ( ph -> ch )

Proof of Theorem mpbii

Step	Hyp	Ref	Expression
1		mpbii.min	. . 3 |- ps
2	1	a1i 9	. 2 |- ( ph -> ps )
3		mpbii.maj	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	mpbid 145	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm2.26dc  847  orandc  881  19.9ht  1573  ax11v2  1742  ax11v  1749  ax11ev  1750  equs5or  1752  nfsbxy  1860  nfsbxyt  1861  eqvisset  2610  vtoclgf  2658  eueq3dc  2767  mo2icl  2772  csbiegf  2947  un00  3297  sneqr  3560  preqr1  3568  preq12b  3570  prel12  3571  nfopd  3595  ssex  3923  iunpw  4237  nfimad  4707  dfrel2  4801  funsng  4976  cnvresid  5004  nffvd  5218  fnbrfvb  5246  funfvop  5311  acexmidlema  5534  tposf12  5918  supsnti  6477  recidnq  6645  ltaddnq  6659  ltadd1sr  7015  pncan3  7383  divcanap2  7835  ltp1  7989  ltm1  7991  recreclt  8045  nn0ind-raph  8545  2tnp1ge0ge0  9383  ltoddhalfle  10437  bezoutlemnewy  10529  bdsepnft  10836  bdssex  10851  bj-inex  10856  bj-d0clsepcl  10878  bj-2inf  10891  bj-inf2vnlem2  10924