Theorem bitr3id 194

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 132	. 2 |- ( ph <-> ps )
3		bitr3id.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	bitrid 192	1 |- ( ch -> ( ph <-> th ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitr3g  222  imbibi  252  ianordc  900  19.16  1566  19.19  1677  cbvab  2317  necon1bbiidc  2425  rspc2gv  2876  elabgt  2901  sbceq1a  2995  sbcralt  3062  sbcrext  3063  sbccsbg  3109  sbccsb2g  3110  iunpw  4511  tfis  4615  xp11m  5104  ressn  5206  fnssresb  5366  fun11iun  5521  funimass4  5607  dffo4  5706  f1ompt  5709  fliftf  5842  resoprab2  6015  ralrnmpo  6033  rexrnmpo  6034  1stconst  6274  2ndconst  6275  dfsmo2  6340  smoiso  6355  brecop  6679  ixpsnf1o  6790  ac6sfi  6954  ismkvnex  7214  nninfwlporlemd  7231  prarloclemn  7559  axcaucvglemres  7959  reapti  8598  indstr  9658  iccneg  10055  sqap0  10677  wrdmap  10945  sqrt00  11184  minclpr  11380  fprodseq  11726  absefib  11914  efieq1re  11915  prmind2  12258  gsumval2  12980  eqgval  13293  isnzr2  13680  sincosq3sgn  14963  sincosq4sgn  14964  lgsdinn0  15164  pw1nct  15493  iswomninnlem  15539