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  909  orandc  942  19.9ht  1665  ax11v2  1844  ax11v  1851  ax11ev  1852  equs5or  1854  nfsbxy  1971  nfsbxyt  1972  nfabdw  2369  eqvisset  2787  vtoclgf  2836  vtoclg1f  2837  eueq3dc  2954  mo2icl  2959  csbiegf  3145  un00  3515  sneqr  3814  preqr1  3822  preq12b  3824  prel12  3825  nfopd  3850  ssex  4197  exmidundif  4266  iunpw  4545  nfimad  5050  dfrel2  5152  funsng  5339  cnvresid  5367  nffvd  5611  fnbrfvb  5642  funfvop  5715  acexmidlema  5958  tposf12  6378  supsnti  7133  pr2cv1  7329  exmidonfinlem  7332  sucpw1ne3  7378  sucpw1nel3  7379  recidnq  7541  ltaddnq  7555  ltadd1sr  7924  suplocsrlempr  7955  pncan3  8315  divcanap2  8788  ltp1  8952  ltm1  8954  recreclt  9008  nn0ind-raph  9525  2tnp1ge0ge0  10481  iswrdiz  11038  fsumcnv  11863  fprodcnv  12051  ef01bndlem  12182  sin01gt0  12188  cos01gt0  12189  ltoddhalfle  12319  bezoutlemnewy  12432  isprm5  12579  4sqlem12  12840  gsumval2  13344  nmznsg  13664  tangtx  15425  gausslemma2dlem1a  15650  lgseisenlem4  15665  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  bdsepnft  16022  bdssex  16037  bj-inex  16042  bj-d0clsepcl  16060  bj-2inf  16073  bj-inf2vnlem2  16106