ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbir Unicode version

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

Proof of Theorem mpbir
StepHypRef Expression
1 mpbir.min . 2  |-  ps
2 mpbir.maj . . 3  |-  ( ph  <->  ps )
32biimpri 132 . 2  |-  ( ps 
->  ph )
41, 3ax-mp 5 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.74ri  180  imnani  665  stabnot  803  mpbir2an  911  mpbir3an  1148  tru  1320  mpgbir  1414  nfxfr  1435  19.8a  1554  sbt  1742  dveeq2  1771  dveeq2or  1772  sbequilem  1794  cbvex2  1874  dvelimALT  1963  dvelimfv  1964  dvelimor  1971  nfeuv  1995  moaneu  2053  moanmo  2054  eqeltri  2190  nfcxfr  2255  neir  2288  neirr  2294  eqnetri  2308  nesymir  2332  nelir  2383  mprgbir  2467  vex  2663  issetri  2669  moeq  2832  cdeqi  2867  ru  2881  eqsstri  3099  3sstr4i  3108  rgenm  3435  mosn  3530  rabrsndc  3561  tpid1  3604  tpid2  3606  tpid3  3609  pwv  3705  uni0  3733  eqbrtri  3919  tr0  4007  trv  4008  zfnuleu  4022  0ex  4025  inex1  4032  0elpw  4058  axpow2  4070  axpow3  4071  vpwex  4073  zfpair2  4102  exss  4119  moop2  4143  pwundifss  4177  po0  4203  epse  4234  fr0  4243  0elon  4284  onm  4293  uniex2  4328  snnex  4339  ordtriexmidlem  4405  ordtriexmid  4407  ontr2exmid  4410  ordtri2or2exmidlem  4411  onsucsssucexmid  4412  onsucelsucexmidlem  4414  ruALT  4436  zfregfr  4458  dcextest  4465  zfinf2  4473  omex  4477  finds  4484  finds2  4485  ordom  4490  omsinds  4505  relsnop  4615  relxp  4618  rel0  4634  relopabi  4635  eliunxp  4648  opeliunxp2  4649  dmi  4724  xpidtr  4899  cnvcnv  4961  dmsn0  4976  cnvsn0  4977  funmpt  5131  funmpt2  5132  funinsn  5142  isarep2  5180  f0  5283  f10  5369  f1o00  5370  f1oi  5373  f1osn  5375  brprcneu  5382  fvopab3ig  5463  opabex  5612  eufnfv  5616  mpofun  5841  reldmmpo  5850  ovid  5855  ovidig  5856  ovidi  5857  ovig  5860  ovi3  5875  oprabex  5994  oprabex3  5995  f1stres  6025  f2ndres  6026  opeliunxp2f  6103  tpos0  6139  issmo  6153  tfrlem6  6181  tfrlem8  6183  tfri1dALT  6216  tfrcl  6229  rdgfun  6238  frecfun  6260  frecfcllem  6269  0lt1o  6305  eqer  6429  ecopover  6495  ecopoverg  6498  th3qcor  6501  mapsnf1o3  6559  ssdomg  6640  ensn1  6658  xpcomf1o  6687  fiunsnnn  6743  finexdc  6764  exmidpw  6770  omct  6970  infnninf  6990  nnnninf  6991  pm54.43  7014  exmidonfinlem  7017  dmaddpi  7101  dmmulpi  7102  1lt2pi  7116  indpi  7118  1lt2nq  7182  genpelxp  7287  ltexprlempr  7384  recexprlempr  7408  cauappcvgprlemcl  7429  cauappcvgprlemladd  7434  caucvgprlemcl  7452  caucvgprprlemcl  7480  m1p1sr  7536  m1m1sr  7537  0lt1sr  7541  peano1nnnn  7628  ax1cn  7637  ax1re  7638  axaddf  7644  axmulf  7645  ax0lt1  7652  0lt1  7857  subaddrii  8019  ixi  8312  1ap0  8319  sup3exmid  8679  nn1suc  8703  neg1lt0  8792  4d2e2  8838  iap0  8901  un0mulcl  8969  pnf0xnn0  9005  3halfnz  9106  nummac  9184  uzf  9285  mnfltpnf  9526  ixxf  9636  ioof  9709  fzf  9749  fzp1disj  9815  fzp1nel  9839  fzo0  9900  frecfzennn  10154  frechashgf1o  10156  fxnn0nninf  10166  seq3f1olemp  10230  sq0  10338  irec  10347  hash0  10498  prhash2ex  10510  climmo  11022  sum0  11112  fisumcom2  11162  cos1bnd  11380  cos2bnd  11381  n2dvdsm1  11522  n2dvds3  11524  flodddiv4  11543  3lcm2e6woprm  11679  6lcm4e12  11680  2prm  11720  3lcm2e6  11750  unennn  11821  structcnvcnv  11886  strleun  11959  restid  12042  tgdom  12152  tgidm  12154  resttopon  12251  rest0  12259  psmetrel  12402  metrel  12422  xmetrel  12423  xmetf  12430  0met  12464  mopnrel  12521  setsmsbasg  12559  setsmsdsg  12560  qtopbasss  12601  reldvg  12728  dvexp  12755  dveflem  12766  efcn  12768  sinhalfpilem  12783  sincosq1lem  12817  ex-fl  12833  bj-nndcALT  12859  bj-axempty  12987  bj-axempty2  12988  bdinex1  12993  bj-zfpair2  13004  bj-uniex2  13010  bj-indint  13025  bj-omind  13028  bj-omex  13036  bj-omelon  13055  pw1dom2  13086  0nninf  13093
  Copyright terms: Public domain W3C validator