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  695  mpbir2and  928  pm3.12dc  942  mpbir3and  1164  pm5.15dc  1367  eqeltrd  2216  eqnetrd  2332  3netr4d  2341  sbcne12g  3020  eqsstrd  3133  3sstr4d  3142  eqbrtrd  3950  3brtr4d  3960  snelpwi  4134  prelpwi  4136  pwel  4140  ordelon  4305  onin  4308  elelsuc  4331  suceloni  4417  sucelon  4419  onintonm  4433  omsinds  4535  sosng  4612  relssdv  4631  eqbrrdv  4636  eqrelrdv2  4638  relsnopg  4643  breldmg  4745  elrnmptdv  4793  iss  4865  xpimasn  4987  elxp4  5026  elxp5  5027  funssres  5165  f0rn0  5317  sefvex  5442  fvun1  5487  eqfnfvd  5521  fvimacnvi  5534  fvimacnv  5535  fvelrn  5551  fmpt3d  5576  fmpt2d  5582  resflem  5584  fmptco  5586  fsn  5592  ftpg  5604  fconst2g  5635  funfvima3  5651  foeqcnvco  5691  f1eqcocnv  5692  fliftfun  5697  fliftfund  5698  fliftval  5701  riota5f  5754  f1ofveu  5762  f1ocnvd  5972  f1opw2  5976  off  5994  offval2  5997  ofrfval2  5998  caofref  6003  caofinvl  6004  elxp6  6067  cnvf1olem  6121  f2ndf  6123  f1od2  6132  tposf12  6166  smores2  6191  tfrlemisucaccv  6222  tfrlemibfn  6225  tfr1onlemsucaccv  6238  tfr1onlembfn  6241  tfrcllemsucaccv  6251  tfrcllembfn  6254  tfrcl  6261  tfri3  6264  frecabcl  6296  nnsucsssuc  6388  ersym  6441  ertr  6444  swoer  6457  erth  6473  riinerm  6502  qliftfund  6512  eroprf  6522  ecopoverg  6530  th3qlem1  6531  elmapssres  6567  mapss  6585  fdiagfn  6586  ixpssmap2g  6621  mapsnf1o  6631  f1dom2g  6650  dom3d  6668  fopwdom  6730  mapxpen  6742  nndomo  6758  dif1en  6773  findcard2  6783  findcard2s  6784  diffisn  6787  fimax2gtrilemstep  6794  fientri3  6803  fiintim  6817  f1dmvrnfibi  6832  sbthlemi6  6850  elfir  6861  fifo  6868  supelti  6889  supsnti  6892  cnvinfex  6905  ordiso2  6920  updjud  6967  djudom  6978  difinfsn  6985  ctssdc  6998  enumctlemm  6999  enumct  7000  enomnilem  7010  fodjuf  7017  ismkvnex  7029  omnimkv  7030  enwomnilem  7040  isnumi  7045  exmidfodomrlemrALT  7066  djudoml  7082  djudomr  7083  cc2lem  7088  cc3  7090  ltsopi  7142  pitri3or  7144  ltdcpi  7145  indpi  7164  enqdc  7183  enqdc1  7184  addcmpblnq  7189  mulcanenq  7207  recrecnq  7216  nqtri3or  7218  ltdcnq  7219  ltsonq  7220  ltaddnq  7229  subhalfnqq  7236  archnqq  7239  prarloclemarch2  7241  enq0tr  7256  nqnq0  7263  addcmpblnq0  7265  mulcanenq0ec  7267  nnnq0lem1  7268  nqpnq0nq  7275  nq0m0r  7278  nq02m  7287  prarloclemlt  7315  prarloclemcalc  7324  addlocpr  7358  nqprl  7373  nqpru  7374  addnqprlemrl  7379  addnqprlemru  7380  prmuloclemcalc  7387  mullocprlem  7392  mulnqprlemrl  7395  mulnqprlemru  7396  1idprl  7412  1idpru  7413  ltaddpr  7419  ltexprlemm  7422  ltexprlemopl  7423  ltexprlemopu  7425  ltexprlemdisj  7428  ltexprlemrl  7432  ltexprlemru  7434  addcanprleml  7436  addcanprlemu  7437  addcanprg  7438  prplnqu  7442  recexprlemloc  7453  recexprlem1ssl  7455  recexprlem1ssu  7456  aptiprleml  7461  aptiprlemu  7462  archpr  7465  cauappcvgprlemm  7467  cauappcvgprlemopl  7468  cauappcvgprlemloc  7474  cauappcvgprlemladdfu  7476  cauappcvgprlemladdfl  7477  cauappcvgprlem1  7481  cauappcvgprlem2  7482  caucvgprlemnkj  7488  caucvgprlemopl  7491  caucvgprlemloc  7497  caucvgprlemladdfu  7499  caucvgprlem2  7502  caucvgprprlemnkltj  7511  caucvgprprlemopl  7519  caucvgprprlemloc  7525  caucvgprprlemexbt  7528  caucvgprprlemaddq  7530  caucvgprprlem2  7532  suplocexprlemmu  7540  suplocexprlemru  7541  suplocexprlemloc  7543  suplocexprlemlub  7546  prsrlem1  7564  0idsr  7589  1idsr  7590  recexgt0sr  7595  archsr  7604  prsradd  7608  caucvgsrlemcau  7615  caucvgsrlembound  7616  caucvgsrlemoffgt1  7621  suplocsrlemb  7628  suplocsrlempr  7629  suplocsrlem  7630  pitonnlem1p1  7668  pitonn  7670  pitoregt0  7671  peano2nnnn  7675  recidpirq  7680  axcaucvglemval  7719  leid  7862  nltled  7897  readdcan  7916  addneintrd  7964  addneintr2d  7965  pncan  7982  subsub2  8004  subsub4  8009  negned  8084  subne0d  8096  subneintrd  8131  subneintr2d  8133  subeq0bd  8155  subdi  8161  gt0add  8349  rimul  8361  rereim  8362  ltmul1a  8367  apreim  8379  apirr  8381  mulap0r  8391  msqge0  8392  mulge0  8395  gt0ap0  8402  ltap  8409  recexaplem2  8427  mulap0bad  8434  mulap0bbd  8435  mul0eqap  8445  divrecap  8462  div0ap  8476  div1  8477  recrecap  8483  divdivdivap  8487  ddcanap  8500  rerecclap  8504  div2negap  8509  diveqap1bd  8609  recgt0  8622  prodgt0  8624  lemul1a  8630  recp1lt1  8671  squeeze0  8676  peano2nn  8746  div4p1lem1div2  8987  arch  8988  peano2z  9104  peano2zm  9106  ztri3or  9111  nn0n0n1ge2  9135  zextle  9156  gtndiv  9160  suprzclex  9163  nn0ind-raph  9182  uzid  9354  uzneg  9358  uztric  9361  uz11  9362  eluzp1l  9364  qdivcl  9449  irrmul  9453  rpnegap  9488  negelrpd  9490  ledivge1le  9527  mul2lt0rlt0  9560  mul2lt0rgt0  9561  nn0ledivnn  9568  ltpnf  9581  mnflt  9583  pnfge  9589  mnfle  9592  xrlttr  9595  xrltso  9596  xrlttri3  9597  xrleid  9600  xaddass2  9667  xltadd1  9673  xlt2add  9677  xleaddadd  9684  iccf1o  9801  fztri3or  9833  fznlem  9835  fzn  9836  fzsplit2  9844  fznatpl1  9870  uzsplit  9886  fseq1p1m1  9888  fzm1  9894  fznn0sub2  9919  difelfznle  9926  1fv  9930  fzodcel  9943  fzospliti  9967  fzouzsplit  9970  eluzgtdifelfzo  9988  exfzdc  10031  subfzo0  10033  exbtwnz  10042  qbtwnrelemcalc  10047  flqlelt  10063  qfraclt1  10067  qfracge0  10068  flqltnz  10074  btwnzge0  10087  flhalf  10089  ceiqle  10100  intfracq  10107  mulqmod0  10117  modqge0  10119  modqlt  10120  modqid  10136  modqid0  10137  m1modge3gt1  10158  modqltm1p1mod  10163  q2txmodxeq0  10171  modaddmodlo  10175  modsumfzodifsn  10183  addmodlteq  10185  frecuzrdgtcl  10199  frecuzrdgtclt  10208  uzennn  10223  uzsinds  10229  seqf  10248  seqf2  10251  monoord2  10264  iseqf1olemqk  10281  iseqf1olemjpcl  10282  iseqf1olemqpcl  10283  seq3f1olemqsumkj  10285  seq3f1olemqsum  10287  seq3f1olemstep  10288  seq3f1oleml  10290  ser3le  10305  exp3vallem  10308  exp3val  10309  expp1  10314  expcllem  10318  ltexp2a  10359  leexp2a  10360  faclbnd  10501  faclbnd2  10502  faclbnd3  10503  bcval5  10523  bcpasc  10526  hashennn  10540  fihasheqf1oi  10548  hashsng  10558  fihashfn  10560  hashun  10565  fihashss  10576  fihashssdif  10578  hashfz  10581  hashxp  10586  fimaxq  10587  zfz1isolem1  10597  seq3coll  10599  shftfn  10610  cjth  10632  cjmulrcl  10673  reim0bd  10730  rerebd  10731  cjrebd  10732  caucvgre  10767  cvg1nlemcxze  10768  cvg1nlemcau  10770  cvg1nlemres  10771  recvguniq  10781  resqrexlemover  10796  resqrexlemdec  10797  resqrexlemgt0  10806  resqrexlemoverl  10807  resqrexlemglsq  10808  rersqrtthlem  10816  sqrtgt0  10820  leabs  10860  absexpzap  10866  absle  10875  recvalap  10883  abstri  10890  abs2dif  10892  amgm2  10904  absne0d  10973  maxleim  10991  maxabslemab  10992  maxabslemlub  10993  maxltsup  11004  zmaxcl  11010  fimaxre2  11012  minmax  11015  rpmincl  11023  bdtrilem  11024  bdtri  11025  xrmaxleim  11027  xrmaxiflemcom  11032  xrmaxltsup  11041  xrmaxadd  11044  xrminmax  11048  xrminrpcl  11057  climconst  11073  climuni  11076  2clim  11084  climcn1  11091  climcn2  11092  reccn2ap  11096  climge0  11108  climle  11117  climsqz  11118  climsqz2  11119  serf0  11135  summodclem3  11163  summodclem2a  11164  fsumcl2lem  11181  sumpr  11196  sumtp  11197  fsum0diaglem  11223  mptfzshft  11225  fsumle  11246  fsumlt  11247  divcnv  11280  trireciplem  11283  expcnvap0  11285  expcnv  11287  explecnv  11288  geosergap  11289  cvgratnnlembern  11306  cvgratnnlemabsle  11310  cvgratnnlemsumlt  11311  cvgratz  11315  cvgratgt0  11316  mertenslemi1  11318  mertenslem2  11319  mertensabs  11320  clim2divap  11323  prodmodclem3  11358  prodmodclem2a  11359  eftcl  11374  ef0lem  11380  efsub  11401  eftlub  11410  eflegeo  11421  tanval2ap  11433  sinadd  11456  cos2t  11470  cos2tsin  11471  sin01bnd  11477  cos01bnd  11478  eirraplem  11496  dvdsval2  11509  dvdsdc  11514  dvds0lem  11516  zdvdsdc  11527  dvdscmulr  11535  dvdsmulcr  11536  dvdslelemd  11554  divconjdvds  11560  dvdsext  11566  fzm1ndvds  11567  dvdsmod  11573  oexpneg  11587  2tp1odd  11594  mulsucdiv2z  11595  2teven  11597  zeo5  11598  opeo  11607  omeo  11608  nn0ob  11618  divalglemnqt  11630  zsupcllemstep  11651  zsupcl  11653  zssinfcl  11654  infssuzex  11655  infssuzcldc  11657  gcddvds  11665  dvdslegcd  11666  gcdneg  11683  bezoutlemnewy  11697  bezoutlemstep  11698  bezoutlema  11700  bezoutlemb  11701  bezoutlemmo  11707  bezoutlemle  11709  bezoutlemsup  11710  dfgcd3  11711  bezout  11712  dfgcd2  11715  lcmcllem  11761  lcmneg  11768  lcmgcdlem  11771  lcmdvds  11773  lcmid  11774  3lcm2e6woprm  11780  6lcm4e12  11781  ncoprmgcdne1b  11783  mulgcddvds  11788  divgcdcoprmex  11796  cncongr1  11797  cncongr2  11798  isprm2lem  11810  prmind2  11814  dvdsnprmd  11819  prm2orodd  11820  sqnprm  11829  rpexp  11844  sqrt2irrlem  11852  oddpwdclemdc  11864  sqrt2irraplemnn  11870  qnumdencoprm  11884  qeqnumdivden  11885  nn0gcdsq  11891  nn0sqrtelqelz  11897  nonsq  11898  phicl2  11903  phibnd  11906  hashdvds  11910  phiprmpw  11911  phimullem  11914  hashgcdlem  11916  znnen  11924  ennnfonelemk  11926  ennnfonelemkh  11938  ennnfonelemhf1o  11939  ennnfonelemrnh  11942  ennnfonelemfun  11943  ennnfonelemf1  11944  ennnfonelemrn  11945  ennnfonelemnn0  11948  ctinfomlemom  11953  ctiunctlemudc  11963  unct  11968  omctfn  11969  structfung  11992  setsfun  12010  setsfun0  12011  setscom  12015  setsslid  12025  baspartn  12233  eltg3i  12241  tgclb  12250  topbas  12252  2basgeng  12267  topcld  12294  0cld  12297  uncld  12298  neif  12326  elnei  12337  0nei  12351  restbasg  12353  iscnp4  12403  cnpnei  12404  cnclima  12408  cncnp  12415  cnrest2r  12422  cndis  12426  lmff  12434  lmtopcnp  12435  txbas  12443  txopn  12450  txcnp  12456  upxp  12457  txdis1cn  12463  cnmpt11  12468  cnmpt21  12476  psmetge0  12516  xmetge0  12550  xmettpos  12555  xmetrtri  12561  metrtri  12562  xblpnfps  12583  xblpnf  12584  blfps  12594  blf  12595  ssblps  12610  ssbl  12611  blbas  12618  metss2  12683  xmettxlem  12694  xmettx  12695  qtopbas  12707  divcnap  12740  cncfss  12755  cdivcncfap  12772  expcncf  12777  cnopnap  12779  dedekindeulemuub  12780  dedekindeulemlu  12784  dedekindeu  12786  suplociccex  12788  dedekindicclemuub  12789  dedekindicclemlu  12793  dedekindicclemicc  12795  ivthinclemlopn  12799  ivthinclemuopn  12801  ivthinc  12806  ellimc3apf  12814  limcimolemlt  12818  limcimo  12819  limcresi  12820  cnplimclemle  12822  reldvg  12833  dvfgg  12842  dvidlemap  12845  dvcjbr  12857  dvcj  12858  dvrecap  12862  dveflem  12872  dvef  12873  reeff1oleme  12878  pilem3  12888  sinq34lt0t  12936  cosq14gt0  12937  coseq0q4123  12939  tangtx  12943  sincosq1eq  12944  cosordlem  12954  logdivlti  12983  bj-sels  13219  bj-nnelon  13264  pwle2  13300  pwf1oexmid  13301  pw1nct  13305  nninfall  13313  nninfsellemdc  13315  nninfself  13318  refeq  13332  isomninnlem  13334  cvgcmp2nlemabs  13336  trilpolemlt1  13343  trirec0  13346  apdifflemf  13348  apdifflemr  13349  apdiff  13350  iswomninnlem  13351
  Copyright terms: Public domain W3C validator