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  892  orandc  923  19.9ht  1620  ax11v2  1792  ax11v  1799  ax11ev  1800  equs5or  1802  nfsbxy  1915  nfsbxyt  1916  eqvisset  2696  vtoclgf  2744  vtoclg1f  2745  eueq3dc  2858  mo2icl  2863  csbiegf  3043  un00  3409  sneqr  3687  preqr1  3695  preq12b  3697  prel12  3698  nfopd  3722  ssex  4065  exmidundif  4129  iunpw  4401  nfimad  4890  dfrel2  4989  funsng  5169  cnvresid  5197  nffvd  5433  fnbrfvb  5462  funfvop  5532  acexmidlema  5765  tposf12  6166  supsnti  6892  exmidonfinlem  7054  recidnq  7213  ltaddnq  7227  ltadd1sr  7596  suplocsrlempr  7627  pncan3  7982  divcanap2  8452  ltp1  8614  ltm1  8616  recreclt  8670  nn0ind-raph  9180  2tnp1ge0ge0  10086  fsumcnv  11218  ef01bndlem  11474  sin01gt0  11479  cos01gt0  11480  ltoddhalfle  11601  bezoutlemnewy  11695  tangtx  12941  bdsepnft  13190  bdssex  13205  bj-inex  13210  bj-d0clsepcl  13228  bj-2inf  13241  bj-inf2vnlem2  13274
  Copyright terms: Public domain W3C validator