Theorem syl5bb 532

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

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

This theorem is referenced by:  syl5rbb 533  syl5bbr 534  3bitr4g 555  oplem1 772  19.23t 1116  sbcom 1258  necon3abid 1599  necon1abid 1618  r19.21t 1715  ceqsrexv 1889  ceqsrex2v 1890  elab2g 1900  elrabf 1904  eueq2 1918  reu8 1936  ru 1938  sbccomglem 1988  rabbirdv 2221  disjpss 2319  undif4 2325  opthpr 2485  dfiun2g 2586  elpwuni 2761  copsex4g 2794  opelopabg 2817  brabg 2818  dfid3 2836  oneqmini 3017  elsucg 3036  elsuc2g 3037  ordpwsuc 3066  dfom2 3133  opbrop 3238  opelcnvg 3296  dmsnop 3328  iss 3397  imasng 3424  cores 3499  cnvpo 3522  fncnv 3561  fununi 3563  fnssresb 3599  fnopabfv 3758  funimass4 3763  fnsnfv 3767  dmfco 3773  fvco 3774  fvopabn 3786  fvopab5 3793  elrnopabg 3800  fvimacnvi 3804  fvimacnvALT 3809  fressnfv 3838  funiunfv 3866  elunirnALT 3869  f1fv 3874  isoini 3900  f1oiso 3904  f1oweALT 3906  tfrlem1 3911  rdglim2 3949  eloprabg 4007  oprabval 4023  2ndconst 4097  dfoprab5 4115  elrnoprabg 4124  brecop 4306  mapsn 4345  ixp0 4361  xpsnen 4435  xpdom2 4442  pw2en 4446  mapxpen 4495  abfii4OLD 4564  fodomfibOLD 4567  noinfep 4640  rankbnd2 4704  aceq3lem 4732  zorn2 4796  fodomb 4800  brdom7disj 4804  brdom6disj 4805  domtri 4838  cardsdomel 4852  iscard2 4854  alephnbtwn 4868  nlt1pi 5033  ltsopq 5075  genpv 5102  ltsosr 5203  suppsrlem 5221  suppsr 5222  supsrlem6 5230  suprelem 5259  supre 5260  axrrecex 5284  renegcl 5416  ltxrt 5495  ltxrltt 5500  xrlenltt 5501  ssxr 5540  divdivdivt 5785  conjmult 5797  lerec 5880  lt2msq 5881  nn1suc 5939  infm3 6054  infmsup 6068  elznn0 6149  elnn0nn 6171  zltp1let 6181  primet 6195  dfuz 6202  rebtwnz 6222  ioo0t 6368  elioo3g 6380  snunioolem 6414  ioojoint 6416  elfz2t 6472  fzshftralt 6522  sq11 6626  dffsum 6998  caucvg3t 7168  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  ivthlem7 7287  tpsex 7605  istps 7606  bastop2 7643  islp2 7747  iscn 7758  iscnp 7760  ismsg 7800  metxp 7834  cncfmet 7905  bl2ioo 7911  iscau 7936  lmclim 7963  isring 8141  isvclem 8196  isnvlem 8229  isphg 8476  isph 8481  phoeqi 8518  spwpr2 8658  spwval 8659  spwnex 8661  shftefif1olem 8741  hhph 9045  sh2 9091  chocuni 9172  projlem15 9200  pjtheu2 9250  adjeqt 9859  elunop2t 9938  lnophmt 9944  cnlnadjeu 10010  adjbd1o 10018  jp 10197  mddmd 10236  chrelat 10291  chrelat2 10292  cvexchlem 10295  dmdbr5at 10349  cdjreu 10359  cdj3 10368  ficli 10472  ficliOLD 10473  cnvhmph 10527  homcard 10539  fgsb 10570  fgsbOLD 10571  fgsb2 10580  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem3 10589  rcfpfillem3OLD 10590  ismgra 10642  isalg 10653  isded 10669  iscat 10687  ishgrag 10769  ispgrag 10779

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 147  df-an 225

Copyright terms: Public domain