Theorem syl5bb 535

Description: A syllogism inference from two biconditionals.

Hypotheses

Ref	Expression
syl5bb.1	|- (ph -> (ps <-> ch))
syl5bb.2	|- (th <-> ps)

Assertion

Ref	Expression
syl5bb	|- (ph -> (th <-> ch))

Proof of Theorem syl5bb

Step	Hyp	Ref	Expression
1		syl5bb.2	. . 3 |- (th <-> ps)
2	1	a1i 8	. 2 |- (ph -> (th <-> ps))
3		syl5bb.1	. 2 |- (ph -> (ps <-> ch))
4	2, 3	bitrd 531	1 |- (ph -> (th <-> ch))

Syntax hints:   -> wi 3   <-> wb 144

This theorem is referenced by:  syl5rbb 536  syl5bbr 537  3bitr4g 558  oplem1 777  19.23t 1152  sbcom 1296  necon3abid 1642  necon1abid 1662  r19.21t 1761  ceqsrexv 1935  ceqsrex2v 1936  elab2g 1946  elrabf 1950  eueq2 1964  reu8 1982  ru 1984  sbccomglem 2038  rabbirdv 2273  disjpss 2372  undif4 2378  opthpr 2550  dfiun2g 2654  elpwuni 2689  copsex4g 2870  opelopabg 2894  brabg 2895  dfid3 2914  oneqmini 3024  elsucg 3040  elsuc2g 3041  ordpwsuc 3172  dfom2 3220  opbrop 3324  opelcnvg 3387  iss 3487  imasng 3516  dmsnop 3577  cores 3602  cnvpo 3627  fncnv 3666  fununi 3668  fnssresb 3705  dffn5 3869  funimass4 3874  fnsnfv 3878  dmfco 3884  fvco 3885  fvopabn 3897  fvopab5 3904  elrnopabg 3914  fvimacnvi 3918  fvimacnvALT 3923  fressnfv 3952  funiunfv 3980  elunirnALT 3983  dff13 3988  isoini 4014  f1oiso 4018  f1oweALT 4020  fnotoprb 4049  eloprabg 4067  oprabval 4083  elrnoprabg 4186  1stconst 4190  2ndconst 4191  fparlem1 4199  fparlem2 4200  onopriun 4211  tfrlem1 4212  rdglim2 4250  brecop 4447  mapsn 4486  ixp0 4502  xpsnen 4576  xpdom2 4583  pw2en 4587  mapxpen 4642  onfin 4666  fodomfib 4710  noinfep 4786  rankbnd2 4850  aceq3lem 4878  zorn2 4942  fodomb 4946  brdom7disj 4950  brdom6disj 4951  domtri 4987  cardsdomel 5002  iscard2 5004  alephnbtwn 5018  nlt1pi 5187  ltsopq 5229  genpv 5256  ltsosr 5357  suppsrlem 5375  suppsr 5376  supsrlem6 5384  suprelem 5413  supre 5414  axrrecex 5438  renegcli 5570  ltxr 5649  ltxrlt 5654  xrlenlt 5655  ssxr 5694  conjmul 5937  lereci 6025  lt2msqi 6026  nn1suc 6084  infm3 6222  infmsup 6236  elznn0 6317  elnn0nn 6339  zltp1le 6349  prime 6366  dfuzi 6373  rebtwnz 6394  ioo0 6494  elioo3g 6506  snunioolem 6541  ioojoin 6543  elfz2 6600  fzsuc 6636  fzshftral 6653  om2uzisoi 6665  sq11i 6823  dffsum 7201  caucvg3 7371  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  ivthlem7 7492  tpsex 7817  istps 7818  bastop2 7855  islp2 7957  iscn 7968  iscnp 7970  ismsg 8010  metxp 8044  cncfmet 8116  bl2ioo 8122  iscau 8147  lmclim 8174  grpidval 8275  isring 8382  isvclem 8443  isnvlem 8476  isphg 8732  isph 8737  phoeqi 8774  spwpr2 8920  spwval 8921  spwnex 8923  sineq0re 8985  shftefif1olem 9013  hhph 9321  sh2 9367  chocunii 9448  projlem15 9476  pjtheu2i 9526  adjeq 10139  elunop2 10217  lnophm 10223  cnlnadjeui 10289  adjbd1o 10297  jpi 10478  mddmd2 10517  chrelati 10572  chrelat2i 10573  cvexchlem 10576  dmdbr5ati 10631  cdjreui 10641  cdj3i 10650  ficli 10756  twsymr 10808  istoset 10861  opidon 10898  exidu1 10902  issmgrp 10911  ismnd 10926  rngmgmbs4 10945  isdivrng 10968  cdrci 10994  cnvhmph 11033  homcard 11045  fgsb 11082  fgsb2 11086  cnfilca 11088  rcfpfillem3 11091  limfillem1 11101  bwt2 11123  usinuniop 11128  singcon 11137  ismgra 11164  isalg 11175  isded 11190  iscat 11208  dfiin2g 11400  fictb 11423  inficlALT 11424  omsubinit 11451  opncldf1 11454  opncldf2 11455  opncldf3 11456  subcls 11481  compsub 11488  compfipin0lem 11492  compfipin0 11493  topfneec 11562  islocfin 11567  neibastop2lem3 11582  neibastop2lem4 11583  isnrm2 11613  elfg 11633  filrn 11643  neifg 11644  fbaslim 11680  cnpfillim 11686  elfilmap2 11691  elfilmap3 11692  flimfnei 11710  fclusbas 11722  isgalem 11771  unpreima 11794  respreima 11795  resoprab2 11809  cnvcan 11814  sdc 11877  blssp 11908  metsstop 11909  icoopnst 11940  iocopnst 11941  cnresima 11952  tlmbrf 11966  uptx 11978  txcnoprab 11981  sstotbnd 11992  bfplem11 12064  rrnheibor 12079  ishgrag 12195  ispgrag 12205

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain