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  941  19.9ht  1663  ax11v2  1842  ax11v  1849  ax11ev  1850  equs5or  1852  nfsbxy  1969  nfsbxyt  1970  nfabdw  2366  eqvisset  2781  vtoclgf  2830  vtoclg1f  2831  eueq3dc  2946  mo2icl  2951  csbiegf  3136  un00  3506  sneqr  3800  preqr1  3808  preq12b  3810  prel12  3811  nfopd  3835  ssex  4180  exmidundif  4249  iunpw  4526  nfimad  5030  dfrel2  5132  funsng  5319  cnvresid  5347  nffvd  5587  fnbrfvb  5618  funfvop  5691  acexmidlema  5934  tposf12  6354  supsnti  7106  exmidonfinlem  7300  sucpw1ne3  7343  sucpw1nel3  7344  recidnq  7505  ltaddnq  7519  ltadd1sr  7888  suplocsrlempr  7919  pncan3  8279  divcanap2  8752  ltp1  8916  ltm1  8918  recreclt  8972  nn0ind-raph  9489  2tnp1ge0ge0  10442  iswrdiz  10999  fsumcnv  11719  fprodcnv  11907  ef01bndlem  12038  sin01gt0  12044  cos01gt0  12045  ltoddhalfle  12175  bezoutlemnewy  12288  isprm5  12435  4sqlem12  12696  gsumval2  13200  nmznsg  13520  tangtx  15281  gausslemma2dlem1a  15506  lgseisenlem4  15521  2lgslem3a  15541  2lgslem3b  15542  2lgslem3c  15543  2lgslem3d  15544  bdsepnft  15785  bdssex  15800  bj-inex  15805  bj-d0clsepcl  15823  bj-2inf  15836  bj-inf2vnlem2  15869