Theorem syl5bb 591

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 587	1 |- (ph -> (th <-> ch))

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

This theorem is referenced by:  syl5rbb 592  syl5bbr 593  3bitr4g 614  oplem1 852  19.23t 1474  sbcom 1632  necon3abid 2033  necon3bid 2035  necon1abid 2061  r19.21t 2177  ceqsrexv 2394  ceqsrex2v 2395  elab2g 2406  elrabf 2413  eueq2 2429  reu8 2448  ru 2451  sbccomglem 2525  csbabg 2588  rabbirdvOLD 2802  disjpss 2924  undif4OLD 2931  rexsng 3072  difsn 3125  opthpr 3156  dfiun2gOLD 3284  dfiin2g 3286  iinxsng 3325  elpwuni 3335  copsex4g 3540  opelopabg 3567  brabg 3568  dfid3 3587  dffr2 3627  ordtri4 3699  oneqmini 3714  elsucg 3732  elsuc2g 3733  dfwe2 3861  ordpwsuc 3896  dfom2 3951  opelxp 4036  opbrop 4064  opelcnvgOLD 4141  issOLD 4255  dmsnopOLD 4368  coresOLD 4401  cnvpo 4427  dffun8 4448  fncnv 4479  fununi 4481  fnssresb 4525  dffn5 4717  funimass4 4722  fnsnfv 4728  dmfco 4735  fvco 4736  fvopabn 4749  fvopab5 4756  elrnopabg 4773  fvimacnvi 4777  fvimacnvALT 4782  fressnfv 4813  funiunfv 4842  elunirnALT 4845  dff13 4850  isoini 4877  f1oiso 4881  f1oweALT 4883  fnotoprb 4916  eloprabg 4936  oprabval 4952  elrnoprabg 5066  1stconst 5070  2ndconst 5071  fparlem1 5081  fparlem2 5082  onopriun 5118  tfrlem1 5119  rdglim2 5157  brecop 5365  mapsn 5404  ixp0 5420  xpsnen 5494  xpdom2 5501  pw2en 5505  riotaundb 5574  mapxpen 5589  onfin 5613  fodomfib 5657  noinfep 5747  rankbnd2 5815  omsubinit 5890  aceq3lem 5894  zorn2 5958  fodomb 5962  brdom7disj 5966  brdom6disj 5967  domtri 5989  cardsdomel 6004  iscard2 6006  alephnbtwn 6016  nlt1pi 6185  ltsopq 6227  genpv 6254  ltsosr 6355  suppsrlem 6373  suppsr 6374  supsrlem6 6382  suprelem 6411  supre 6412  axrrecex 6437  renegcli 6576  renegcliOLD 6577  ltxr 6664  ltxrlt 6669  xrlenlt 6670  ssxrOLD 6715  conjmul 6975  lereci 7063  lt2msqi 7064  nn1suc 7122  infm3 7263  infmsup 7277  elznn0 7358  elnn0nn 7380  zltp1le 7390  prime 7407  dfuzi 7414  rebtwnz 7435  ioo0 7535  elioo3g 7547  snunioolem 7583  ioojoin 7585  elfz2 7642  fzsuc 7678  fzshftral 7701  om2uzisoi 7713  sq11i 7871  dffsum 8258  caucvg3 8428  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  ivthlem7 8549  tpsex 8874  istps 8875  bastop2 8913  islp2 9023  iscn 9034  iscnp 9036  ismsg 9077  metxp 9111  cncfmet 9183  bl2ioo 9189  iscau 9214  lmclim 9241  grpidval 9342  isgalem 9449  isring 9465  isvclem 9528  isnvlem 9561  isphg 9817  isph 9822  phoeqi 9859  spwpr2 10001  spwval 10002  spwnex 10004  sineq0re 10067  shftefif1olem 10095  cdrci 10182  istoset 10209  uptx 10226  elfg 10284  filrn 10293  elfilmap2 10313  elfilmap3 10314  flimfnei 10319  fbaslim 10322  usinuniop 10341  opidon 10369  exidu1 10373  issmgrp 10381  ismnd 10390  rngmgmbs4 10401  isdivrng 10417  hhph 10678  sh2 10724  chocunii 10805  projlem15 10833  pjtheu2i 10883  adjeq 11496  elunop2 11575  lnophm 11581  cnlnadjeui 11647  adjbd1o 11655  jpi 11842  mddmd2 11881  chrelati 11936  chrelat2i 11937  cvexchlem 11940  dmdbr5ati 11994  cdjreui 12004  cdj3i 12013  bnj971 12860  bnj1454 13135  bnj517 13259  bnj891 13321  bnj892 13322  bnj984 13358  bnj1173 13441  bnj1313 13494  bnj1319 13495  bnj1321 13498  bnj1373 13506  bnj1417 13530  elfzm11 13604  eqreznegel 13654  divides 13664  gcdcllem2 13719  gcdn0gt0 13728  mulgcdlem2 13757  isprm2 13775  isprm3 13776  dfon2lem3 13851  poseq 13954  axsltsolem1 14006  axfelem16 14046  fnoprvpop 14338  ficli 14353  twsymr 14394  cbicplem 14508  iscst4 14522  dffprod 14670  prsubrtr 14763  vecval1b 14794  svs2 14829  cnvhmph 14881  homcard 14893  fgsb 14921  fgsb2 14925  cnfilca 14927  rcfpfillem3 14930  limfillem1 14938  bwt2 14960  singcon 14968  istopgrp 14971  supnuf 15041  supexr 15043  ismgra 15057  isalg 15068  isded 15083  iscat 15101  dualalg 15131  bpmp 15251  btmp 15252  vtarsuelt 15272  isplibg 15319  dfiin2gOLD 15356  fictb 15371  inficlALT 15372  omsubinitOLD 15399  opncldf1 15402  opncldf2 15403  opncldf3 15404  subcls 15424  compsub 15431  compfipin0lem 15435  compfipin0 15436  topfneec 15501  islocfin 15506  neibastop2lem3 15521  neibastop2lem4 15522  isnrm2 15552  neifg 15559  cnpfillim 15589  fclusbas 15610  unpreima 15683  respreima 15684  oprabvalg 15706  resoprab2 15710  cnvcan 15715  addsubeq4 15778  fzsplit 15792  sdc 15811  fdc 15812  blssp 15844  icoopnst 15876  iocopnst 15877  cnresima 15891  tlmbrf 15905  txcnoprab 15911  txmet 15925  sstotbnd 15936  bfplem11 16008  rrnheibor 16023  isfldidl2 16217  isdmn3 16222  prtlem16 16272  prtlem19 16280  ishgrag 16291  ispgrag 16301  pm10.52 16312  pm14.122a 16386  pm14.122b 16387  pm14.123a 16389  rusbcALT 16410  compab 16418  fvsb 16430  strdif 16719  eustrdif 16722  pltval 16781  posgelem 16795  lubid 16807  cmtval 16938  omllaw2 16965  cvrval 16988  cvrval2 16991  pmapglbx 17251

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 164  df-an 242

Copyright terms: Public domain