ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbii GIF 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 𝜓
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 145 1 (𝜑𝜒)
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  1743  ax11v  1750  ax11ev  1751  equs5or  1753  nfsbxy  1861  nfsbxyt  1862  eqvisset  2619  vtoclgf  2667  eueq3dc  2776  mo2icl  2781  csbiegf  2956  un00  3307  sneqr  3573  preqr1  3581  preq12b  3583  prel12  3584  nfopd  3608  ssex  3936  exmidundif  3992  iunpw  4258  nfimad  4728  dfrel2  4822  funsng  4997  cnvresid  5025  nffvd  5240  fnbrfvb  5268  funfvop  5333  acexmidlema  5556  tposf12  5940  supsnti  6514  recidnq  6722  ltaddnq  6736  ltadd1sr  7092  pncan3  7460  divcanap2  7912  ltp1  8066  ltm1  8068  recreclt  8122  nn0ind-raph  8622  2tnp1ge0ge0  9460  ltoddhalfle  10525  bezoutlemnewy  10617  bdsepnft  10970  bdssex  10985  bj-inex  10990  bj-d0clsepcl  11012  bj-2inf  11025  bj-inf2vnlem2  11058
  Copyright terms: Public domain W3C validator