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  940  19.9ht  1651  ax11v2  1830  ax11v  1837  ax11ev  1838  equs5or  1840  nfsbxy  1952  nfsbxyt  1953  nfabdw  2348  eqvisset  2759  vtoclgf  2807  vtoclg1f  2808  eueq3dc  2923  mo2icl  2928  csbiegf  3112  un00  3481  sneqr  3772  preqr1  3780  preq12b  3782  prel12  3783  nfopd  3807  ssex  4152  exmidundif  4218  iunpw  4492  nfimad  4991  dfrel2  5091  funsng  5274  cnvresid  5302  nffvd  5539  fnbrfvb  5569  funfvop  5641  acexmidlema  5879  tposf12  6284  supsnti  7018  exmidonfinlem  7206  sucpw1ne3  7245  sucpw1nel3  7246  recidnq  7406  ltaddnq  7420  ltadd1sr  7789  suplocsrlempr  7820  pncan3  8179  divcanap2  8651  ltp1  8815  ltm1  8817  recreclt  8871  nn0ind-raph  9384  2tnp1ge0ge0  10315  fsumcnv  11459  fprodcnv  11647  ef01bndlem  11778  sin01gt0  11783  cos01gt0  11784  ltoddhalfle  11912  bezoutlemnewy  12011  isprm5  12156  nmznsg  13113  tangtx  14612  bdsepnft  14992  bdssex  15007  bj-inex  15012  bj-d0clsepcl  15030  bj-2inf  15043  bj-inf2vnlem2  15076