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

Theorem sylbi 114
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 113 . 2 (φψ)
3 sylbi.2 . 2 (ψχ)
42, 3syl 14 1 (φχ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3imtr4i  190  mpan10  446  an12s  487  an32s  490  an4s  509  sylnbi  590  condc  737  notnot2dc  739  pm2.61ddc  746  pm5.18dc  765  dcim  772  pm2.25dc  780  pm2.85dc  799  pm5.12dc  804  pm5.14dc  805  pm5.55dc  807  peircedc  808  pm5.54dc  815  dcor  829  pm5.62dc  838  pm5.63dc  839  pm4.83dc  844  3simpb  888  3simpc  889  3imp  1082  3com12  1092  3com13  1093  syl3anb  1162  xoranor  1251  xorbin  1256  xordc1  1265  biassdc  1267  nfr  1388  nfand  1438  19.21t  1452  19.30dc  1496  exintrbi  1502  19.9t  1511  nfnt  1524  equveli  1620  exdistrfor  1659  sbcof2  1669  sbidm  1709  sbi1v  1749  sbalyz  1853  sbal1yz  1855  nfsb4t  1868  euex  1908  eumo0  1909  mor  1920  exmodc  1928  mo3h  1931  mopick  1956  moexexdc  1962  euexex  1963  2euex  1965  exists2  1975  eqcoms  2021  eleq2s  2110  nfcr  2148  necon3ai  2228  rexnalim  2291  rexex  2342  rsp  2343  ralim  2354  rexim  2387  r19.32r  2431  r19.44av  2443  r19.45av  2444  gencl  2559  gencbvex  2573  gencbval  2575  vtoclgf  2585  pm13.183  2654  elrabi  2668  eueq2dc  2687  eueq3dc  2688  mob2  2694  euxfr2dc  2699  reu3  2704  rmoim  2713  2rmorex  2718  sbcex  2745  ra5  2819  sseq1  2939  difdif  3042  difindiss  3164  undif3ss  3171  dfrab3ss  3188  abvor0dc  3215  reldisj  3244  disjel  3247  disj4im  3249  inssdif0im  3264  uneqdifeqim  3281  r19.2m  3282  r19.3rm  3285  r19.9rmv  3287  rexm  3295  ralm  3300  raaanlem  3301  ifnefalse  3315  nelpri  3367  prprc1  3448  difprsn2  3474  diftpsn3  3475  snsssn  3502  preqr2  3510  preq12b  3511  opthpr  3513  prneimg  3515  oprcl  3543  pwprss  3546  intmin4  3613  uniintabim  3622  dfiin2g  3660  iinss2  3679  iundif2ss  3692  invdisj  3729  trel  3831  trss  3833  ssex  3864  bnd2  3896  abssexg  3904  rext  3921  unipw  3923  euabex  3931  mss  3932  exss  3933  copsexg  3951  opelopabsb  3967  pwssunim  3991  epelg  3997  sowlin  4027  sotritric  4031  elsuci  4085  sucprc  4094  reusv3  4138  ordon  4158  onsucmin  4178  onsucelsucr  4179  unon  4182  onsucelsucexmid  4195  setind  4202  setind2  4203  sucprcreg  4207  en2lp  4212  eunex  4219  ordsoexmid  4220  ordpwsucss  4223  tfi  4228  peano1  4240  peano2  4241  find  4245  0nelelxp  4296  opelxp  4297  elvvuni  4327  optocl  4339  ralxpf  4405  rexxpf  4406  relop  4409  breldm  4462  dmxpm  4478  elreldm  4483  dmrnssfld  4518  dmcosseq  4526  resabs1  4563  resima2  4567  issref  4630  asymref  4633  xpidtr  4638  trin2  4639  poirr2  4640  xpmlem  4667  dmxpss  4676  xp11m  4682  cnveqb  4699  dfco2a  4744  cores2  4756  coi2  4760  relcnvtr  4763  relresfld  4770  relcnvexb  4780  cnviinm  4782  iotauni  4802  iota1  4804  iota4  4808  dffun8  4851  funcnvsn  4867  imadif  4901  imainlem  4902  fcoi1  4991  fcoi2  4992  f1ocnv  5060  f1ocnvb  5061  fun11iun  5068  ffoss  5079  f1o00  5082  fo00  5083  relelfvdm  5126  nfvres  5127  nfunsn  5128  ssimaex  5155  fvmptss2  5168  fvmptssdm  5176  unpreima  5213  respreima  5216  elrnrexdm  5227  elrnrexdmb  5228  rexrnmpt  5231  dffo4  5236  rnmptss  5247  fvpr1  5286  fvpr2  5287  elunirn  5326  f1veqaeq  5329  isores1  5375  riotauni  5394  riotacl2  5401  riota1  5406  riota1a  5407  snriota  5417  eusvobj2  5418  acexmidlema  5423  acexmidlemb  5424  acexmidlem2  5429  oprabid  5457  0neqopab  5469  brabvv  5470  1stval2  5701  2ndval2  5702  xp1st  5711  xp2nd  5712  unielxp  5719  releldm2  5730  cnvf1o  5765  fo2ndf  5767  poxp  5771  reldmtpos  5786  dftpos4  5796  tpostpos  5797  tpostpos2  5798  iunon  5817  smoel  5833  tfrlem4  5847  tfrlem7  5851  tfrlem8  5852  tfrlem9  5853  nnaord  5989  ecexr  6018  swoord1  6042  swoord2  6043  0er  6047  subhalfnqq  6265  archnqq  6268  enq0sym  6281  nqnq0pi  6287  nqnq0  6290  mulnnnq0  6299  prml  6325  prmu  6326  prssnql  6327  prssnqu  6328  prcdnql  6332  prcunqu  6333  prltlu  6335  prnmaxl  6336  prnminu  6337  prloc  6339  prdisj  6340  addcanprg  6447  recexprlemopl  6453  recexprlemopu  6455  recexsrlem  6514  renfdisj  6674  bj-nfalt  7150  bdel  7211  bdssex  7264  findset  7306
  Copyright terms: Public domain W3C validator