Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbii GIF 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 𝜓
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 146 1 (𝜑𝜒)
 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  893  orandc  924  19.9ht  1617  ax11v2  1788  ax11v  1795  ax11ev  1796  equs5or  1798  nfsbxy  1910  nfsbxyt  1911  eqvisset  2701  vtoclgf  2749  vtoclg1f  2750  eueq3dc  2864  mo2icl  2869  csbiegf  3050  un00  3416  sneqr  3697  preqr1  3705  preq12b  3707  prel12  3708  nfopd  3732  ssex  4075  exmidundif  4140  iunpw  4412  nfimad  4902  dfrel2  5001  funsng  5181  cnvresid  5209  nffvd  5445  fnbrfvb  5474  funfvop  5544  acexmidlema  5777  tposf12  6178  supsnti  6909  exmidonfinlem  7078  sucpw1ne3  7112  sucpw1nel3  7113  recidnq  7254  ltaddnq  7268  ltadd1sr  7637  suplocsrlempr  7668  pncan3  8023  divcanap2  8493  ltp1  8655  ltm1  8657  recreclt  8711  nn0ind-raph  9221  2tnp1ge0ge0  10134  fsumcnv  11267  ef01bndlem  11535  sin01gt0  11540  cos01gt0  11541  ltoddhalfle  11662  bezoutlemnewy  11756  tangtx  13003  bdsepnft  13301  bdssex  13316  bj-inex  13321  bj-d0clsepcl  13339  bj-2inf  13352  bj-inf2vnlem2  13385
 Copyright terms: Public domain W3C validator