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  904  19.16  1601  19.19  1712  cbvab  2353  necon1bbiidc  2461  rspc2gv  2919  elabgt  2944  sbceq1a  3038  sbcralt  3105  sbcrext  3106  sbccsbg  3153  sbccsb2g  3154  iunpw  4570  tfis  4674  reldmm  4941  xp11m  5166  ressn  5268  fnssresb  5434  fun11iun  5592  funimass4  5683  dffo4  5782  f1ompt  5785  fliftf  5922  resoprab2  6100  ralrnmpo  6118  rexrnmpo  6119  1stconst  6365  2ndconst  6366  dfsmo2  6431  smoiso  6446  brecop  6770  ixpsnf1o  6881  ac6sfi  7056  ismkvnex  7318  nninfwlporlemd  7335  prarloclemn  7682  axcaucvglemres  8082  reapti  8722  indstr  9784  iccneg  10181  sqap0  10823  wrdmap  11098  wrdind  11249  sqrt00  11546  minclpr  11743  fprodseq  12089  absefib  12277  efieq1re  12278  prmind2  12637  gsumval2  13425  eqgval  13755  isnzr2  14142  sincosq3sgn  15496  sincosq4sgn  15497  fsumdvdsmul  15659  lgsdinn0  15721  pw1nct  16328  iswomninnlem  16376