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  1868  ax11v  1875  ax11ev  1876  equs5or  1878  nfsbxy  1995  nfsbxyt  1996  nfabdw  2394  eqvisset  2814  vtoclgf  2863  vtoclg1f  2864  eueq3dc  2981  mo2icl  2986  csbiegf  3172  un00  3543  sneqr  3848  preqr1  3856  preq12b  3858  prel12  3859  nfopd  3884  ssex  4231  exmidundif  4302  iunpw  4583  nfimad  5091  dfrel2  5194  funsng  5383  cnvresid  5411  nffvd  5660  fnbrfvb  5693  funfvop  5768  acexmidlema  6019  tposf12  6478  supsnti  7247  pr2cv1  7443  exmidonfinlem  7447  sucpw1ne3  7493  sucpw1nel3  7494  recidnq  7656  ltaddnq  7670  ltadd1sr  8039  suplocsrlempr  8070  pncan3  8429  divcanap2  8902  ltp1  9066  ltm1  9068  recreclt  9122  nn0ind-raph  9641  2tnp1ge0ge0  10607  iswrdiz  11169  fsumcnv  12061  fprodcnv  12249  ef01bndlem  12380  sin01gt0  12386  cos01gt0  12387  ltoddhalfle  12517  bezoutlemnewy  12630  isprm5  12777  4sqlem12  13038  gsumval2  13543  nmznsg  13863  tangtx  15632  gausslemma2dlem1a  15860  lgseisenlem4  15875  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  bdsepnft  16586  bdssex  16601  bj-inex  16606  bj-d0clsepcl  16624  bj-2inf  16637  bj-inf2vnlem2  16670  gfsump1  16798