Theorem syl5bb 410

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 7	. 2 |- (ph -> (th <-> ps))
3		syl5bb.1	. 2 |- (ph -> (ps <-> ch))
4	2, 3	bitrd 406	1 |- (ph -> (th <-> ch))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  syl5rbb 411  syl5bbr 412  3bitr4g 428  oplem1 578  19.16 730  19.19 737  sbcom 916  ceqsrexv 1413  elab2g 1418  elrabf 1421  eueq2 1429  ru 1437  birabrdv 1648  disjpss 1738  undif4 1744  r19.36zv 1772  copsex4g 1904  brabg 2116  oneqmini 2272  elsucg 2290  elsuc2g 2291  onpwsuc 2315  dfom2 2374  opbrop 2472  opelcnvg 2517  dmsnop 2547  resieq 2581  iss 2599  imasn 2616  cores 2659  fununi 2705  fnopabfv 2858  fnsnfv 2861  dmfco 2864  fvco 2865  fvopabn 2873  fressnfv 2898  f1fv 2916  isoini 2938  f1oiso 2942  f1oweOLD 2944  tfrlem1 2949  rdglim2 2987  eloprabg 3035  oprabval 3047  ndmoprg 3057  brecop 3242  mapsn 3269  xpsnen 3339  xpdom2 3345  pw2en 3348  mapxpen 3390  aceq3lem 3555  zorn 3611  fodomb 3615  domtri 3644  cardsdomel 3658  iscard2 3660  alephnbtwn 3674  nlt1pi 3827  ltsopq 3869  genpv 3896  ltsosr 3997  suppsrlem 4015  suppsr 4016  supsrlem6 4024  suprelem 4053  supre 4054  axrrecex 4081  renegcl 4171  divdivdivt 4265  leltt 4278  lerec 4411  lt2sq 4414  nn1suc 4435  elznn0 4576  elnn0nn 4593  zltp1let 4597  rebtwnz 4620  sqe11 4702  znnen 4930  sh2 5126  chocuni 5179  projlem15 5207  jp 5703  chrelat 5757  chrelat2 5758  cvexchlem 5759

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org