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  907  19.16  1604  19.19  1714  cbvab  2358  necon1bbiidc  2473  rspc2gv  2932  elabgt  2957  sbceq1a  3051  sbcralt  3118  sbcrext  3119  sbccsbg  3166  sbccsb2g  3167  iunpw  4600  tfis  4704  reldmm  4974  xp11m  5200  ressn  5302  fnssresb  5469  fun11iun  5634  funimass4  5726  dffo4  5824  f1ompt  5827  fliftf  5971  resoprab2  6149  ralrnmpo  6167  rexrnmpo  6168  1stconst  6416  2ndconst  6417  dfsmo2  6517  smoiso  6532  brecop  6858  ixpsnf1o  6970  ac6sfi  7154  ismkvnex  7445  nninfwlporlemd  7462  prarloclemn  7813  axcaucvglemres  8213  reapti  8852  indstr  9924  iccneg  10321  sqap0  10967  wrdmap  11252  wrdind  11410  sqrt00  11721  minclpr  11918  fprodseq  12265  absefib  12453  efieq1re  12454  prmind2  12813  gsumval2  13602  eqgval  13932  isnzr2  14321  sincosq3sgn  15685  sincosq4sgn  15686  fsumdvdsmul  15851  lgsdinn0  15913  pw1nct  16769  iswomninnlem  16826