Theorem syl5bb 534

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

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

This theorem is referenced by:  syl5rbb 535  syl5bbr 536  3bitr4g 557  oplem1 774  19.23t 1118  sbcom 1260  necon3abid 1602  necon1abid 1621  r19.21t 1718  ceqsrexv 1892  ceqsrex2v 1893  elab2g 1903  elrabf 1907  eueq2 1921  reu8 1939  ru 1941  sbccomglem 1991  rabbirdv 2224  disjpss 2323  undif4 2329  opthpr 2489  dfiun2g 2590  elpwuni 2767  copsex4g 2800  opelopabg 2823  brabg 2824  dfid3 2842  oneqmini 3023  elsucg 3042  elsuc2g 3043  ordpwsuc 3072  dfom2 3139  opbrop 3244  opelcnvg 3302  dmsnop 3334  iss 3403  imasng 3430  cores 3505  cnvpo 3528  fncnv 3567  fununi 3569  fnssresb 3605  fnopabfv 3764  funimass4 3769  fnsnfv 3773  dmfco 3779  fvco 3780  fvopabn 3792  fvopab5 3799  elrnopabg 3806  fvimacnvi 3810  fvimacnvALT 3815  fressnfv 3844  funiunfv 3872  elunirnALT 3875  f1fv 3880  isoini 3906  f1oiso 3910  f1oweALT 3912  tfrlem1 3917  rdglim2 3955  eloprabg 4013  oprabval 4029  2ndconst 4103  dfoprab5 4121  elrnoprabg 4130  brecop 4312  mapsn 4351  ixp0 4367  xpsnen 4441  xpdom2 4448  pw2en 4452  mapxpen 4501  noinfep 4650  rankbnd2 4714  aceq3lem 4742  zorn2 4806  fodomb 4810  brdom7disj 4814  brdom6disj 4815  domtri 4848  cardsdomel 4863  iscard2 4865  alephnbtwn 4879  nlt1pi 5045  ltsopq 5087  genpv 5114  ltsosr 5215  suppsrlem 5233  suppsr 5234  supsrlem6 5242  suprelem 5271  supre 5272  axrrecex 5296  renegcl 5428  ltxrt 5507  ltxrltt 5512  xrlenltt 5513  ssxr 5552  divdivdivt 5787  conjmult 5799  lerec 5882  lt2msq 5883  nn1suc 5941  infm3 6056  infmsup 6070  elznn0 6151  elnn0nn 6173  zltp1let 6183  primet 6197  dfuz 6204  rebtwnz 6224  ioo0t 6369  elioo3g 6381  snunioolem 6415  ioojoint 6417  elfz2t 6473  fzshftralt 6523  sq11 6627  dffsum 6998  caucvg3t 7168  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  ivthlem7 7287  tpsex 7606  istps 7607  bastop2 7642  islp2 7744  iscn 7755  iscnp 7757  ismsg 7797  metxp 7831  cncfmet 7902  bl2ioo 7908  iscau 7933  lmclim 7960  isring 8137  isvclem 8192  isnvlem 8225  isphg 8472  isph 8477  phoeqi 8514  spwpr2 8654  spwval 8655  spwnex 8657  shftefif1olem 8736  hhph 9040  sh2 9086  chocuni 9167  projlem15 9195  pjtheu2 9245  adjeqt 9854  elunop2t 9933  lnophmt 9939  cnlnadjeu 10005  adjbd1o 10013  jp 10192  mddmd 10231  chrelat 10286  chrelat2 10287  cvexchlem 10290  dmdbr5at 10344  cdjreu 10354  cdj3 10363  ficli 10462  cnvhmph 10513  homcard 10525  fgsb 10555  fgsb2 10560  cnfilca 10562  rcfpfillem3 10565  ismgra 10613  isalg 10624  isded 10640  iscat 10658  ishgrag 10740  ispgrag 10750

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