ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbir GIF 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 𝜓
mpbir.maj (𝜑𝜓)
Assertion
Ref Expression
mpbir 𝜑

Proof of Theorem mpbir
StepHypRef Expression
1 mpbir.min . 2 𝜓
2 mpbir.maj . . 3 (𝜑𝜓)
32biimpri 131 . 2 (𝜓𝜑)
41, 3ax-mp 7 1 𝜑
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  658  stabnot  776  mpbir2an  886  mpbir3an  1123  tru  1291  mpgbir  1385  nfxfr  1406  19.8a  1525  sbt  1711  dveeq2  1740  dveeq2or  1741  sbequilem  1763  cbvex2  1842  dvelimALT  1931  dvelimfv  1932  dvelimor  1939  nfeuv  1963  moaneu  2021  moanmo  2022  eqeltri  2157  nfcxfr  2222  neir  2254  neirr  2260  eqnetri  2274  nesymir  2298  nelir  2349  mprgbir  2429  vex  2618  issetri  2622  moeq  2781  cdeqi  2814  ru  2828  eqsstri  3045  3sstr4i  3054  rgenm  3371  mosn  3462  rabrsndc  3493  tpid1  3536  tpid2  3537  tpid3  3539  pwv  3635  uni0  3663  eqbrtri  3839  tr0  3922  trv  3923  zfnuleu  3938  0ex  3941  inex1  3948  0elpw  3974  axpow2  3986  axpow3  3987  vpwex  3989  zfpair2  4011  exss  4028  moop2  4052  pwundifss  4086  po0  4112  epse  4143  fr0  4152  0elon  4193  onm  4202  uniex2  4237  snnex  4245  ordtriexmidlem  4309  ordtriexmid  4311  ontr2exmid  4314  ordtri2or2exmidlem  4315  onsucsssucexmid  4316  onsucelsucexmidlem  4318  ruALT  4340  zfregfr  4362  dcextest  4369  zfinf2  4377  omex  4381  finds  4388  finds2  4389  ordom  4394  omsinds  4408  relsnop  4512  relxp  4515  rel0  4530  relopabi  4531  eliunxp  4543  opeliunxp2  4544  dmi  4619  xpidtr  4789  cnvcnv  4849  dmsn0  4864  cnvsn0  4865  funmpt  5017  funmpt2  5018  funinsn  5028  isarep2  5066  f0  5164  f10  5250  f1o00  5251  f1oi  5254  f1osn  5256  brprcneu  5261  fvopab3ig  5341  opabex  5482  eufnfv  5486  mpt2fun  5704  reldmmpt2  5713  ovid  5718  ovidig  5719  ovidi  5720  ovig  5723  ovi3  5738  oprabex  5856  oprabex3  5857  f1stres  5887  f2ndres  5888  tpos0  5993  issmo  6007  tfrlem6  6035  tfrlem8  6037  tfri1dALT  6070  tfrcl  6083  rdgfun  6092  frecfun  6114  frecfcllem  6123  0lt1o  6158  eqer  6276  ecopover  6342  ecopoverg  6345  th3qcor  6348  mapsnf1o3  6406  ssdomg  6447  ensn1  6465  xpcomf1o  6493  fiunsnnn  6549  finexdc  6570  exmidpw  6576  infnninf  6749  nnnninf  6750  pm54.43  6762  dmaddpi  6828  dmmulpi  6829  1lt2pi  6843  indpi  6845  1lt2nq  6909  genpelxp  7014  ltexprlempr  7111  recexprlempr  7135  cauappcvgprlemcl  7156  cauappcvgprlemladd  7161  caucvgprlemcl  7179  caucvgprprlemcl  7207  m1p1sr  7250  m1m1sr  7251  0lt1sr  7255  peano1nnnn  7333  ax1cn  7342  ax1re  7343  ax0lt1  7355  0lt1  7554  subaddrii  7715  ixi  8001  1ap0  8008  nn1suc  8376  neg1lt0  8465  4d2e2  8510  iap0  8572  un0mulcl  8640  pnf0xnn0  8676  3halfnz  8776  nummac  8853  uzf  8954  mnfltpnf  9187  ixxf  9248  ioof  9321  fzf  9360  fzp1disj  9424  fzp1nel  9448  fzo0  9507  frecfzennn  9761  frechashgf1o  9763  fxnn0nninf  9772  iseqf1olemp  9835  sq0  9943  irec  9951  hash0  10101  prhash2ex  10113  climmo  10579  sum0  10666  n2dvdsm1  10788  n2dvds3  10790  flodddiv4  10809  3lcm2e6woprm  10943  6lcm4e12  10944  2prm  10984  3lcm2e6  11014  unennn  11085  ex-fl  11091  bj-axempty  11222  bj-axempty2  11223  bdinex1  11228  bj-zfpair2  11239  bj-uniex2  11245  bj-indint  11264  bj-omind  11267  bj-omex  11275  bj-omelon  11294  pw1dom2  11327  0nninf  11331
  Copyright terms: Public domain W3C validator