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	|- 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 147	1 |- ( ph -> ch )

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  912  orandc  945  19.9ht  1687  ax11v2  1866  ax11v  1873  ax11ev  1874  equs5or  1876  nfsbxy  1993  nfsbxyt  1994  nfabdw  2391  eqvisset  2811  vtoclgf  2860  vtoclg1f  2861  eueq3dc  2978  mo2icl  2983  csbiegf  3169  un00  3539  sneqr  3841  preqr1  3849  preq12b  3851  prel12  3852  nfopd  3877  ssex  4224  exmidundif  4294  iunpw  4575  nfimad  5083  dfrel2  5185  funsng  5373  cnvresid  5401  nffvd  5647  fnbrfvb  5680  funfvop  5755  acexmidlema  6004  tposf12  6430  supsnti  7195  pr2cv1  7391  exmidonfinlem  7394  sucpw1ne3  7440  sucpw1nel3  7441  recidnq  7603  ltaddnq  7617  ltadd1sr  7986  suplocsrlempr  8017  pncan3  8377  divcanap2  8850  ltp1  9014  ltm1  9016  recreclt  9070  nn0ind-raph  9587  2tnp1ge0ge0  10551  iswrdiz  11110  fsumcnv  11988  fprodcnv  12176  ef01bndlem  12307  sin01gt0  12313  cos01gt0  12314  ltoddhalfle  12444  bezoutlemnewy  12557  isprm5  12704  4sqlem12  12965  gsumval2  13470  nmznsg  13790  tangtx  15552  gausslemma2dlem1a  15777  lgseisenlem4  15792  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  bdsepnft  16418  bdssex  16433  bj-inex  16438  bj-d0clsepcl  16456  bj-2inf  16469  bj-inf2vnlem2  16502