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

Theorem mpbii 136
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 ψ
mpbii.maj (φ → (ψχ))
Assertion
Ref Expression
mpbii (φχ)

Proof of Theorem mpbii
StepHypRef Expression
1 mpbii.min . . 3 ψ
21a1i 9 . 2 (φψ)
3 mpbii.maj . 2 (φ → (ψχ))
42, 3mpbid 135 1 (φχ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm2.26dc  812  19.9ht  1529  ax11v2  1698  ax11v  1705  ax11ev  1706  equs5or  1708  nfsbxy  1815  nfsbxyt  1816  eqvisset  2559  vtoclgf  2606  eueq3dc  2709  mo2icl  2714  csbiegf  2884  un00  3257  sneqr  3522  preqr1  3530  preq12b  3532  prel12  3533  nfopd  3557  ssex  3885  iunpw  4177  nfimad  4620  dfrel2  4714  elxp5  4752  funsng  4889  cnvresid  4916  nffvd  5130  fnbrfvb  5157  funfvop  5222  acexmidlema  5446  tposf12  5825  recidnq  6377  ltaddnq  6390  pncan3  6976  divcanap2  7401  ltp1  7551  ltm1  7553  recreclt  7607  nn0ind-raph  8091  bdsepnft  9275  bdssex  9287  bj-inex  9292  bj-d0clsepcl  9314  bj-2inf  9326  bj-inf2vnlem2  9355
  Copyright terms: Public domain W3C validator