New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  mpbird GIF 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-1 5  ax-2 6  ax-3 7  ax-mp 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