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

Theorem mpbir 146
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 133 . 2 (𝜓𝜑)
41, 3ax-mp 5 1 𝜑
Colors of variables: wff set class
Syntax hints:  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm5.74ri  181  imnani  691  stabnot  833  mpbir2an  942  mpbir3an  1179  tru  1357  mpgbir  1453  nfxfr  1474  19.8a  1590  sbt  1784  dveeq2  1815  dveeq2or  1816  sbequilem  1838  cbvex2  1922  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  nfeuv  2044  moaneu  2102  moanmo  2103  eqeltri  2250  nfcxfr  2316  neir  2350  neirr  2356  eqnetri  2370  nesymir  2394  nelir  2445  mprgbir  2535  vex  2740  issetri  2746  moeq  2912  cdeqi  2947  ru  2961  eqsstri  3187  3sstr4i  3196  rgenm  3525  mosn  3627  rabrsndc  3659  tpid1  3702  tpid2  3704  tpid3  3707  pwv  3806  uni0  3834  eqbrtri  4021  tr0  4109  trv  4110  zfnuleu  4124  0ex  4127  inex1  4134  elpwi2  4155  0elpw  4161  axpow2  4173  axpow3  4174  vpwex  4176  zfpair2  4206  exss  4223  moop2  4247  pwundifss  4281  po0  4307  epse  4338  fr0  4347  0elon  4388  onm  4397  uniex2  4432  snnex  4444  ordtriexmidlem  4514  ordtriexmid  4516  ontr2exmid  4520  ordtri2or2exmidlem  4521  onsucsssucexmid  4522  onsucelsucexmidlem  4524  ruALT  4546  zfregfr  4569  dcextest  4576  zfinf2  4584  omex  4588  finds  4595  finds2  4596  ordom  4602  omsinds  4617  relsnop  4728  relxp  4731  rel0  4747  relopabi  4748  eliunxp  4761  opeliunxp2  4762  dmi  4837  xpidtr  5014  cnvcnv  5076  dmsn0  5091  cnvsn0  5092  funmpt  5249  funmpt2  5250  funinsn  5260  isarep2  5298  f0  5401  f10  5490  f1o00  5491  f1oi  5494  f1osn  5496  brprcneu  5503  fvopab3ig  5585  opabex  5735  eufnfv  5741  mpofun  5970  reldmmpo  5979  ovid  5984  ovidig  5985  ovidi  5986  ovig  5989  ovi3  6004  oprabex  6122  oprabex3  6123  f1stres  6153  f2ndres  6154  opeliunxp2f  6232  tpos0  6268  issmo  6282  tfrlem6  6310  tfrlem8  6312  tfri1dALT  6345  tfrcl  6358  rdgfun  6367  frecfun  6389  frecfcllem  6398  0lt1o  6434  eqer  6560  ecopover  6626  ecopoverg  6629  th3qcor  6632  mapsnf1o3  6690  ssdomg  6771  ensn1  6789  xpcomf1o  6818  fiunsnnn  6874  finexdc  6895  exmidpw  6901  dcfi  6973  omct  7109  infnninf  7115  infnninfOLD  7116  pm54.43  7182  exmidonfinlem  7185  pw1on  7218  pw1dom2  7219  pw1ne1  7221  dmaddpi  7302  dmmulpi  7303  1lt2pi  7317  indpi  7319  1lt2nq  7383  genpelxp  7488  ltexprlempr  7585  recexprlempr  7609  cauappcvgprlemcl  7630  cauappcvgprlemladd  7635  caucvgprlemcl  7653  caucvgprprlemcl  7681  m1p1sr  7737  m1m1sr  7738  0lt1sr  7742  peano1nnnn  7829  ax1cn  7838  ax1re  7839  axaddf  7845  axmulf  7846  ax0lt1  7853  0lt1  8061  subaddrii  8223  ixi  8517  1ap0  8524  sup3exmid  8890  nn1suc  8914  neg1lt0  9003  4d2e2  9055  iap0  9118  un0mulcl  9186  pnf0xnn0  9222  3halfnz  9326  nummac  9404  uzf  9507  mnfltpnf  9759  ixxf  9872  ioof  9945  fzf  9986  fzp1disj  10053  fzp1nel  10077  fzo0  10141  frecfzennn  10399  frechashgf1o  10401  fxnn0nninf  10411  seq3f1olemp  10475  sq0  10583  irec  10592  hash0  10747  prhash2ex  10760  climmo  11277  sum0  11367  fisumcom2  11417  prod0  11564  fprodcom2fi  11605  cos1bnd  11738  cos2bnd  11739  n2dvdsm1  11888  n2dvds3  11890  flodddiv4  11909  3lcm2e6woprm  12056  6lcm4e12  12057  2prm  12097  3lcm2e6  12130  pockthi  12326  unennn  12368  ssnnctlemct  12417  structcnvcnv  12448  strleun  12532  scandxnbasendx  12574  scandxnplusgndx  12575  scandxnmulrndx  12576  tsetndxnplusgndx  12601  tsetndxnmulrndx  12602  tsetndxnstarvndx  12603  slotstnscsi  12604  dsndxnplusgndx  12618  dsndxnmulrndx  12619  slotsdnscsi  12620  dsndxntsetndx  12621  slotsdifdsndx  12622  restid  12634  mgmidmo  12670  tgdom  13205  tgidm  13207  resttopon  13304  rest0  13312  psmetrel  13455  metrel  13475  xmetrel  13476  xmetf  13483  0met  13517  mopnrel  13574  setsmsbasg  13612  setsmsdsg  13613  qtopbasss  13654  reldvg  13781  dvexp  13808  dveflem  13820  efcn  13822  sinhalfpilem  13845  sincosq1lem  13879  tangtx  13892  sincos4thpi  13894  pigt3  13898  dfrelog  13914  relogf1o  13915  log1  13920  loge  13921  relogiso  13927  2logb9irr  14022  2logb9irrap  14028  2sqlem9  14093  2sqlem10  14094  ex-fl  14099  bj-nndcALT  14132  bj-axempty  14267  bj-axempty2  14268  bdinex1  14273  bj-zfpair2  14284  bj-uniex2  14290  bj-indint  14305  bj-omind  14308  bj-omex  14316  bj-omelon  14335  0nninf  14376  dceqnconst  14430  dcapnconst  14431
  Copyright terms: Public domain W3C validator