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  5573  fnbrfvb  5604  funfvop  5677  acexmidlema  5916  tposf12  6336  supsnti  7080  exmidonfinlem  7272  sucpw1ne3  7315  sucpw1nel3  7316  recidnq  7477  ltaddnq  7491  ltadd1sr  7860  suplocsrlempr  7891  pncan3  8251  divcanap2  8724  ltp1  8888  ltm1  8890  recreclt  8944  nn0ind-raph  9460  2tnp1ge0ge0  10408  iswrdiz  10959  fsumcnv  11619  fprodcnv  11807  ef01bndlem  11938  sin01gt0  11944  cos01gt0  11945  ltoddhalfle  12075  bezoutlemnewy  12188  isprm5  12335  4sqlem12  12596  gsumval2  13099  nmznsg  13419  tangtx  15158  gausslemma2dlem1a  15383  lgseisenlem4  15398  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  bdsepnft  15617  bdssex  15632  bj-inex  15637  bj-d0clsepcl  15655  bj-2inf  15668  bj-inf2vnlem2  15701