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

Theorem mpbii 146
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 145 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm2.26dc  847  orandc  881  19.9ht  1573  ax11v2  1742  ax11v  1749  ax11ev  1750  equs5or  1752  nfsbxy  1860  nfsbxyt  1861  eqvisset  2610  vtoclgf  2658  eueq3dc  2767  mo2icl  2772  csbiegf  2947  un00  3297  sneqr  3560  preqr1  3568  preq12b  3570  prel12  3571  nfopd  3595  ssex  3923  iunpw  4237  nfimad  4707  dfrel2  4801  funsng  4976  cnvresid  5004  nffvd  5218  fnbrfvb  5246  funfvop  5311  acexmidlema  5534  tposf12  5918  supsnti  6477  recidnq  6645  ltaddnq  6659  ltadd1sr  7015  pncan3  7383  divcanap2  7835  ltp1  7989  ltm1  7991  recreclt  8045  nn0ind-raph  8545  2tnp1ge0ge0  9383  ltoddhalfle  10437  bezoutlemnewy  10529  bdsepnft  10836  bdssex  10851  bj-inex  10856  bj-d0clsepcl  10878  bj-2inf  10891  bj-inf2vnlem2  10924
  Copyright terms: Public domain W3C validator