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  889  19.16  1543  19.19  1654  cbvab  2290  necon1bbiidc  2397  rspc2gv  2842  elabgt  2867  sbceq1a  2960  sbcralt  3027  sbcrext  3028  sbccsbg  3074  sbccsb2g  3075  iunpw  4458  tfis  4560  xp11m  5042  ressn  5144  fnssresb  5300  fun11iun  5453  funimass4  5537  dffo4  5633  f1ompt  5636  fliftf  5767  resoprab2  5939  ralrnmpo  5956  rexrnmpo  5957  1stconst  6189  2ndconst  6190  dfsmo2  6255  smoiso  6270  brecop  6591  ixpsnf1o  6702  ac6sfi  6864  ismkvnex  7119  prarloclemn  7440  axcaucvglemres  7840  reapti  8477  indstr  9531  iccneg  9925  sqap0  10521  sqrt00  10982  minclpr  11178  fprodseq  11524  absefib  11711  efieq1re  11712  prmind2  12052  sincosq3sgn  13389  sincosq4sgn  13390  lgsdinn0  13589  pw1nct  13883  iswomninnlem  13928