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  1996  nfsbxyt  1997  nfabdw  2403  eqvisset  2824  vtoclgf  2873  vtoclg1f  2874  eueq3dc  2991  mo2icl  2996  csbiegf  3182  un00  3555  sneqr  3864  preqr1  3872  preq12b  3874  prel12  3875  nfopd  3900  ssex  4247  exmidundif  4319  iunpw  4601  nfimad  5110  dfrel2  5213  funsng  5402  cnvresid  5430  nffvd  5682  fnbrfvb  5715  funfvop  5790  acexmidlema  6041  tposf12  6500  supsnti  7296  pr2cv1  7492  exmidonfinlem  7496  sucpw1ne3  7542  sucpw1nel3  7543  recidnq  7708  ltaddnq  7722  ltadd1sr  8091  suplocsrlempr  8122  pncan3  8481  divcanap2  8954  ltp1  9118  ltm1  9120  recreclt  9174  nn0ind-raph  9695  2tnp1ge0ge0  10661  iswrdiz  11231  fsumcnv  12123  fprodcnv  12311  ef01bndlem  12442  sin01gt0  12448  cos01gt0  12449  ltoddhalfle  12579  bezoutlemnewy  12692  isprm5  12839  4sqlem12  13100  gsumval2  13610  nmznsg  13930  tangtx  15703  gausslemma2dlem1a  15931  lgseisenlem4  15946  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  bdsepnft  16657  bdssex  16672  bj-inex  16677  bj-d0clsepcl  16695  bj-2inf  16708  bj-inf2vnlem2  16741  gfsump1  16868