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

Theorem sylbi 118
Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
sylbi.1 (𝜑𝜓)
sylbi.2 (𝜓𝜒)
Assertion
Ref Expression
sylbi (𝜑𝜒)

Proof of Theorem sylbi
StepHypRef Expression
1 sylbi.1 . . 3 (𝜑𝜓)
21biimpi 117 . 2 (𝜑𝜓)
3 sylbi.2 . 2 (𝜓𝜒)
42, 3syl 14 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3imtr4i  194  simplbiim  373  mpan10  451  an12s  507  an32s  510  an4s  530  sylnbi  613  condc  760  notnotrdc  762  pm2.61ddc  769  pm5.18dc  788  dcim  795  pm2.25dc  803  pm2.85dc  822  pm5.12dc  827  pm5.14dc  828  pm5.55dc  830  peircedc  831  pm5.54dc  838  dcor  854  pm5.62dc  863  pm5.63dc  864  pm4.83dc  869  3simpb  913  3simpc  914  3imp  1109  3com12  1119  3com13  1120  syl3anb  1189  xoranor  1284  xorbin  1291  xordc1  1300  biassdc  1302  nfr  1427  nfand  1476  19.21t  1490  19.30dc  1534  exintrbi  1540  19.9t  1549  nfnt  1562  equveli  1658  exdistrfor  1697  sbcof2  1707  sbidm  1747  sbi1v  1787  sbalyz  1891  sbal1yz  1893  nfsb4t  1906  euex  1946  eumo0  1947  mor  1958  exmodc  1966  mo3h  1969  mopick  1994  moexexdc  2000  euexex  2001  2euex  2003  exists2  2013  eqcoms  2059  eleq2s  2148  nfcr  2186  necon3ai  2269  rexnalim  2334  rexex  2385  rsp  2386  ralim  2397  rexim  2430  r19.32r  2474  r19.44av  2486  r19.45av  2487  gencl  2603  gencbvex  2617  gencbval  2619  vtoclgf  2629  pm13.183  2703  elrabi  2717  eueq2dc  2736  eueq3dc  2737  mob2  2743  euxfr2dc  2748  reu3  2753  rmoim  2762  2rmorex  2767  sbcex  2794  sbcbi2  2835  ra5  2873  sseq1  2993  difdif  3096  difindiss  3218  undif3ss  3225  dfrab3ss  3242  abvor0dc  3269  reldisj  3298  disjel  3301  disj4im  3303  inssdif0im  3318  uneqdifeqim  3335  r19.2m  3336  r19.3rm  3337  r19.9rmv  3340  rexm  3347  ralm  3352  raaanlem  3353  ifnefalse  3369  nelpri  3426  prprc1  3505  difprsn2  3531  diftpsn3  3532  snsssn  3559  preqr2  3567  preq12b  3568  opthpr  3570  prneimg  3572  oprcl  3600  pwprss  3603  intmin4  3670  uniintabim  3679  dfiin2g  3717  iinss2  3736  iundif2ss  3749  invdisj  3786  trel  3888  trss  3890  ssex  3921  bnd2  3953  abssexg  3961  rext  3978  unipw  3980  euabex  3988  mss  3989  exss  3990  copsexg  4008  opelopabsb  4024  pwssunim  4048  epelg  4054  sowlin  4084  sotritric  4088  elsuci  4167  sucprc  4176  reusv3  4219  ordon  4239  onsucmin  4260  onsucelsucr  4261  unon  4264  onsucelsucexmid  4282  setind  4291  setind2  4292  sucprcreg  4300  en2lp  4305  eunex  4312  ordsoexmid  4313  ordpwsucss  4318  tfi  4332  peano1  4344  peano2  4345  find  4349  0nelelxp  4400  opelxp  4401  elvvuni  4431  optocl  4443  ralxpf  4509  rexxpf  4510  relop  4513  breldm  4566  dmxpm  4582  elreldm  4587  dmrnssfld  4622  dmcosseq  4630  resabs1  4667  resima2  4671  issref  4734  asymref  4737  xpidtr  4742  trin2  4743  poirr2  4744  xpmlem  4771  dmxpss  4780  xp11m  4786  cnveqb  4803  dfco2a  4848  cores2  4860  coi2  4864  relcnvtr  4867  relresfld  4874  relcnvexb  4884  cnviinm  4886  iotauni  4906  iota1  4908  iota4  4912  dffun8  4956  funcnvsn  4972  imadif  5006  imainlem  5007  fcoi1  5097  fcoi2  5098  f1ocnv  5166  f1ocnvb  5167  fun11iun  5174  ffoss  5185  f1o00  5188  fo00  5189  relelfvdm  5232  nfvres  5233  nfunsn  5234  ssimaex  5261  fvmptss2  5274  fvmptssdm  5282  unpreima  5319  respreima  5322  elrnrexdm  5333  elrnrexdmb  5334  rexrnmpt  5337  dffo4  5342  rnmptss  5353  fvpr1  5392  fvpr2  5393  elunirn  5432  f1veqaeq  5435  isores1  5481  riotauni  5501  riotacl2  5508  riota1  5513  riota1a  5514  snriota  5524  eusvobj2  5525  acexmidlema  5530  acexmidlemb  5531  acexmidlem2  5536  oprabid  5564  0neqopab  5577  brabvv  5578  1stval2  5809  2ndval2  5810  xp1st  5819  xp2nd  5820  unielxp  5827  releldm2  5838  cnvf1o  5873  fo2ndf  5875  poxp  5880  reldmtpos  5898  dftpos4  5908  tpostpos  5909  tpostpos2  5910  iunon  5929  smoel  5945  tfrlem4  5959  tfrlem7  5963  tfrlem8  5964  tfrlem9  5965  nnaord  6112  ecexr  6141  swoord1  6165  swoord2  6166  0er  6170  idssen  6287  ener  6289  en0  6305  en1  6309  en1bg  6310  2dom  6315  enm  6324  xpsnen  6325  snnen2og  6352  php5dom  6355  phpm  6357  findcard  6375  findcard2  6376  findcard2s  6377  finnum  6420  indpi  6497  subhalfnqq  6569  archnqq  6572  enq0sym  6587  nqnq0pi  6593  nqnq0  6596  mulnnnq0  6605  prml  6632  prmu  6633  prssnql  6634  prssnqu  6635  prcdnql  6639  prcunqu  6640  prltlu  6642  prnmaxl  6643  prnminu  6644  prloc  6646  prdisj  6647  addcanprg  6771  recexprlemopl  6780  recexprlemopu  6782  cauappcvgprlemladdfu  6809  caucvgprlemladdfu  6832  recexgt0sr  6915  renfdisj  7137  recexre  7642  apsqgt0  7665  apreim  7667  recexaplem2  7706  rerecclap  7780  nn0ge0  8263  elnnnn0b  8282  znegcl  8332  zeo  8401  nn0ind  8410  nn0ind-raph  8413  uzn0  8583  eluzaddi  8594  eluzsubi  8595  uznn0sub  8599  uz3m2nn  8610  uznnssnn  8615  uz2m1nn  8638  uz2mulcl  8641  indstr2  8642  qmulz  8654  qre  8656  qnegcl  8667  qreccl  8673  rphalflt  8709  nn0ledivnn  8784  xrltnr  8801  nltpnft  8830  ngtmnft  8831  xrrebnd  8832  xnegcl  8845  xnegneg  8846  xltnegi  8848  elioore  8881  elfzuz2  8994  uzsubsubfz  9012  fzdisj  9017  fzmmmeqm  9022  elfz0ubfz0  9083  elfz0fzfz0  9084  fz0fzelfz0  9085  fz0fzdiffz0  9088  elfzmlbp  9091  difelfzle  9093  difelfznle  9094  nn0disj  9096  2ffzeq  9099  fzo1fzo0n0  9140  elfzo0z  9141  elfzo0le  9142  fzonmapblen  9144  fzofzim  9145  elfzodifsumelfzo  9158  elfzonlteqm1  9167  fzonn0p1p1  9170  elfzom1p1elfzo  9171  ssfzo12bi  9182  ubmelm1fzo  9183  fzind2  9196  subfzo0  9198  rebtwn2z  9210  fldiv4p1lem1div2  9254  flqeqceilz  9267  zmodidfzoimp  9303  modfzo0difsn  9344  expcl2lemap  9431  qexpclz  9440  facp1  9597  facnn2  9601  faclbnd3  9610  bcn1  9625  cvg1nlemres  9811  rexanuz  9814  fclim  10045  climmo  10049  dvdsdivcl  10161  addmodlteqALT  10170  odd2np1  10183  oddge22np1  10192  m1expe  10210  nn0enne  10213  nn0o1gt2  10216  nno  10217  ialgfx  10253  bj-nfalt  10270  bdel  10331  bdssex  10388  bj-indind  10422  findset  10436
  Copyright terms: Public domain W3C validator