Theorem syl5bb 530

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

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

This theorem is referenced by:  syl5rbb 531  syl5bbr 532  3bitr4g 553  oplem1 770  19.23t 1112  sbcom 1253  necon3abid 1591  necon1abid 1610  r19.21t 1707  ceqsrexv 1880  ceqsrex2v 1881  elab2g 1891  elrabf 1895  eueq2 1909  reu8 1926  ru 1928  sbccomglem 1978  rabbirdv 2211  disjpss 2309  undif4 2315  opthpr 2476  dfiun2g 2576  elpwuni 2751  copsex4g 2784  opelopabg 2806  brabg 2807  dfid3 2826  oneqmini 3007  elsucg 3026  elsuc2g 3027  ordpwsuc 3056  dfom2 3123  opbrop 3228  opelcnvg 3285  dmsnop 3317  iss 3381  imasng 3408  cores 3485  cnvpo 3508  fncnv 3547  fununi 3549  fnssresb 3585  fnopabfv 3743  funimass4 3748  fnsnfv 3752  dmfco 3758  fvco 3759  fvopabn 3771  fvopab5 3778  elrnopabg 3785  fvimacnvi 3789  fvimacnvALT 3794  fressnfv 3823  funiunfv 3851  elunirnALT 3854  f1fv 3859  isoini 3885  f1oiso 3889  f1oweALT 3891  tfrlem1 3896  rdglim2 3934  eloprabg 3992  oprabval 4008  ndmoprgOLD 4029  2ndconst 4081  dfoprab5 4099  elrnoprabg 4108  brecop 4290  mapsn 4329  ixp0 4345  xpsnen 4415  xpdom2 4422  pw2en 4426  mapxpen 4475  abfii4 4538  fodomfib 4541  noinfep 4612  rankbnd2 4676  aceq3lem 4704  zorn2 4768  fodomb 4772  brdom7disj 4776  brdom6disj 4777  domtri 4810  cardsdomel 4824  iscard2 4826  alephnbtwn 4840  nlt1pi 5005  ltsopq 5047  genpv 5074  ltsosr 5175  suppsrlem 5193  suppsr 5194  supsrlem6 5202  suprelem 5231  supre 5232  axrrecex 5256  renegcl 5388  ltxrt 5467  ltxrltt 5472  xrlenltt 5473  ssxr 5513  divdivdivt 5741  conjmult 5753  lerec 5828  lt2msq 5829  nn1suc 5887  infm3 6001  infmsup 6015  elznn0 6096  elnn0nn 6118  zltp1let 6128  primet 6142  dfuz 6150  rebtwnz 6170  ioo0t 6305  elioo3g 6317  snunioolem 6347  elfz2t 6404  fzshftralt 6454  sq11 6557  dffsum 6936  caucvg3t 7104  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  ivthlem7 7222  ivthlem7OLD 7231  tpsex 7547  istps 7548  bastop2 7585  islp2 7688  iscn 7698  iscnp 7700  ismsg 7739  metxp 7774  cncfmet 7844  bl2ioo 7850  iscau 7874  lmclim 7898  isring 8078  isvcgOLD 8133  isvclem 8134  isnvlem 8167  isnvgOLD 8168  isphg 8407  isph 8412  phoeqi 8449  spwval 8582  shftefif1olem 8661  shftefif1olemOLD 8662  hhph 8966  sh2 9012  chocuni 9088  projlem15 9116  pjtheu2 9165  adjeqt 9775  elunop2t 9853  lnophmt 9859  cnlnadjeu 9925  adjbd1o 9933  jp 10107  mddmd 10144  chrelat 10199  chrelat2 10200  cvexchlem 10203  dmdbr5at 10255  cdjreu 10264  cdj3 10273  ficli 10368  cnvhmph 10414  homcard 10426  fgsb 10444  fgsb2 10449  cnfilca 10451  ismgra 10486  isalg 10497  isded 10513  iscat 10531  ishgrag 10605  ispgrag 10615

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