Theorem bitr3id 193

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr3id.1	|- ( ps <-> ph )
bitr3id.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
bitr3id	|- ( ch -> ( ph <-> th ) )

Proof of Theorem bitr3id

Step	Hyp	Ref	Expression
1		bitr3id.1	. . 3 |- ( ps <-> ph )
2	1	bicomi 131	. 2 |- ( ph <-> ps )
3		bitr3id.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	syl5bb 191	1 |- ( ch -> ( ph <-> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr3g  221  ianordc  885  19.16  1532  19.19  1643  cbvab  2278  necon1bbiidc  2385  rspc2gv  2825  elabgt  2849  sbceq1a  2942  sbcralt  3009  sbcrext  3010  sbccsbg  3056  sbccsb2g  3057  iunpw  4434  tfis  4536  xp11m  5017  ressn  5119  fnssresb  5275  fun11iun  5428  funimass4  5512  dffo4  5608  f1ompt  5611  fliftf  5740  resoprab2  5908  ralrnmpo  5925  rexrnmpo  5926  1stconst  6158  2ndconst  6159  dfsmo2  6224  smoiso  6239  brecop  6559  ixpsnf1o  6670  ac6sfi  6832  ismkvnex  7077  prarloclemn  7398  axcaucvglemres  7798  reapti  8433  indstr  9483  iccneg  9871  sqap0  10463  sqrt00  10917  minclpr  11113  fprodseq  11457  absefib  11644  efieq1re  11645  prmind2  11968  sincosq3sgn  13088  sincosq4sgn  13089  pw1nct  13514  iswomninnlem  13561