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  1566  19.19  1677  cbvab  2317  necon1bbiidc  2425  rspc2gv  2877  elabgt  2902  sbceq1a  2996  sbcralt  3063  sbcrext  3064  sbccsbg  3110  sbccsb2g  3111  iunpw  4512  tfis  4616  xp11m  5105  ressn  5207  fnssresb  5367  fun11iun  5522  funimass4  5608  dffo4  5707  f1ompt  5710  fliftf  5843  resoprab2  6016  ralrnmpo  6034  rexrnmpo  6035  1stconst  6276  2ndconst  6277  dfsmo2  6342  smoiso  6357  brecop  6681  ixpsnf1o  6792  ac6sfi  6956  ismkvnex  7216  nninfwlporlemd  7233  prarloclemn  7561  axcaucvglemres  7961  reapti  8600  indstr  9661  iccneg  10058  sqap0  10680  wrdmap  10948  sqrt00  11187  minclpr  11383  fprodseq  11729  absefib  11917  efieq1re  11918  prmind2  12261  gsumval2  12983  eqgval  13296  isnzr2  13683  sincosq3sgn  15004  sincosq4sgn  15005  lgsdinn0  15205  pw1nct  15563  iswomninnlem  15609