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

Theorem mpbird 165
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 156 . 2 (𝜑 → (𝜒𝜓))
41, 3mpd 13 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  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:  mpbiri  166  pm5.19  655  mpbir2and  888  pm3.12dc  902  mpbir3and  1124  pm5.15dc  1323  eqeltrd  2161  eqnetrd  2275  3netr4d  2284  sbcne12g  2938  eqsstrd  3049  3sstr4d  3058  eqbrtrd  3840  3brtr4d  3850  snelpwi  4013  prelpwi  4015  pwel  4019  ordelon  4184  onin  4187  elelsuc  4210  suceloni  4291  sucelon  4293  onintonm  4307  omsinds  4408  sosng  4479  relssdv  4498  eqbrrdv  4503  eqrelrdv2  4505  relsnopg  4510  breldmg  4610  iss  4725  xpimasn  4845  elxp4  4884  elxp5  4885  funssres  5021  f0rn0  5168  sefvex  5289  fvun1  5333  eqfnfvd  5363  fvimacnvi  5376  fvimacnv  5377  fvelrn  5393  fmpt3d  5417  fmpt2d  5423  resflem  5425  fmptco  5427  fsn  5432  ftpg  5444  fconst2g  5473  funfvima3  5489  foeqcnvco  5530  f1eqcocnv  5531  fliftfun  5536  fliftfund  5537  fliftval  5540  riota5f  5593  f1ofveu  5601  f1ocnvd  5803  f1opw2  5807  fnofval  5822  off  5825  offval2  5827  ofrfval2  5828  caofref  5833  caofinvl  5834  elxp6  5897  cnvf1olem  5946  f2ndf  5948  f1od2  5957  tposf12  5988  smores2  6013  tfrlemisucaccv  6044  tfrlemibfn  6047  tfr1onlemsucaccv  6060  tfr1onlembfn  6063  tfrcllemsucaccv  6073  tfrcllembfn  6076  tfrcl  6083  tfri3  6086  frecabcl  6118  nnsucsssuc  6207  ersym  6256  ertr  6259  swoer  6272  erth  6288  riinerm  6317  qliftfund  6327  eroprf  6337  ecopoverg  6345  th3qlem1  6346  elmapssres  6382  mapss  6400  fdiagfn  6401  f1dom2g  6425  dom3d  6443  fopwdom  6504  mapxpen  6516  nndomo  6532  dif1en  6547  findcard2  6557  findcard2s  6558  diffisn  6561  fimax2gtrilemstep  6568  fientri3  6577  f1dmvrnfibi  6603  sbthlemi6  6615  supelti  6641  supsnti  6644  cnvinfex  6657  ordiso2  6672  djuun  6704  updjud  6717  djudom  6731  enomnilem  6738  fodjuomnilemf  6744  isnumi  6754  exmidfodomrlemrALT  6773  ltsopi  6823  pitri3or  6825  ltdcpi  6826  indpi  6845  enqdc  6864  enqdc1  6865  addcmpblnq  6870  mulcanenq  6888  recrecnq  6897  nqtri3or  6899  ltdcnq  6900  ltsonq  6901  ltaddnq  6910  subhalfnqq  6917  archnqq  6920  prarloclemarch2  6922  enq0tr  6937  nqnq0  6944  addcmpblnq0  6946  mulcanenq0ec  6948  nnnq0lem1  6949  nqpnq0nq  6956  nq0m0r  6959  nq02m  6968  prarloclemlt  6996  prarloclemcalc  7005  addlocpr  7039  nqprl  7054  nqpru  7055  addnqprlemrl  7060  addnqprlemru  7061  prmuloclemcalc  7068  mullocprlem  7073  mulnqprlemrl  7076  mulnqprlemru  7077  1idprl  7093  1idpru  7094  ltaddpr  7100  ltexprlemm  7103  ltexprlemopl  7104  ltexprlemopu  7106  ltexprlemdisj  7109  ltexprlemrl  7113  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  addcanprg  7119  prplnqu  7123  recexprlemloc  7134  recexprlem1ssl  7136  recexprlem1ssu  7137  aptiprleml  7142  aptiprlemu  7143  archpr  7146  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemloc  7155  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlem1  7162  cauappcvgprlem2  7163  caucvgprlemnkj  7169  caucvgprlemopl  7172  caucvgprlemloc  7178  caucvgprlemladdfu  7180  caucvgprlem2  7183  caucvgprprlemnkltj  7192  caucvgprprlemopl  7200  caucvgprprlemloc  7206  caucvgprprlemexbt  7209  caucvgprprlemaddq  7211  caucvgprprlem2  7213  prsrlem1  7232  0idsr  7257  1idsr  7258  recexgt0sr  7263  archsr  7271  prsradd  7275  caucvgsrlemcau  7282  caucvgsrlembound  7283  caucvgsrlemoffgt1  7288  pitonnlem1p1  7327  pitonn  7329  pitoregt0  7330  peano2nnnn  7334  recidpirq  7339  axcaucvglemval  7376  leid  7513  nltled  7548  readdcan  7566  addneintrd  7614  addneintr2d  7615  pncan  7632  subsub2  7654  subsub4  7659  negned  7734  subne0d  7746  subneintrd  7781  subneintr2d  7783  subeq0bd  7801  subdi  7807  gt0add  7991  rimul  8003  rereim  8004  ltmul1a  8009  apreim  8021  apirr  8023  mulap0r  8033  msqge0  8034  mulge0  8037  gt0ap0  8043  ltap  8049  recexaplem2  8060  mulap0bad  8067  mulap0bbd  8068  divrecap  8094  div0ap  8108  div1  8109  recrecap  8115  divdivdivap  8119  ddcanap  8132  rerecclap  8136  div2negap  8141  recgt0  8246  prodgt0  8248  lemul1a  8254  recp1lt1  8295  squeeze0  8300  peano2nn  8369  div4p1lem1div2  8602  arch  8603  peano2z  8719  peano2zm  8721  ztri3or  8726  nn0n0n1ge2  8750  zextle  8770  gtndiv  8774  suprzclex  8777  nn0ind-raph  8796  uzid  8965  uzneg  8969  uztric  8972  uz11  8973  eluzp1l  8975  qdivcl  9060  irrmul  9064  rpnegap  9098  ledivge1le  9135  nn0ledivnn  9170  ltpnf  9183  mnflt  9185  pnfge  9191  mnfle  9194  xrlttr  9197  xrltso  9198  xrlttri3  9199  xrleid  9201  iccf1o  9353  fztri3or  9385  fznlem  9387  fzn  9388  fzsplit2  9396  fznatpl1  9420  uzsplit  9436  fseq1p1m1  9438  fzm1  9444  fznn0sub2  9467  difelfznle  9474  1fv  9478  fzodcel  9491  fzospliti  9515  fzouzsplit  9518  eluzgtdifelfzo  9536  exfzdc  9579  subfzo0  9581  exbtwnz  9590  qbtwnrelemcalc  9595  flqlelt  9611  qfraclt1  9615  qfracge0  9616  flqltnz  9622  btwnzge0  9635  flhalf  9637  ceiqle  9648  intfracq  9655  mulqmod0  9665  modqge0  9667  modqlt  9668  modqid  9684  modqid0  9685  m1modge3gt1  9706  modqltm1p1mod  9711  q2txmodxeq0  9719  modaddmodlo  9723  modsumfzodifsn  9731  addmodlteq  9733  frecuzrdgtcl  9747  frecuzrdgtclt  9756  uzsinds  9776  iseqfclt  9794  iseqoveq  9798  monoord2  9810  iseqf1olemqk  9827  iseqf1olemjpcl  9828  iseqf1olemqpcl  9829  iseqf1olemqsumkj  9831  iseqf1olemqsum  9833  iseqf1olemstep  9834  iseqf1oleml  9836  iseqid3  9840  serile  9851  expivallem  9854  expival  9855  expp1  9860  expcllem  9864  ltexp2a  9905  leexp2a  9906  faclbnd  10045  faclbnd2  10046  faclbnd3  10047  ibcval5  10067  bcpasc  10070  hashennn  10084  fihasheqf1oi  10092  hashsng  10102  fihashfn  10104  hashun  10109  fihashss  10120  fihashssdif  10122  hashfz  10125  hashxp  10130  fimaxq  10131  zfz1isolem1  10141  iseqcoll  10143  shftfn  10154  cjth  10175  cjmulrcl  10216  reim0bd  10273  rerebd  10274  cjrebd  10275  caucvgre  10309  cvg1nlemcxze  10310  cvg1nlemcau  10312  cvg1nlemres  10313  recvguniq  10323  resqrexlemover  10338  resqrexlemdec  10339  resqrexlemgt0  10348  resqrexlemoverl  10349  resqrexlemglsq  10350  rersqrtthlem  10358  sqrtgt0  10362  leabs  10402  absexpzap  10408  absle  10417  recvalap  10425  abstri  10432  abs2dif  10434  amgm2  10446  absne0d  10515  maxleim  10533  maxabslemab  10534  maxabslemlub  10535  maxltsup  10546  fimaxre2  10551  minmax  10554  climconst  10571  climuni  10574  2clim  10582  climcn1  10589  climcn2  10590  climge0  10605  climle  10614  climsqz  10615  climsqz2  10616  serif0  10631  isummolem3  10659  isummolem2a  10660  dvdsval2  10674  dvdsdc  10679  dvds0lem  10681  zdvdsdc  10692  dvdscmulr  10700  dvdsmulcr  10701  dvdslelemd  10719  divconjdvds  10725  dvdsext  10731  fzm1ndvds  10732  dvdsmod  10738  oexpneg  10752  2tp1odd  10759  mulsucdiv2z  10760  2teven  10762  zeo5  10763  opeo  10772  omeo  10773  nn0ob  10783  divalglemnqt  10795  zsupcllemstep  10816  zsupcl  10818  zssinfcl  10819  infssuzex  10820  infssuzcldc  10822  gcddvds  10830  dvdslegcd  10831  gcdneg  10848  bezoutlemnewy  10860  bezoutlemstep  10861  bezoutlema  10863  bezoutlemb  10864  bezoutlemmo  10870  bezoutlemle  10872  bezoutlemsup  10873  dfgcd3  10874  bezout  10875  dfgcd2  10878  lcmcllem  10924  lcmneg  10931  lcmgcdlem  10934  lcmdvds  10936  lcmid  10937  3lcm2e6woprm  10943  6lcm4e12  10944  ncoprmgcdne1b  10946  mulgcddvds  10951  divgcdcoprmex  10959  cncongr1  10960  cncongr2  10961  isprm2lem  10973  prmind2  10977  dvdsnprmd  10982  prm2orodd  10983  sqnprm  10992  rpexp  11007  sqrt2irrlem  11015  oddpwdclemdc  11026  sqrt2irraplemnn  11032  qnumdencoprm  11046  qeqnumdivden  11047  nn0gcdsq  11053  nn0sqrtelqelz  11059  nonsq  11060  phicl2  11065  phibnd  11068  hashdvds  11072  phiprmpw  11073  phimullem  11076  hashgcdlem  11078  znnen  11086  bj-sels  11243  bj-nnelon  11292  nninfall  11338  nninfsellemdc  11340  nninfself  11343
  Copyright terms: Public domain W3C validator