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  919  orandc  952  19.9ht  1694  ax11v2  1873  ax11v  1880  ax11ev  1881  equs5or  1883  nfsbxy  2002  nfsbxyt  2003  nfabdw  2411  eqvisset  2832  vtoclgf  2881  vtoclg1f  2882  eueq3dc  3000  mo2icl  3005  csbiegf  3191  un00  3566  vvin  3568  sneqr  3880  preqr1  3888  preq12b  3890  prel12  3891  nfopd  3916  ssex  4265  exmidundif  4338  iunpw  4621  nfimad  5130  dfrel2  5233  funsng  5422  cnvresid  5450  nffvd  5702  fnbrfvb  5735  funfvop  5812  acexmidlema  6066  tposf12  6530  supsnti  7335  pr2cv1  7531  exmidonfinlem  7535  sucpw1ne3  7581  sucpw1nel3  7582  recidnq  7750  ltaddnq  7764  ltadd1sr  8133  suplocsrlempr  8164  pncan3  8524  divcanap2  9000  ltp1  9164  ltm1  9166  recreclt  9220  nn0ind-raph  9742  2tnp1ge0ge0  10714  iswrdiz  11289  fsumcnv  12182  fprodcnv  12370  ef01bndlem  12501  sin01gt0  12507  cos01gt0  12508  ltoddhalfle  12638  bezoutlemnewy  12751  isprm5  12898  4sqlem12  13159  gzsumval2  13691  nmznsg  13993  gsump1  14134  tangtx  15862  gausslemma2dlem1a  16091  lgseisenlem4  16106  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  bdsepnft  16827  bdssex  16842  bj-inex  16847  bj-d0clsepcl  16865  bj-2inf  16878  bj-inf2vnlem2  16911