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

Theorem sylibr 133
Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
sylibr.1  |-  ( ph  ->  ps )
sylibr.2  |-  ( ch  <->  ps )
Assertion
Ref Expression
sylibr  |-  ( ph  ->  ch )

Proof of Theorem sylibr
StepHypRef Expression
1 sylibr.1 . 2  |-  ( ph  ->  ps )
2 sylibr.2 . . 3  |-  ( ch  <->  ps )
32biimpri 132 . 2  |-  ( ps 
->  ch )
41, 3syl 14 1  |-  ( ph  ->  ch )
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:  sylbbr  135  pm5.74rd  182  bitri  183  3imtr4i  200  sylanbrc  413  oibabs  688  dcim  811  dcstab  814  stdcndc  815  stdcndcOLD  816  dcor  904  3mix1  1135  3mix2  1136  3jca  1146  syl3anbrc  1150  inegd  1335  pclem6  1337  xoranor  1340  nfxfrd  1436  nfd  1488  hban  1511  nfan1  1528  nford  1531  nfand  1532  hbim1  1534  alexim  1609  ax6blem  1613  nf4r  1634  19.34  1647  nfexd  1719  sbcof2  1766  nfsb2or  1793  sbidm  1807  nfdv  1833  nfeudv  1992  mon  2006  eumo  2009  mo23  2018  eu2  2021  eu3h  2022  exmodc  2027  exmonim  2028  mo2r  2029  mo3h  2030  bm1.1  2102  eqrdv  2115  3eltr4g  2203  abbi2dv  2236  abbi1dv  2237  nfcd  2253  nfcxfrd  2256  dcned  2291  neqned  2292  3netr4g  2320  necon3bi  2335  necon2ai  2339  alral  2455  rspe  2458  rsp2e  2460  rgen2a  2463  ralrimi  2480  r19.27v  2536  r19.28v  2537  r19.27av  2544  r19.32r  2555  nfreudxy  2581  mormo  2619  nrexrmo  2624  cgsex2g  2696  cgsex4g  2697  spc2egv  2749  spc2gv  2750  spc3egv  2751  spc3gv  2752  rspce  2758  ceqex  2786  elrab3t  2812  elrabd  2815  mosubt  2834  mo2icl  2836  reu3  2847  reu6i  2848  2rmorex  2863  sbc5  2905  rspesbca  2965  rmo2ilem  2970  sbnfc2  3030  ssrd  3072  ssrdv  3073  3sstr4g  3110  eqsstrid  3113  ss2abdv  3140  abssdv  3141  rabssdv  3147  ss2rabdv  3148  ssun1  3209  unssad  3223  unssbd  3224  ssddif  3280  uneqin  3297  indifdir  3302  undif3ss  3307  reuss2  3326  n0rf  3345  reximdva0m  3348  rabxmdc  3364  ssindif0im  3392  minel  3394  ralidm  3433  ralm  3437  dcun  3443  ifmdc  3479  disjsn2  3556  absneu  3565  rabsneu  3566  opprc  3696  elunii  3711  dfnfc2  3724  uniss2  3737  unidif  3738  ssunieq  3739  intab  3770  iunss2  3828  iunxdif2  3831  invdisj  3893  disjiun  3894  3brtr4g  3932  trin  4006  triun  4009  truni  4010  trint  4011  iinexgm  4049  class2seteq  4057  pwuni  4086  exmid1dc  4093  exmidn0m  4094  exmidsssn  4095  exmid0el  4097  exmidel  4098  exmidundif  4099  exmidundifim  4100  mss  4118  copsex2t  4137  euotd  4146  pwunim  4178  ispod  4196  sotricim  4215  exse  4228  frind  4244  trssord  4272  suctr  4313  pwnex  4340  eusvnf  4344  eusvnfb  4345  eusv2nf  4347  rexxfrd  4354  ralxfr2d  4355  rexxfr2d  4356  rabxfrd  4360  reuhypd  4362  eldifpw  4368  iunpw  4371  ssorduni  4373  sucelon  4389  onsucelsucr  4394  sucunielr  4396  ordtri2or2exmidlem  4411  onsucelsucexmid  4415  reg2exmidlema  4419  setindel  4423  elirr  4426  orddisj  4431  en2lp  4439  suc11g  4442  ordsuc  4448  nlimsucg  4451  ordtri2or2exmid  4456  zfregfr  4458  wessep  4462  tfi  4466  peano5  4482  limom  4497  peano2b  4498  nndceq0  4501  nnpredcl  4506  0nelrel  4555  eqrelrdv  4605  xpsspw  4621  relint  4633  relop  4659  eqbrrdva  4679  opeldm  4712  elres  4825  relssres  4827  exse2  4883  issref  4891  trin2  4900  dminss  4923  imainss  4924  rnxpid  4943  dmsn0el  4978  dmmptg  5006  relrelss  5035  cnviinm  5050  iotanul  5073  sniota  5085  dffun5r  5105  funmo  5108  funco  5133  funun  5137  funprg  5143  funtpg  5144  funtp  5146  fntpg  5149  fununi  5161  funcnvuni  5162  imadiflem  5172  imainlem  5174  funimaexglem  5176  isarep2  5180  fnunsn  5200  2elresin  5204  fnimadisj  5213  dmmptd  5223  fco  5258  funssxp  5262  fssres  5268  feu  5275  fimacnvdisj  5277  fabexg  5280  f00  5284  f0rn0  5287  f1co  5310  fores  5324  foco  5325  f1ores  5350  foimacnv  5353  f1oun  5355  fun11iun  5356  f1oco  5358  fo00  5371  brprcneu  5382  fv3  5412  relelfvdm  5421  nfvres  5422  nfunsn  5423  funfvbrb  5501  respreima  5516  dff2  5532  dff3im  5533  dffo4  5536  fvmptelrn  5541  ffvresb  5551  f1oresrab  5553  fmptco  5554  fsn  5560  fpr  5570  ftpg  5572  fsnunf  5588  fsnunfv  5589  elabrex  5627  dff1o6  5645  foeqcnvco  5659  fliftel1  5663  isores1  5683  isoini2  5688  riotasbc  5713  acexmidlemph  5735  acexmidlemcase  5737  oprabidlem  5770  brabvv  5785  eloprabga  5826  fnoprabg  5840  caovimo  5932  oprabexd  5993  fo1stresm  6027  fo2ndresm  6028  unielxp  6040  1st2ndbr  6050  fmpoco  6081  1stconst  6086  2ndconst  6087  poxp  6097  spc2ed  6098  disjxp1  6101  reldmtpos  6118  tposfun  6125  dftpos4  6128  smores  6157  smores2  6159  tfrlem1  6173  tfr0dm  6187  tfrlemibxssdm  6192  tfrlemibex  6194  tfrlemiubacc  6195  tfrlemi14d  6198  tfrexlem  6199  tfri1d  6200  tfr1onlembxssdm  6208  tfr1onlembex  6210  tfr1onlemubacc  6211  tfr1onlemres  6214  tfrcllemsucfn  6218  tfrcllembxssdm  6221  tfrcllembex  6223  tfrcllemubacc  6224  tfrcllemres  6227  tfri3  6232  rdgon  6251  frecabcl  6264  frecfcllem  6269  frecrdg  6273  2oconcl  6304  nnsucelsuc  6355  nntri3or  6357  nndceq  6363  nndcel  6364  dcdifsnid  6368  ecexr  6402  brdifun  6424  ecelqsdm  6467  iinerm  6469  eroveu  6488  erovlem  6489  ecopovtrn  6494  ecopovtrng  6497  th3qlem1  6499  pmsspw  6545  map0b  6549  mapsn  6552  mapsncnv  6557  ixpf  6582  uniixp  6583  ixpexgg  6584  resixp  6595  f1oen3g  6616  ssdomg  6640  domtr  6647  snfig  6676  enpr2d  6679  xpf1o  6706  xpmapenlem  6711  php5dom  6725  fidceq  6731  nnfi  6734  fiunsnnn  6743  findcard  6750  findcard2  6751  findcard2s  6752  ac6sfi  6760  tridc  6761  fimax2gtri  6763  finexdc  6764  exmidpw  6770  nnwetri  6772  unsnfi  6775  unsnfidcex  6776  unsnfidcel  6777  undifdcss  6779  tpfidisj  6784  iunfidisj  6802  snexxph  6806  fidcenumlemrks  6809  sbthlem2  6814  sbthlemi3  6815  sbthlem7  6819  sbthlemi8  6820  fival  6826  supmoti  6848  djuss  6923  updjudhf  6932  updjud  6935  casefun  6938  caseinj  6942  omp1eomlem  6947  djufun  6957  djuinj  6959  ctssdccl  6964  ctfoex  6971  finomni  6980  exmidomniim  6981  exmidomni  6982  fodjuomnilemdc  6984  nnnninf  6991  exmidonfinlem  7017  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  exmidaclem  7032  dju1en  7037  dmaddpqlem  7153  nqpi  7154  dmaddpq  7155  dmmulpq  7156  ltdcnq  7173  subhalfnqq  7190  enq0sym  7208  enq0ref  7209  enq0tr  7210  nqnq0pi  7214  nq0nn  7218  addnq0mo  7223  mulnq0mo  7224  nqpnq0nq  7229  nqnq0a  7230  nqnq0m  7231  npsspw  7247  elnp1st2nd  7252  prnmaxl  7264  prnminu  7265  prarloc  7279  genprndl  7297  genprndu  7298  nqprm  7318  nqprl  7327  nqpru  7328  addnqprlemrl  7333  addnqprlemru  7334  prmuloc  7342  mulnqprlemrl  7349  mulnqprlemru  7350  ltsopr  7372  ltexprlemm  7376  ltexprlemopl  7377  ltexprlemopu  7379  lteupri  7393  recexprlemopl  7401  recexprlemopu  7403  recexprlemdisj  7406  archpr  7419  cauappcvgprlemdisj  7427  cauappcvgprlemladdrl  7433  cauappcvgprlem2  7436  caucvgprlemnbj  7443  caucvgprlemdisj  7450  caucvgprlemladdfu  7453  caucvgprlem2  7456  caucvgprprlemnbj  7469  caucvgprprlemdisj  7478  suplocexprlemml  7492  suplocexprlemrl  7493  suplocexprlemmu  7494  suplocexprlemloc  7497  addsrmo  7519  mulsrmo  7520  recexgt0sr  7549  prsrpos  7561  caucvgsrlemasr  7566  suplocsrlemb  7582  suplocsrlempr  7583  suplocsr  7585  elrealeu  7605  pitonn  7624  pitoregt0  7625  pitore  7626  recnnre  7627  axaddcl  7640  axaddrcl  7641  axmulcl  7642  axmulrcl  7643  axrnegex  7655  axcnre  7657  axpre-lttrn  7660  rereceu  7665  axarch  7667  axpre-suploclemres  7677  axpre-suploc  7678  ltxrlt  7798  apirr  8334  cnstab  8374  divmulasscomap  8423  rerecclap  8457  lbreu  8667  arch  8932  0mnnnnn0  8967  nnm1nn0  8976  elnnnn0c  8980  elnnz1  9035  ztri3or0  9054  nzadd  9064  nn0n0n1ge2  9079  zdceq  9084  zdcle  9085  zdclt  9086  uzind  9120  eluzge3nn  9323  supinfneg  9346  infsupneg  9347  eluz2b2  9353  elnn1uz2  9357  nn01to3  9365  znq  9372  qaddcl  9383  qmulcl  9385  qreccl  9390  irradd  9394  irrmul  9395  cnref1o  9396  xrpnfdc  9580  xrmnfdc  9581  xaddcom  9599  xnegdi  9606  xpncan  9609  xleadd1a  9611  iooidg  9647  elioo4g  9672  fzdcel  9775  fznlem  9776  fzpreddisj  9806  elfz0ubfz0  9857  elfz0fzfz0  9858  fz0fzelfz0  9859  fz0fzdiffz0  9862  elfzmlbp  9864  difelfzle  9866  4fvwrd4  9872  fzosplit  9909  elfzo0  9914  fzo1fzo0n0  9915  elfzonn0  9918  fzofzim  9920  elfzo1  9922  elfzom1elp1fzo  9934  fzossfzop1  9944  ssfzo12bi  9957  exfzdc  9972  qdceq  9979  exbtwnzlemstep  9980  exbtwnzlemex  9982  exbtwnz  9983  rebtwn2zlemstep  9985  rebtwn2z  9987  qbtwnxr  9990  modfzo0difsn  10123  frec2uzrand  10133  frec2uzf1od  10134  frecuzrdgrcl  10138  frecuzrdgtcl  10140  frecuzrdgrclt  10143  frecuzrdgfunlem  10147  frecfzennn  10154  seq3f1olemp  10230  seq3f1oleml  10231  ser0f  10243  expcl2lemap  10260  hashunsng  10508  shftfvalg  10545  shftfval  10548  caucvgre  10708  rexanuz  10715  recvguniq  10722  rennim  10729  resqrexlemf  10734  rsqrmo  10754  fimaxre2  10953  climeu  11020  sumdc  11082  summodc  11107  zsumdc  11108  isum  11109  fisumss  11116  isumss2  11117  fsumsplit  11131  sumsnf  11133  fsumsplitsn  11134  sumtp  11138  sumsplitdc  11156  fsum2dlemstep  11158  fisum0diag2  11171  fsumconst  11178  modfsummodlemstep  11181  fsum00  11186  fsumabs  11189  fsumiun  11201  isumlessdc  11220  expcnv  11228  ef0lem  11280  modmulconst  11437  dvdsdivcl  11460  dvdsssfz1  11462  dvdsfac  11470  zeoxor  11478  nn0ehalf  11512  nn0oddm1d2  11518  nnoddm1d2  11519  divalglemeunn  11530  divalglemeuneg  11532  zsupcllemstep  11550  infssuzex  11554  gcdsupex  11558  gcdsupcl  11559  bezoutlemnewy  11596  bezoutlemmain  11598  bezoutlemeu  11607  dfgcd2  11614  algrf  11638  algcvgblem  11642  lcmgcdlem  11670  lcmdvds  11672  coprmgcdb  11681  mulgcddvds  11687  qredeu  11690  cncongr1  11696  cncongr2  11697  isprm2lem  11709  dvdsnprmd  11718  oddprmge3  11727  pw2dvdseu  11757  phibndlem  11803  dfphi2  11807  hashdvds  11808  phiprmpw  11809  hashgcdeq  11815  ennnfonelemdc  11823  ennnfonelemh  11828  ennnfonelemhf1o  11837  ennnfonelemf1  11842  ennnfonelemrn  11843  ennnfonelemdm  11844  exmidunben  11850  ctinfomlemom  11851  ctinfom  11852  ctiunctlemudc  11861  ctiunctlemf  11862  isstructim  11884  setsresg  11908  strleund  11958  1strbas  11969  2strbasg  11971  2stropg  11972  restsspw  12041  istopon  12091  toponcom  12105  topgele  12107  topontopn  12115  tsettps  12116  tgval  12129  eltg2b  12134  unitg  12142  tgss2  12159  bastop2  12164  distop  12165  epttop  12170  cldss2  12186  neisspw  12228  neipsm  12234  neiuni  12241  tgcn  12288  tgcnp  12289  cnntr  12305  lmff  12329  txuni2  12336  txbasex  12337  txbas  12338  txcnp  12351  txcnmpt  12353  txcn  12355  txdis  12357  txdis1cn  12358  cnmpt11  12363  cnmpt12  12367  cnmpt21  12371  cnmpt2t  12373  cnmpt22  12374  blsscls2  12573  xmetxpbl  12588  xmettxlem  12589  tgqioo  12627  fsumcncntop  12636  cncfmpt1f  12664  mulcncflem  12670  mulcncf  12671  dedekindeu  12681  dedekindicclemicc  12690  dedekindicc  12691  ivthinclemdisj  12698  limcimo  12714  cnmptlimc  12723  reldvg  12728  dvfvalap  12730  dvfgg  12737  dveflem  12766  dvef  12767  sincn  12769  coscn  12770  pilem3  12775  bj-nnal  12845  bj-trst  12847  bj-fast  12848  bj-stand  12852  bj-trdc  12855  bj-fadc  12856  decidr  12899  djulclALT  12904  djurclALT  12905  bj-indind  13026  bj-2inf  13032  bj-nntrans2  13046  bj-peano4  13049  bj-nnord  13052  bj-inf2vn  13068  bj-inf2vn2  13069  bj-findis  13073  pwf1oexmid  13090  exmid1stab  13091  subctctexmid  13092  nnsf  13095  nninfsellemdc  13102  nninffeq  13112  exmidsbthrlem  13113  sbthom  13117  triap  13120  trilpo  13132
  Copyright terms: Public domain W3C validator