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  849  orandc  883  19.9ht  1575  ax11v2  1745  ax11v  1752  ax11ev  1753  equs5or  1755  nfsbxy  1863  nfsbxyt  1864  eqvisset  2623  vtoclgf  2671  eueq3dc  2780  mo2icl  2785  csbiegf  2960  un00  3317  sneqr  3587  preqr1  3595  preq12b  3597  prel12  3598  nfopd  3622  ssex  3951  exmidundif  4009  iunpw  4275  nfimad  4750  dfrel2  4847  funsng  5025  cnvresid  5053  nffvd  5280  fnbrfvb  5308  funfvop  5374  acexmidlema  5604  tposf12  5988  supsnti  6644  recidnq  6896  ltaddnq  6910  ltadd1sr  7266  pncan3  7634  divcanap2  8086  ltp1  8240  ltm1  8242  recreclt  8296  nn0ind-raph  8796  2tnp1ge0ge0  9636  ltoddhalfle  10775  bezoutlemnewy  10867  bdsepnft  11223  bdssex  11238  bj-inex  11243  bj-d0clsepcl  11265  bj-2inf  11278  bj-inf2vnlem2  11311
  Copyright terms: Public domain W3C validator