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  1655  ax11v2  1834  ax11v  1841  ax11ev  1842  equs5or  1844  nfsbxy  1961  nfsbxyt  1962  nfabdw  2358  eqvisset  2773  vtoclgf  2822  vtoclg1f  2823  eueq3dc  2938  mo2icl  2943  csbiegf  3128  un00  3498  sneqr  3791  preqr1  3799  preq12b  3801  prel12  3802  nfopd  3826  ssex  4171  exmidundif  4240  iunpw  4516  nfimad  5019  dfrel2  5121  funsng  5305  cnvresid  5333  nffvd  5571  fnbrfvb  5602  funfvop  5675  acexmidlema  5914  tposf12  6328  supsnti  7072  exmidonfinlem  7262  sucpw1ne3  7301  sucpw1nel3  7302  recidnq  7462  ltaddnq  7476  ltadd1sr  7845  suplocsrlempr  7876  pncan3  8236  divcanap2  8709  ltp1  8873  ltm1  8875  recreclt  8929  nn0ind-raph  9445  2tnp1ge0ge0  10393  iswrdiz  10944  fsumcnv  11604  fprodcnv  11792  ef01bndlem  11923  sin01gt0  11929  cos01gt0  11930  ltoddhalfle  12060  bezoutlemnewy  12173  isprm5  12320  4sqlem12  12581  gsumval2  13050  nmznsg  13353  tangtx  15084  gausslemma2dlem1a  15309  lgseisenlem4  15324  2lgslem3a  15344  2lgslem3b  15345  2lgslem3c  15346  2lgslem3d  15347  bdsepnft  15543  bdssex  15558  bj-inex  15563  bj-d0clsepcl  15581  bj-2inf  15594  bj-inf2vnlem2  15627