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  1569  19.19  1680  cbvab  2320  necon1bbiidc  2428  rspc2gv  2880  elabgt  2905  sbceq1a  2999  sbcralt  3066  sbcrext  3067  sbccsbg  3113  sbccsb2g  3114  iunpw  4516  tfis  4620  xp11m  5109  ressn  5211  fnssresb  5373  fun11iun  5528  funimass4  5614  dffo4  5713  f1ompt  5716  fliftf  5849  resoprab2  6023  ralrnmpo  6041  rexrnmpo  6042  1stconst  6288  2ndconst  6289  dfsmo2  6354  smoiso  6369  brecop  6693  ixpsnf1o  6804  ac6sfi  6968  ismkvnex  7230  nninfwlporlemd  7247  prarloclemn  7583  axcaucvglemres  7983  reapti  8623  indstr  9684  iccneg  10081  sqap0  10715  wrdmap  10983  sqrt00  11222  minclpr  11419  fprodseq  11765  absefib  11953  efieq1re  11954  prmind2  12313  gsumval2  13099  eqgval  13429  isnzr2  13816  sincosq3sgn  15148  sincosq4sgn  15149  fsumdvdsmul  15311  lgsdinn0  15373  pw1nct  15734  iswomninnlem  15780