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  2810  vtoclgf  2859  vtoclg1f  2860  eueq3dc  2977  mo2icl  2982  csbiegf  3168  un00  3538  sneqr  3837  preqr1  3845  preq12b  3847  prel12  3848  nfopd  3873  ssex  4220  exmidundif  4289  iunpw  4570  nfimad  5076  dfrel2  5178  funsng  5366  cnvresid  5394  nffvd  5638  fnbrfvb  5671  funfvop  5746  acexmidlema  5991  tposf12  6413  supsnti  7168  pr2cv1  7364  exmidonfinlem  7367  sucpw1ne3  7413  sucpw1nel3  7414  recidnq  7576  ltaddnq  7590  ltadd1sr  7959  suplocsrlempr  7990  pncan3  8350  divcanap2  8823  ltp1  8987  ltm1  8989  recreclt  9043  nn0ind-raph  9560  2tnp1ge0ge0  10516  iswrdiz  11073  fsumcnv  11943  fprodcnv  12131  ef01bndlem  12262  sin01gt0  12268  cos01gt0  12269  ltoddhalfle  12399  bezoutlemnewy  12512  isprm5  12659  4sqlem12  12920  gsumval2  13425  nmznsg  13745  tangtx  15506  gausslemma2dlem1a  15731  lgseisenlem4  15746  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  bdsepnft  16208  bdssex  16223  bj-inex  16228  bj-d0clsepcl  16246  bj-2inf  16259  bj-inf2vnlem2  16292