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  1664  ax11v2  1843  ax11v  1850  ax11ev  1851  equs5or  1853  nfsbxy  1970  nfsbxyt  1971  nfabdw  2367  eqvisset  2782  vtoclgf  2831  vtoclg1f  2832  eueq3dc  2947  mo2icl  2952  csbiegf  3137  un00  3507  sneqr  3801  preqr1  3809  preq12b  3811  prel12  3812  nfopd  3836  ssex  4181  exmidundif  4250  iunpw  4527  nfimad  5031  dfrel2  5133  funsng  5320  cnvresid  5348  nffvd  5588  fnbrfvb  5619  funfvop  5692  acexmidlema  5935  tposf12  6355  supsnti  7107  exmidonfinlem  7301  sucpw1ne3  7344  sucpw1nel3  7345  recidnq  7506  ltaddnq  7520  ltadd1sr  7889  suplocsrlempr  7920  pncan3  8280  divcanap2  8753  ltp1  8917  ltm1  8919  recreclt  8973  nn0ind-raph  9490  2tnp1ge0ge0  10444  iswrdiz  11001  fsumcnv  11748  fprodcnv  11936  ef01bndlem  12067  sin01gt0  12073  cos01gt0  12074  ltoddhalfle  12204  bezoutlemnewy  12317  isprm5  12464  4sqlem12  12725  gsumval2  13229  nmznsg  13549  tangtx  15310  gausslemma2dlem1a  15535  lgseisenlem4  15550  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  bdsepnft  15823  bdssex  15838  bj-inex  15843  bj-d0clsepcl  15861  bj-2inf  15874  bj-inf2vnlem2  15907