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  907  orandc  939  19.9ht  1641  ax11v2  1820  ax11v  1827  ax11ev  1828  equs5or  1830  nfsbxy  1942  nfsbxyt  1943  nfabdw  2338  eqvisset  2748  vtoclgf  2796  vtoclg1f  2797  eueq3dc  2912  mo2icl  2917  csbiegf  3101  un00  3470  sneqr  3761  preqr1  3769  preq12b  3771  prel12  3772  nfopd  3796  ssex  4141  exmidundif  4207  iunpw  4481  nfimad  4980  dfrel2  5080  funsng  5263  cnvresid  5291  nffvd  5528  fnbrfvb  5557  funfvop  5629  acexmidlema  5866  tposf12  6270  supsnti  7004  exmidonfinlem  7192  sucpw1ne3  7231  sucpw1nel3  7232  recidnq  7392  ltaddnq  7406  ltadd1sr  7775  suplocsrlempr  7806  pncan3  8165  divcanap2  8637  ltp1  8801  ltm1  8803  recreclt  8857  nn0ind-raph  9370  2tnp1ge0ge0  10301  fsumcnv  11445  fprodcnv  11633  ef01bndlem  11764  sin01gt0  11769  cos01gt0  11770  ltoddhalfle  11898  bezoutlemnewy  11997  isprm5  12142  nmznsg  13073  tangtx  14262  bdsepnft  14642  bdssex  14657  bj-inex  14662  bj-d0clsepcl  14680  bj-2inf  14693  bj-inf2vnlem2  14726