ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbii Unicode version

Theorem mpbii 147
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
StepHypRef Expression
1 mpbii.min . . 3  |-  ps
21a1i 9 . 2  |-  ( ph  ->  ps )
3 mpbii.maj . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3mpbid 146 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm2.26dc  897  orandc  928  19.9ht  1628  ax11v2  1807  ax11v  1814  ax11ev  1815  equs5or  1817  nfsbxy  1929  nfsbxyt  1930  nfabdw  2325  eqvisset  2732  vtoclgf  2780  vtoclg1f  2781  eueq3dc  2896  mo2icl  2901  csbiegf  3084  un00  3451  sneqr  3735  preqr1  3743  preq12b  3745  prel12  3746  nfopd  3770  ssex  4114  exmidundif  4180  iunpw  4453  nfimad  4950  dfrel2  5049  funsng  5229  cnvresid  5257  nffvd  5493  fnbrfvb  5522  funfvop  5592  acexmidlema  5828  tposf12  6229  supsnti  6962  exmidonfinlem  7141  sucpw1ne3  7180  sucpw1nel3  7181  recidnq  7326  ltaddnq  7340  ltadd1sr  7709  suplocsrlempr  7740  pncan3  8098  divcanap2  8568  ltp1  8731  ltm1  8733  recreclt  8787  nn0ind-raph  9300  2tnp1ge0ge0  10227  fsumcnv  11368  fprodcnv  11556  ef01bndlem  11687  sin01gt0  11692  cos01gt0  11693  ltoddhalfle  11819  bezoutlemnewy  11918  isprm5  12063  tangtx  13326  bdsepnft  13630  bdssex  13645  bj-inex  13650  bj-d0clsepcl  13668  bj-2inf  13681  bj-inf2vnlem2  13714
  Copyright terms: Public domain W3C validator