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  908  orandc  941  19.9ht  1655  ax11v2  1834  ax11v  1841  ax11ev  1842  equs5or  1844  nfsbxy  1961  nfsbxyt  1962  nfabdw  2358  eqvisset  2773  vtoclgf  2822  vtoclg1f  2823  eueq3dc  2938  mo2icl  2943  csbiegf  3128  un00  3497  sneqr  3790  preqr1  3798  preq12b  3800  prel12  3801  nfopd  3825  ssex  4170  exmidundif  4239  iunpw  4515  nfimad  5018  dfrel2  5120  funsng  5304  cnvresid  5332  nffvd  5570  fnbrfvb  5601  funfvop  5674  acexmidlema  5913  tposf12  6327  supsnti  7071  exmidonfinlem  7260  sucpw1ne3  7299  sucpw1nel3  7300  recidnq  7460  ltaddnq  7474  ltadd1sr  7843  suplocsrlempr  7874  pncan3  8234  divcanap2  8707  ltp1  8871  ltm1  8873  recreclt  8927  nn0ind-raph  9443  2tnp1ge0ge0  10391  iswrdiz  10942  fsumcnv  11602  fprodcnv  11790  ef01bndlem  11921  sin01gt0  11927  cos01gt0  11928  ltoddhalfle  12058  bezoutlemnewy  12163  isprm5  12310  4sqlem12  12571  gsumval2  13040  nmznsg  13343  tangtx  15074  gausslemma2dlem1a  15299  lgseisenlem4  15314  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  bdsepnft  15533  bdssex  15548  bj-inex  15553  bj-d0clsepcl  15571  bj-2inf  15584  bj-inf2vnlem2  15617