ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbird Unicode 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  |-  ( ph  ->  ch )
mpbird.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mpbird  |-  ( ph  ->  ps )

Proof of Theorem mpbird
StepHypRef Expression
1 mpbird.min . 2  |-  ( ph  ->  ch )
2 mpbird.maj . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32biimprd 157 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mpd 13 1  |-  ( ph  ->  ps )
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  3953  3brtr4d  3963  snelpwi  4137  prelpwi  4139  pwel  4143  ordelon  4308  onin  4311  elelsuc  4334  suceloni  4420  sucelon  4422  onintonm  4436  omsinds  4538  sosng  4615  relssdv  4634  eqbrrdv  4639  eqrelrdv2  4641  relsnopg  4646  breldmg  4748  elrnmptdv  4796  iss  4868  xpimasn  4990  elxp4  5029  elxp5  5030  funssres  5168  f0rn0  5320  sefvex  5445  fvun1  5490  eqfnfvd  5524  fvimacnvi  5537  fvimacnv  5538  fvelrn  5554  fmpt3d  5579  fmpt2d  5585  resflem  5587  fmptco  5589  fsn  5595  ftpg  5607  fconst2g  5638  funfvima3  5654  foeqcnvco  5694  f1eqcocnv  5695  fliftfun  5700  fliftfund  5701  fliftval  5704  riota5f  5757  f1ofveu  5765  f1ocnvd  5975  f1opw2  5979  off  5997  offval2  6000  ofrfval2  6001  caofref  6006  caofinvl  6007  elxp6  6070  cnvf1olem  6124  f2ndf  6126  f1od2  6135  tposf12  6169  smores2  6194  tfrlemisucaccv  6225  tfrlemibfn  6228  tfr1onlemsucaccv  6241  tfr1onlembfn  6244  tfrcllemsucaccv  6254  tfrcllembfn  6257  tfrcl  6264  tfri3  6267  frecabcl  6299  nnsucsssuc  6391  ersym  6444  ertr  6447  swoer  6460  erth  6476  riinerm  6505  qliftfund  6515  eroprf  6525  ecopoverg  6533  th3qlem1  6534  elmapssres  6570  mapss  6588  fdiagfn  6589  ixpssmap2g  6624  mapsnf1o  6634  f1dom2g  6653  dom3d  6671  fopwdom  6733  mapxpen  6745  nndomo  6761  dif1en  6776  findcard2  6786  findcard2s  6787  diffisn  6790  fimax2gtrilemstep  6797  fientri3  6806  fiintim  6820  f1dmvrnfibi  6835  sbthlemi6  6853  elfir  6864  fifo  6871  supelti  6892  supsnti  6895  cnvinfex  6908  ordiso2  6923  updjud  6970  djudom  6981  difinfsn  6988  ctssdc  7001  enumctlemm  7002  enumct  7003  enomnilem  7013  fodjuf  7020  ismkvnex  7032  omnimkv  7033  enmkvlem  7038  enwomnilem  7045  isnumi  7050  exmidfodomrlemrALT  7071  djudoml  7087  djudomr  7088  cc2lem  7093  cc3  7095  ltsopi  7147  pitri3or  7149  ltdcpi  7150  indpi  7169  enqdc  7188  enqdc1  7189  addcmpblnq  7194  mulcanenq  7212  recrecnq  7221  nqtri3or  7223  ltdcnq  7224  ltsonq  7225  ltaddnq  7234  subhalfnqq  7241  archnqq  7244  prarloclemarch2  7246  enq0tr  7261  nqnq0  7268  addcmpblnq0  7270  mulcanenq0ec  7272  nnnq0lem1  7273  nqpnq0nq  7280  nq0m0r  7283  nq02m  7292  prarloclemlt  7320  prarloclemcalc  7329  addlocpr  7363  nqprl  7378  nqpru  7379  addnqprlemrl  7384  addnqprlemru  7385  prmuloclemcalc  7392  mullocprlem  7397  mulnqprlemrl  7400  mulnqprlemru  7401  1idprl  7417  1idpru  7418  ltaddpr  7424  ltexprlemm  7427  ltexprlemopl  7428  ltexprlemopu  7430  ltexprlemdisj  7433  ltexprlemrl  7437  ltexprlemru  7439  addcanprleml  7441  addcanprlemu  7442  addcanprg  7443  prplnqu  7447  recexprlemloc  7458  recexprlem1ssl  7460  recexprlem1ssu  7461  aptiprleml  7466  aptiprlemu  7467  archpr  7470  cauappcvgprlemm  7472  cauappcvgprlemopl  7473  cauappcvgprlemloc  7479  cauappcvgprlemladdfu  7481  cauappcvgprlemladdfl  7482  cauappcvgprlem1  7486  cauappcvgprlem2  7487  caucvgprlemnkj  7493  caucvgprlemopl  7496  caucvgprlemloc  7502  caucvgprlemladdfu  7504  caucvgprlem2  7507  caucvgprprlemnkltj  7516  caucvgprprlemopl  7524  caucvgprprlemloc  7530  caucvgprprlemexbt  7533  caucvgprprlemaddq  7535  caucvgprprlem2  7537  suplocexprlemmu  7545  suplocexprlemru  7546  suplocexprlemloc  7548  suplocexprlemlub  7551  prsrlem1  7569  0idsr  7594  1idsr  7595  recexgt0sr  7600  archsr  7609  prsradd  7613  caucvgsrlemcau  7620  caucvgsrlembound  7621  caucvgsrlemoffgt1  7626  suplocsrlemb  7633  suplocsrlempr  7634  suplocsrlem  7635  pitonnlem1p1  7673  pitonn  7675  pitoregt0  7676  peano2nnnn  7680  recidpirq  7685  axcaucvglemval  7724  leid  7867  nltled  7902  readdcan  7921  addneintrd  7969  addneintr2d  7970  pncan  7987  subsub2  8009  subsub4  8014  negned  8089  subne0d  8101  subneintrd  8136  subneintr2d  8138  subeq0bd  8160  subdi  8166  gt0add  8354  rimul  8366  rereim  8367  ltmul1a  8372  apreim  8384  apirr  8386  mulap0r  8396  msqge0  8397  mulge0  8400  gt0ap0  8407  ltap  8414  recexaplem2  8432  mulap0bad  8439  mulap0bbd  8440  mul0eqap  8450  divrecap  8467  div0ap  8481  div1  8482  recrecap  8488  divdivdivap  8492  ddcanap  8505  rerecclap  8509  div2negap  8514  diveqap1bd  8614  recgt0  8627  prodgt0  8629  lemul1a  8635  recp1lt1  8676  squeeze0  8681  peano2nn  8751  div4p1lem1div2  8992  arch  8993  peano2z  9109  peano2zm  9111  ztri3or  9116  nn0n0n1ge2  9140  zextle  9161  gtndiv  9165  suprzclex  9168  nn0ind-raph  9187  uzid  9359  uzneg  9363  uztric  9366  uz11  9367  eluzp1l  9369  qdivcl  9457  irrmul  9461  rpnegap  9496  negelrpd  9498  ledivge1le  9536  mul2lt0rlt0  9569  mul2lt0rgt0  9570  nn0ledivnn  9577  ltpnf  9590  mnflt  9592  pnfge  9598  mnfle  9601  xrlttr  9604  xrltso  9605  xrlttri3  9606  xrleid  9609  xaddass2  9676  xltadd1  9682  xlt2add  9686  xleaddadd  9693  iccf1o  9810  fztri3or  9843  fznlem  9845  fzn  9846  fzsplit2  9854  fznatpl1  9880  uzsplit  9896  fseq1p1m1  9898  fzm1  9904  fznn0sub2  9929  difelfznle  9936  1fv  9940  fzodcel  9953  fzospliti  9977  fzouzsplit  9980  eluzgtdifelfzo  9998  exfzdc  10041  subfzo0  10043  exbtwnz  10052  qbtwnrelemcalc  10057  flqlelt  10073  qfraclt1  10077  qfracge0  10078  flqltnz  10084  btwnzge0  10097  flhalf  10099  ceiqle  10110  intfracq  10117  mulqmod0  10127  modqge0  10129  modqlt  10130  modqid  10146  modqid0  10147  m1modge3gt1  10168  modqltm1p1mod  10173  q2txmodxeq0  10181  modaddmodlo  10185  modsumfzodifsn  10193  addmodlteq  10195  frecuzrdgtcl  10209  frecuzrdgtclt  10218  uzennn  10233  uzsinds  10239  seqf  10258  seqf2  10261  monoord2  10274  iseqf1olemqk  10291  iseqf1olemjpcl  10292  iseqf1olemqpcl  10293  seq3f1olemqsumkj  10295  seq3f1olemqsum  10297  seq3f1olemstep  10298  seq3f1oleml  10300  ser3le  10315  exp3vallem  10318  exp3val  10319  expp1  10324  expcllem  10328  ltexp2a  10369  leexp2a  10370  faclbnd  10511  faclbnd2  10512  faclbnd3  10513  bcval5  10533  bcpasc  10536  hashennn  10550  fihasheqf1oi  10558  hashsng  10568  fihashfn  10570  hashun  10575  fihashss  10586  fihashssdif  10588  hashfz  10591  hashxp  10596  fimaxq  10597  zfz1isolem1  10607  seq3coll  10609  shftfn  10620  cjth  10642  cjmulrcl  10683  reim0bd  10740  rerebd  10741  cjrebd  10742  caucvgre  10777  cvg1nlemcxze  10778  cvg1nlemcau  10780  cvg1nlemres  10781  recvguniq  10791  resqrexlemover  10806  resqrexlemdec  10807  resqrexlemgt0  10816  resqrexlemoverl  10817  resqrexlemglsq  10818  rersqrtthlem  10826  sqrtgt0  10830  leabs  10870  absexpzap  10876  absle  10885  recvalap  10893  abstri  10900  abs2dif  10902  amgm2  10914  absne0d  10983  maxleim  11001  maxabslemab  11002  maxabslemlub  11003  maxltsup  11014  zmaxcl  11020  fimaxre2  11022  minmax  11025  rpmincl  11033  bdtrilem  11034  bdtri  11035  xrmaxleim  11037  xrmaxiflemcom  11042  xrmaxltsup  11051  xrmaxadd  11054  xrminmax  11058  xrminrpcl  11067  climconst  11083  climuni  11086  2clim  11094  climcn1  11101  climcn2  11102  reccn2ap  11106  climge0  11118  climle  11127  climsqz  11128  climsqz2  11129  serf0  11145  summodclem3  11173  summodclem2a  11174  fsumcl2lem  11191  sumpr  11206  sumtp  11207  fsum0diaglem  11233  mptfzshft  11235  fsumle  11256  fsumlt  11257  divcnv  11290  trireciplem  11293  expcnvap0  11295  expcnv  11297  explecnv  11298  geosergap  11299  cvgratnnlembern  11316  cvgratnnlemabsle  11320  cvgratnnlemsumlt  11321  cvgratz  11325  cvgratgt0  11326  mertenslemi1  11328  mertenslem2  11329  mertensabs  11330  clim2divap  11333  prodmodclem3  11368  prodmodclem2a  11369  eftcl  11384  ef0lem  11390  efsub  11411  eftlub  11420  eflegeo  11431  tanval2ap  11443  sinadd  11466  cos2t  11480  cos2tsin  11481  sin01bnd  11487  cos01bnd  11488  eirraplem  11506  dvdsval2  11519  dvdsdc  11524  dvds0lem  11526  zdvdsdc  11537  dvdscmulr  11545  dvdsmulcr  11546  dvdslelemd  11564  divconjdvds  11570  dvdsext  11576  fzm1ndvds  11577  dvdsmod  11583  oexpneg  11597  2tp1odd  11604  mulsucdiv2z  11605  2teven  11607  zeo5  11608  opeo  11617  omeo  11618  nn0ob  11628  divalglemnqt  11640  zsupcllemstep  11661  zsupcl  11663  zssinfcl  11664  infssuzex  11665  infssuzcldc  11667  gcddvds  11675  dvdslegcd  11676  gcdneg  11693  bezoutlemnewy  11707  bezoutlemstep  11708  bezoutlema  11710  bezoutlemb  11711  bezoutlemmo  11717  bezoutlemle  11719  bezoutlemsup  11720  dfgcd3  11721  bezout  11722  dfgcd2  11725  lcmcllem  11771  lcmneg  11778  lcmgcdlem  11781  lcmdvds  11783  lcmid  11784  3lcm2e6woprm  11790  6lcm4e12  11791  ncoprmgcdne1b  11793  mulgcddvds  11798  divgcdcoprmex  11806  cncongr1  11807  cncongr2  11808  isprm2lem  11820  prmind2  11824  dvdsnprmd  11829  prm2orodd  11830  sqnprm  11839  rpexp  11854  sqrt2irrlem  11862  oddpwdclemdc  11874  sqrt2irraplemnn  11880  qnumdencoprm  11894  qeqnumdivden  11895  nn0gcdsq  11901  nn0sqrtelqelz  11907  nonsq  11908  phicl2  11913  phibnd  11916  hashdvds  11920  phiprmpw  11921  phimullem  11924  hashgcdlem  11926  znnen  11934  ennnfonelemk  11936  ennnfonelemkh  11948  ennnfonelemhf1o  11949  ennnfonelemrnh  11952  ennnfonelemfun  11953  ennnfonelemf1  11954  ennnfonelemrn  11955  ennnfonelemnn0  11958  ctinfomlemom  11963  ctiunctlemudc  11973  unct  11978  omctfn  11979  structfung  12002  setsfun  12020  setsfun0  12021  setscom  12025  setsslid  12035  baspartn  12243  eltg3i  12251  tgclb  12260  topbas  12262  2basgeng  12277  topcld  12304  0cld  12307  uncld  12308  neif  12336  elnei  12347  0nei  12361  restbasg  12363  iscnp4  12413  cnpnei  12414  cnclima  12418  cncnp  12425  cnrest2r  12432  cndis  12436  lmff  12444  lmtopcnp  12445  txbas  12453  txopn  12460  txcnp  12466  upxp  12467  txdis1cn  12473  cnmpt11  12478  cnmpt21  12486  psmetge0  12526  xmetge0  12560  xmettpos  12565  xmetrtri  12571  metrtri  12572  xblpnfps  12593  xblpnf  12594  blfps  12604  blf  12605  ssblps  12620  ssbl  12621  blbas  12628  metss2  12693  xmettxlem  12704  xmettx  12705  qtopbas  12717  divcnap  12750  cncfss  12765  cdivcncfap  12782  expcncf  12787  cnopnap  12789  dedekindeulemuub  12790  dedekindeulemlu  12794  dedekindeu  12796  suplociccex  12798  dedekindicclemuub  12799  dedekindicclemlu  12803  dedekindicclemicc  12805  ivthinclemlopn  12809  ivthinclemuopn  12811  ivthinc  12816  ellimc3apf  12824  limcimolemlt  12828  limcimo  12829  limcresi  12830  cnplimclemle  12832  reldvg  12843  dvfgg  12852  dvidlemap  12855  dvcjbr  12867  dvcj  12868  dvrecap  12872  dveflem  12882  dvef  12883  reeff1oleme  12888  pilem3  12898  sinq34lt0t  12946  cosq14gt0  12947  coseq0q4123  12949  tangtx  12953  sincosq1eq  12954  cosordlem  12964  logdivlti  12996  relogbval  13061  relogbzcl  13062  nnlogbexp  13069  bj-sels  13256  bj-nnelon  13301  pwle2  13339  pwf1oexmid  13340  pw1nct  13344  nninfall  13352  nninfsellemdc  13354  nninfself  13357  refeq  13371  isomninnlem  13373  cvgcmp2nlemabs  13375  trilpolemlt1  13382  trirec0  13385  apdifflemf  13387  apdifflemr  13388  apdiff  13389  iswomninnlem  13390  ismkvnnlem  13392
  Copyright terms: Public domain W3C validator