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  915  orandc  948  19.9ht  1690  ax11v2  1869  ax11v  1876  ax11ev  1877  equs5or  1879  nfsbxy  1998  nfsbxyt  1999  nfabdw  2405  eqvisset  2826  vtoclgf  2875  vtoclg1f  2876  eueq3dc  2994  mo2icl  2999  csbiegf  3185  un00  3559  sneqr  3869  preqr1  3877  preq12b  3879  prel12  3880  nfopd  3905  ssex  4252  exmidundif  4324  iunpw  4606  nfimad  5115  dfrel2  5218  funsng  5407  cnvresid  5435  nffvd  5687  fnbrfvb  5720  funfvop  5795  acexmidlema  6049  tposf12  6513  supsnti  7309  pr2cv1  7505  exmidonfinlem  7509  sucpw1ne3  7555  sucpw1nel3  7556  recidnq  7724  ltaddnq  7738  ltadd1sr  8107  suplocsrlempr  8138  pncan3  8497  divcanap2  8971  ltp1  9135  ltm1  9137  recreclt  9191  nn0ind-raph  9713  2tnp1ge0ge0  10685  iswrdiz  11256  fsumcnv  12148  fprodcnv  12336  ef01bndlem  12467  sin01gt0  12473  cos01gt0  12474  ltoddhalfle  12604  bezoutlemnewy  12717  isprm5  12864  4sqlem12  13125  gsumval2  13660  nmznsg  13966  gfsump1  14108  tangtx  15829  gausslemma2dlem1a  16057  lgseisenlem4  16072  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  bdsepnft  16783  bdssex  16798  bj-inex  16803  bj-d0clsepcl  16821  bj-2inf  16834  bj-inf2vnlem2  16867