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  899  19.16  1553  19.19  1664  cbvab  2299  necon1bbiidc  2406  rspc2gv  2851  elabgt  2876  sbceq1a  2970  sbcralt  3037  sbcrext  3038  sbccsbg  3084  sbccsb2g  3085  iunpw  4474  tfis  4576  xp11m  5059  ressn  5161  fnssresb  5320  fun11iun  5474  funimass4  5558  dffo4  5656  f1ompt  5659  fliftf  5790  resoprab2  5962  ralrnmpo  5979  rexrnmpo  5980  1stconst  6212  2ndconst  6213  dfsmo2  6278  smoiso  6293  brecop  6615  ixpsnf1o  6726  ac6sfi  6888  ismkvnex  7143  nninfwlporlemd  7160  prarloclemn  7473  axcaucvglemres  7873  reapti  8510  indstr  9566  iccneg  9960  sqap0  10556  sqrt00  11017  minclpr  11213  fprodseq  11559  absefib  11746  efieq1re  11747  prmind2  12087  sincosq3sgn  13829  sincosq4sgn  13830  lgsdinn0  14029  pw1nct  14322  iswomninnlem  14367