NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  mpbid GIF version

Theorem mpbid 201
Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbid.min (φψ)
mpbid.maj (φ → (ψχ))
Assertion
Ref Expression
mpbid (φχ)

Proof of Theorem mpbid
StepHypRef Expression
1 mpbid.min . 2 (φψ)
2 mpbid.maj . . 3 (φ → (ψχ))
32biimpd 198 . 2 (φ → (ψχ))
41, 3mpd 14 1 (φχ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  mpbii  202  mpbi2and  887  dvelimdf  2082  ax11eq  2193  ax11el  2194  eqtrd  2385  eleqtrd  2429  neeqtrd  2538  3netr3d  2542  rexlimd2  2736  ceqsalt  2881  vtoclgft  2905  vtoclegft  2926  eueq2  3010  sbceq1dd  3052  csbexg  3146  csbiedf  3173  sseqtrd  3307  3sstr3d  3313  ifbothda  3692  elimdhyp  3715  snssd  3853  dfnfc2  3909  opkth1g  4130  iota4  4357  findsd  4410  ltfintri  4466  t1csfin1c  4545  vfintle  4546  vfin1cltv  4547  vfinspclt  4552  breqtrd  4663  3brtr3d  4668  fssres2  5239  feu  5242  f1orescnv  5301  resdif  5306  fimacnv  5411  fsn2  5434  isoini2  5498  clos1is  5881  erthi  5970  mapsn  6026  enmap2lem5  6067  enmap1lem5  6073  enprmaplem5  6080  eqncg  6126  ceclr  6187  ceclnn1  6189  nc0suc  6217  te0c  6236  nmembers1lem3  6269  spacis  6286  nchoicelem5  6291  nchoicelem17  6303  nchoicelem19  6305  nchoice  6306  fnfreclem3  6317
  Copyright terms: Public domain W3C validator