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

Theorem mpbir 200
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbir.min
mpbir.maj
Assertion
Ref Expression
mpbir

Proof of Theorem mpbir
StepHypRef Expression
1 mpbir.min . 2
2 mpbir.maj . . 3
32biimpri 197 . 2
41, 3ax-mp 8 1
Colors of variables: wff set class
Syntax hints:   wb 176
This theorem is referenced by:  pm5.74ri  237  con4bii  288  orri  365  imorri  403  imnani  412  mpbir2an  886  mpbir3an  1134  tru  1321  nic-mpALT  1437  nic-ax  1438  nic-axALT  1439  mpto2OLD  1535  mtp-xor  1536  mtp-xorOLD  1537  mpgbir  1550  nfxfr  1570  19.35ri  1602  a9ev  1656  exiftruOLD  1658  a9e  1951  cbval2  2004  cbvex2  2005  sbt  2033  moaneu  2263  moanmo  2264  axi12  2333  axext2  2335  eqeltri  2423  nfcxfr  2486  neirr  2521  exmidne  2522  eqnetri  2533  mprgbir  2684  vex  2862  issetri  2866  moeq  3012  ru  3045  eqsstri  3301  3sstr4i  3310  necompl  3544  tpid1  3829  tpid2  3830  tpid3  3832  pwv  3886  uni0  3918  nincompl  4072  ninexg  4097  snex  4111  opkth1g  4130  snel1c  4140  1cex  4142  0nel1c  4159  opkabssvvk  4208  eqrelkriiv  4213  sikss1c1c  4267  ins2kss  4279  ins3kss  4280  xpkvexg  4285  ins2kexg  4305  ins3kexg  4306  0cnsuc  4401  finds  4410  nulel0c  4421  0fin  4422  nnsucelr  4427  vfin1cltv  4547  eqbrtri  4650  relsnop  4852  relxp  4855  rel0  4869  relopabi  4870  dmi  4931  cnvcnv  5081  dfcnv2  5133  nfunv  5172  funsn  5181  f10  5356  f1o00  5357  f1oi  5360  f1osn  5362  fvopab3ig  5427  fnasrn  5457  1stfo  5546  2ndfo  5547  swapf1o  5552  opfv1st  5555  opfv2nd  5556  ovidig  5635  ovidi  5636  ovig  5639  ov3  5641  funmpt  5727  reldmmpt2  5757  relmptopab  5766  reltxp  5814  op1st2nd  5819  fncup  5845  addcfn  5853  relpprod  5863  fncross  5873  fnfullfun  5884  fvfullfunlem2  5888  ssetpov  5964  fnmap  6027  fnpm  6028  xpassen  6077  enprmaplem5  6100  enpw  6107  muccom  6155  mucass  6156  1cnc  6160  df1c3  6161  mucid1  6164  ncaddccl  6165  ncpwpw1  6174  1p1e2c  6176  2p1e3c  6177  tcdi  6185  fnce  6197  ce0addcnnul  6200  ce0nulnc  6205  fce  6209  ce2  6213  tlenc1c  6260  nchoicelem9  6297
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
  Copyright terms: Public domain W3C validator