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

Theorem mpbir 144
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 131 . 2  |-  ( ps 
->  ph )
41, 3ax-mp 7 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.74ri  179  imnani  660  stabnot  778  mpbir2an  888  mpbir3an  1125  tru  1293  mpgbir  1387  nfxfr  1408  19.8a  1527  sbt  1714  dveeq2  1743  dveeq2or  1744  sbequilem  1766  cbvex2  1845  dvelimALT  1934  dvelimfv  1935  dvelimor  1942  nfeuv  1966  moaneu  2024  moanmo  2025  eqeltri  2160  nfcxfr  2225  neir  2258  neirr  2264  eqnetri  2278  nesymir  2302  nelir  2353  mprgbir  2433  vex  2622  issetri  2628  moeq  2788  cdeqi  2823  ru  2837  eqsstri  3054  3sstr4i  3063  rgenm  3380  mosn  3474  rabrsndc  3505  tpid1  3548  tpid2  3549  tpid3  3551  pwv  3647  uni0  3675  eqbrtri  3856  tr0  3939  trv  3940  zfnuleu  3955  0ex  3958  inex1  3965  0elpw  3991  axpow2  4003  axpow3  4004  vpwex  4006  zfpair2  4028  exss  4045  moop2  4069  pwundifss  4103  po0  4129  epse  4160  fr0  4169  0elon  4210  onm  4219  uniex2  4254  snnex  4262  ordtriexmidlem  4326  ordtriexmid  4328  ontr2exmid  4331  ordtri2or2exmidlem  4332  onsucsssucexmid  4333  onsucelsucexmidlem  4335  ruALT  4357  zfregfr  4379  dcextest  4386  zfinf2  4394  omex  4398  finds  4405  finds2  4406  ordom  4411  omsinds  4425  relsnop  4532  relxp  4535  rel0  4550  relopabi  4551  eliunxp  4563  opeliunxp2  4564  dmi  4639  xpidtr  4809  cnvcnv  4870  dmsn0  4885  cnvsn0  4886  funmpt  5038  funmpt2  5039  funinsn  5049  isarep2  5087  f0  5185  f10  5271  f1o00  5272  f1oi  5275  f1osn  5277  brprcneu  5282  fvopab3ig  5362  opabex  5503  eufnfv  5507  mpt2fun  5729  reldmmpt2  5738  ovid  5743  ovidig  5744  ovidi  5745  ovig  5748  ovi3  5763  oprabex  5881  oprabex3  5882  f1stres  5912  f2ndres  5913  opeliunxp2f  5985  tpos0  6021  issmo  6035  tfrlem6  6063  tfrlem8  6065  tfri1dALT  6098  tfrcl  6111  rdgfun  6120  frecfun  6142  frecfcllem  6151  0lt1o  6186  eqer  6304  ecopover  6370  ecopoverg  6373  th3qcor  6376  mapsnf1o3  6434  ssdomg  6475  ensn1  6493  xpcomf1o  6521  fiunsnnn  6577  finexdc  6598  exmidpw  6604  infnninf  6784  nnnninf  6785  pm54.43  6797  dmaddpi  6863  dmmulpi  6864  1lt2pi  6878  indpi  6880  1lt2nq  6944  genpelxp  7049  ltexprlempr  7146  recexprlempr  7170  cauappcvgprlemcl  7191  cauappcvgprlemladd  7196  caucvgprlemcl  7214  caucvgprprlemcl  7242  m1p1sr  7285  m1m1sr  7286  0lt1sr  7290  peano1nnnn  7368  ax1cn  7377  ax1re  7378  ax0lt1  7390  0lt1  7589  subaddrii  7750  ixi  8036  1ap0  8043  nn1suc  8413  neg1lt0  8501  4d2e2  8546  iap0  8609  un0mulcl  8677  pnf0xnn0  8713  3halfnz  8813  nummac  8890  uzf  8991  mnfltpnf  9224  ixxf  9285  ioof  9358  fzf  9397  fzp1disj  9461  fzp1nel  9485  fzo0  9544  frecfzennn  9798  frechashgf1o  9800  fxnn0nninf  9809  seq3f1olemp  9896  sq0  10010  irec  10019  hash0  10170  prhash2ex  10182  climmo  10650  sum0  10744  fisumcom2  10795  n2dvdsm1  11006  n2dvds3  11008  flodddiv4  11027  3lcm2e6woprm  11161  6lcm4e12  11162  2prm  11202  3lcm2e6  11232  unennn  11303  ex-fl  11309  bj-axempty  11441  bj-axempty2  11442  bdinex1  11447  bj-zfpair2  11458  bj-uniex2  11464  bj-indint  11483  bj-omind  11486  bj-omex  11494  bj-omelon  11513  pw1dom2  11546  0nninf  11550
  Copyright terms: Public domain W3C validator