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

Theorem mpbird 223
Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbird.min
mpbird.maj
Assertion
Ref Expression
mpbird

Proof of Theorem mpbird
StepHypRef Expression
1 mpbird.min . 2
2 mpbird.maj . . 3
32biimprd 214 . 2
41, 3mpd 14 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  mpbiri  224  mpbir2and  888  mpbir3and  1135  eqeltrd  2427  eqnetrd  2534  3netr4d  2543  eqsstrd  3305  3sstr4d  3314  lefinaddc  4450  nulge  4456  ltfinp1  4462  tfinprop  4489  sucevenodd  4510  sucoddeven  4511  sfintfin  4532  eqbrtrd  4659  3brtr4d  4669  eqfnfvd  5395  fvimacnvi  5402  fconst2g  5452  f1ofveu  5480  f1od  5726  brtxp  5783  trrd  5925  refrd  5926  antird  5928  connexrd  5930  iserd  5942  enmap2lem5  6067  enmap1lem5  6073  enprmaplem5  6080  nenpw1pwlem2  6085  pw1eltc  6162  ce0nnuli  6178  ce0  6190  lecidg  6196  lec0cg  6198  lecncvg  6199  addlec  6208  nmembers1lem3  6270  spacis  6288  nchoicelem17  6305  dmfrec  6316  frec0  6321  frecsuc  6322
  Copyright terms: Public domain W3C validator