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

Theorem mpbird 166
Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbird.min (𝜑𝜒)
mpbird.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpbird (𝜑𝜓)

Proof of Theorem mpbird
StepHypRef Expression
1 mpbird.min . 2 (𝜑𝜒)
2 mpbird.maj . . 3 (𝜑 → (𝜓𝜒))
32biimprd 157 . 2 (𝜑 → (𝜒𝜓))
41, 3mpd 13 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  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:  mpbiri  167  pm5.19  680  mpbir2and  913  pm3.12dc  927  mpbir3and  1149  pm5.15dc  1352  eqeltrd  2194  eqnetrd  2309  3netr4d  2318  sbcne12g  2991  eqsstrd  3103  3sstr4d  3112  eqbrtrd  3920  3brtr4d  3930  snelpwi  4104  prelpwi  4106  pwel  4110  ordelon  4275  onin  4278  elelsuc  4301  suceloni  4387  sucelon  4389  onintonm  4403  omsinds  4505  sosng  4582  relssdv  4601  eqbrrdv  4606  eqrelrdv2  4608  relsnopg  4613  breldmg  4715  elrnmptdv  4763  iss  4835  xpimasn  4957  elxp4  4996  elxp5  4997  funssres  5135  f0rn0  5287  sefvex  5410  fvun1  5455  eqfnfvd  5489  fvimacnvi  5502  fvimacnv  5503  fvelrn  5519  fmpt3d  5544  fmpt2d  5550  resflem  5552  fmptco  5554  fsn  5560  ftpg  5572  fconst2g  5603  funfvima3  5619  foeqcnvco  5659  f1eqcocnv  5660  fliftfun  5665  fliftfund  5666  fliftval  5669  riota5f  5722  f1ofveu  5730  f1ocnvd  5940  f1opw2  5944  off  5962  offval2  5965  ofrfval2  5966  caofref  5971  caofinvl  5972  elxp6  6035  cnvf1olem  6089  f2ndf  6091  f1od2  6100  tposf12  6134  smores2  6159  tfrlemisucaccv  6190  tfrlemibfn  6193  tfr1onlemsucaccv  6206  tfr1onlembfn  6209  tfrcllemsucaccv  6219  tfrcllembfn  6222  tfrcl  6229  tfri3  6232  frecabcl  6264  nnsucsssuc  6356  ersym  6409  ertr  6412  swoer  6425  erth  6441  riinerm  6470  qliftfund  6480  eroprf  6490  ecopoverg  6498  th3qlem1  6499  elmapssres  6535  mapss  6553  fdiagfn  6554  ixpssmap2g  6589  mapsnf1o  6599  f1dom2g  6618  dom3d  6636  fopwdom  6698  mapxpen  6710  nndomo  6726  dif1en  6741  findcard2  6751  findcard2s  6752  diffisn  6755  fimax2gtrilemstep  6762  fientri3  6771  fiintim  6785  f1dmvrnfibi  6800  sbthlemi6  6818  elfir  6829  fifo  6836  supelti  6857  supsnti  6860  cnvinfex  6873  ordiso2  6888  updjud  6935  djudom  6946  difinfsn  6953  ctssdc  6966  enumctlemm  6967  enumct  6968  enomnilem  6978  fodjuf  6985  ismkvnex  6997  omnimkv  6998  isnumi  7006  exmidfodomrlemrALT  7027  djudoml  7043  djudomr  7044  ltsopi  7096  pitri3or  7098  ltdcpi  7099  indpi  7118  enqdc  7137  enqdc1  7138  addcmpblnq  7143  mulcanenq  7161  recrecnq  7170  nqtri3or  7172  ltdcnq  7173  ltsonq  7174  ltaddnq  7183  subhalfnqq  7190  archnqq  7193  prarloclemarch2  7195  enq0tr  7210  nqnq0  7217  addcmpblnq0  7219  mulcanenq0ec  7221  nnnq0lem1  7222  nqpnq0nq  7229  nq0m0r  7232  nq02m  7241  prarloclemlt  7269  prarloclemcalc  7278  addlocpr  7312  nqprl  7327  nqpru  7328  addnqprlemrl  7333  addnqprlemru  7334  prmuloclemcalc  7341  mullocprlem  7346  mulnqprlemrl  7349  mulnqprlemru  7350  1idprl  7366  1idpru  7367  ltaddpr  7373  ltexprlemm  7376  ltexprlemopl  7377  ltexprlemopu  7379  ltexprlemdisj  7382  ltexprlemrl  7386  ltexprlemru  7388  addcanprleml  7390  addcanprlemu  7391  addcanprg  7392  prplnqu  7396  recexprlemloc  7407  recexprlem1ssl  7409  recexprlem1ssu  7410  aptiprleml  7415  aptiprlemu  7416  archpr  7419  cauappcvgprlemm  7421  cauappcvgprlemopl  7422  cauappcvgprlemloc  7428  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  cauappcvgprlem1  7435  cauappcvgprlem2  7436  caucvgprlemnkj  7442  caucvgprlemopl  7445  caucvgprlemloc  7451  caucvgprlemladdfu  7453  caucvgprlem2  7456  caucvgprprlemnkltj  7465  caucvgprprlemopl  7473  caucvgprprlemloc  7479  caucvgprprlemexbt  7482  caucvgprprlemaddq  7484  caucvgprprlem2  7486  suplocexprlemmu  7494  suplocexprlemru  7495  suplocexprlemloc  7497  suplocexprlemlub  7500  prsrlem1  7518  0idsr  7543  1idsr  7544  recexgt0sr  7549  archsr  7558  prsradd  7562  caucvgsrlemcau  7569  caucvgsrlembound  7570  caucvgsrlemoffgt1  7575  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  pitonnlem1p1  7622  pitonn  7624  pitoregt0  7625  peano2nnnn  7629  recidpirq  7634  axcaucvglemval  7673  leid  7816  nltled  7851  readdcan  7870  addneintrd  7918  addneintr2d  7919  pncan  7936  subsub2  7958  subsub4  7963  negned  8038  subne0d  8050  subneintrd  8085  subneintr2d  8087  subeq0bd  8109  subdi  8115  gt0add  8302  rimul  8314  rereim  8315  ltmul1a  8320  apreim  8332  apirr  8334  mulap0r  8344  msqge0  8345  mulge0  8348  gt0ap0  8355  ltap  8362  recexaplem2  8380  mulap0bad  8387  mulap0bbd  8388  mul0eqap  8398  divrecap  8415  div0ap  8429  div1  8430  recrecap  8436  divdivdivap  8440  ddcanap  8453  rerecclap  8457  div2negap  8462  diveqap1bd  8562  recgt0  8572  prodgt0  8574  lemul1a  8580  recp1lt1  8621  squeeze0  8626  peano2nn  8696  div4p1lem1div2  8931  arch  8932  peano2z  9048  peano2zm  9050  ztri3or  9055  nn0n0n1ge2  9079  zextle  9100  gtndiv  9104  suprzclex  9107  nn0ind-raph  9126  uzid  9296  uzneg  9300  uztric  9303  uz11  9304  eluzp1l  9306  qdivcl  9391  irrmul  9395  rpnegap  9429  negelrpd  9431  ledivge1le  9468  mul2lt0rlt0  9501  mul2lt0rgt0  9502  nn0ledivnn  9509  ltpnf  9522  mnflt  9524  pnfge  9530  mnfle  9533  xrlttr  9536  xrltso  9537  xrlttri3  9538  xrleid  9541  xaddass2  9608  xltadd1  9614  xlt2add  9618  xleaddadd  9625  iccf1o  9742  fztri3or  9774  fznlem  9776  fzn  9777  fzsplit2  9785  fznatpl1  9811  uzsplit  9827  fseq1p1m1  9829  fzm1  9835  fznn0sub2  9860  difelfznle  9867  1fv  9871  fzodcel  9884  fzospliti  9908  fzouzsplit  9911  eluzgtdifelfzo  9929  exfzdc  9972  subfzo0  9974  exbtwnz  9983  qbtwnrelemcalc  9988  flqlelt  10004  qfraclt1  10008  qfracge0  10009  flqltnz  10015  btwnzge0  10028  flhalf  10030  ceiqle  10041  intfracq  10048  mulqmod0  10058  modqge0  10060  modqlt  10061  modqid  10077  modqid0  10078  m1modge3gt1  10099  modqltm1p1mod  10104  q2txmodxeq0  10112  modaddmodlo  10116  modsumfzodifsn  10124  addmodlteq  10126  frecuzrdgtcl  10140  frecuzrdgtclt  10149  uzennn  10164  uzsinds  10170  seqf  10189  seqf2  10192  monoord2  10205  iseqf1olemqk  10222  iseqf1olemjpcl  10223  iseqf1olemqpcl  10224  seq3f1olemqsumkj  10226  seq3f1olemqsum  10228  seq3f1olemstep  10229  seq3f1oleml  10231  ser3le  10246  exp3vallem  10249  exp3val  10250  expp1  10255  expcllem  10259  ltexp2a  10300  leexp2a  10301  faclbnd  10442  faclbnd2  10443  faclbnd3  10444  bcval5  10464  bcpasc  10467  hashennn  10481  fihasheqf1oi  10489  hashsng  10499  fihashfn  10501  hashun  10506  fihashss  10517  fihashssdif  10519  hashfz  10522  hashxp  10527  fimaxq  10528  zfz1isolem1  10538  seq3coll  10540  shftfn  10551  cjth  10573  cjmulrcl  10614  reim0bd  10671  rerebd  10672  cjrebd  10673  caucvgre  10708  cvg1nlemcxze  10709  cvg1nlemcau  10711  cvg1nlemres  10712  recvguniq  10722  resqrexlemover  10737  resqrexlemdec  10738  resqrexlemgt0  10747  resqrexlemoverl  10748  resqrexlemglsq  10749  rersqrtthlem  10757  sqrtgt0  10761  leabs  10801  absexpzap  10807  absle  10816  recvalap  10824  abstri  10831  abs2dif  10833  amgm2  10845  absne0d  10914  maxleim  10932  maxabslemab  10933  maxabslemlub  10934  maxltsup  10945  zmaxcl  10951  fimaxre2  10953  minmax  10956  rpmincl  10964  bdtrilem  10965  bdtri  10966  xrmaxleim  10968  xrmaxiflemcom  10973  xrmaxltsup  10982  xrmaxadd  10985  xrminmax  10989  xrminrpcl  10998  climconst  11014  climuni  11017  2clim  11025  climcn1  11032  climcn2  11033  reccn2ap  11037  climge0  11049  climle  11058  climsqz  11059  climsqz2  11060  serf0  11076  summodclem3  11104  summodclem2a  11105  fsumcl2lem  11122  sumpr  11137  sumtp  11138  fsum0diaglem  11164  mptfzshft  11166  fsumle  11187  fsumlt  11188  divcnv  11221  trireciplem  11224  expcnvap0  11226  expcnv  11228  explecnv  11229  geosergap  11230  cvgratnnlembern  11247  cvgratnnlemabsle  11251  cvgratnnlemsumlt  11252  cvgratz  11256  cvgratgt0  11257  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  eftcl  11274  ef0lem  11280  efsub  11301  eftlub  11310  eflegeo  11322  tanval2ap  11334  sinadd  11357  cos2t  11371  cos2tsin  11372  sin01bnd  11378  cos01bnd  11379  eirraplem  11395  dvdsval2  11408  dvdsdc  11413  dvds0lem  11415  zdvdsdc  11426  dvdscmulr  11434  dvdsmulcr  11435  dvdslelemd  11453  divconjdvds  11459  dvdsext  11465  fzm1ndvds  11466  dvdsmod  11472  oexpneg  11486  2tp1odd  11493  mulsucdiv2z  11494  2teven  11496  zeo5  11497  opeo  11506  omeo  11507  nn0ob  11517  divalglemnqt  11529  zsupcllemstep  11550  zsupcl  11552  zssinfcl  11553  infssuzex  11554  infssuzcldc  11556  gcddvds  11564  dvdslegcd  11565  gcdneg  11582  bezoutlemnewy  11596  bezoutlemstep  11597  bezoutlema  11599  bezoutlemb  11600  bezoutlemmo  11606  bezoutlemle  11608  bezoutlemsup  11609  dfgcd3  11610  bezout  11611  dfgcd2  11614  lcmcllem  11660  lcmneg  11667  lcmgcdlem  11670  lcmdvds  11672  lcmid  11673  3lcm2e6woprm  11679  6lcm4e12  11680  ncoprmgcdne1b  11682  mulgcddvds  11687  divgcdcoprmex  11695  cncongr1  11696  cncongr2  11697  isprm2lem  11709  prmind2  11713  dvdsnprmd  11718  prm2orodd  11719  sqnprm  11728  rpexp  11743  sqrt2irrlem  11751  oddpwdclemdc  11762  sqrt2irraplemnn  11768  qnumdencoprm  11782  qeqnumdivden  11783  nn0gcdsq  11789  nn0sqrtelqelz  11795  nonsq  11796  phicl2  11801  phibnd  11804  hashdvds  11808  phiprmpw  11809  phimullem  11812  hashgcdlem  11814  znnen  11822  ennnfonelemk  11824  ennnfonelemkh  11836  ennnfonelemhf1o  11837  ennnfonelemrnh  11840  ennnfonelemfun  11841  ennnfonelemf1  11842  ennnfonelemrn  11843  ennnfonelemnn0  11846  ctinfomlemom  11851  ctiunctlemudc  11861  unct  11865  structfung  11887  setsfun  11905  setsfun0  11906  setscom  11910  setsslid  11920  baspartn  12128  eltg3i  12136  tgclb  12145  topbas  12147  2basgeng  12162  topcld  12189  0cld  12192  uncld  12193  neif  12221  elnei  12232  0nei  12246  restbasg  12248  iscnp4  12298  cnpnei  12299  cnclima  12303  cncnp  12310  cnrest2r  12317  cndis  12321  lmff  12329  lmtopcnp  12330  txbas  12338  txopn  12345  txcnp  12351  upxp  12352  txdis1cn  12358  cnmpt11  12363  cnmpt21  12371  psmetge0  12411  xmetge0  12445  xmettpos  12450  xmetrtri  12456  metrtri  12457  xblpnfps  12478  xblpnf  12479  blfps  12489  blf  12490  ssblps  12505  ssbl  12506  blbas  12513  metss2  12578  xmettxlem  12589  xmettx  12590  qtopbas  12602  divcnap  12635  cncfss  12650  cdivcncfap  12667  expcncf  12672  cnopnap  12674  dedekindeulemuub  12675  dedekindeulemlu  12679  dedekindeu  12681  suplociccex  12683  dedekindicclemuub  12684  dedekindicclemlu  12688  dedekindicclemicc  12690  ivthinclemlopn  12694  ivthinclemuopn  12696  ivthinc  12701  ellimc3apf  12709  limcimolemlt  12713  limcimo  12714  limcresi  12715  cnplimclemle  12717  reldvg  12728  dvfgg  12737  dvidlemap  12740  dvcjbr  12752  dvcj  12753  dvrecap  12757  dveflem  12766  dvef  12767  pilem3  12775  sinq34lt0t  12823  cosq14gt0  12824  coseq0q4123  12826  bj-sels  13008  bj-nnelon  13053  pwle2  13089  pwf1oexmid  13090  nninfall  13100  nninfsellemdc  13102  nninfself  13105  refeq  13119  isomninnlem  13121  cvgcmp2nlemabs  13123  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator