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  4568  tfis  4672  xp11m  5163  ressn  5265  fnssresb  5431  fun11iun  5589  funimass4  5677  dffo4  5776  f1ompt  5779  fliftf  5916  resoprab2  6092  ralrnmpo  6110  rexrnmpo  6111  1stconst  6357  2ndconst  6358  dfsmo2  6423  smoiso  6438  brecop  6762  ixpsnf1o  6873  ac6sfi  7048  ismkvnex  7310  nninfwlporlemd  7327  prarloclemn  7674  axcaucvglemres  8074  reapti  8714  indstr  9776  iccneg  10173  sqap0  10815  wrdmap  11089  wrdind  11240  sqrt00  11537  minclpr  11734  fprodseq  12080  absefib  12268  efieq1re  12269  prmind2  12628  gsumval2  13416  eqgval  13746  isnzr2  14133  sincosq3sgn  15487  sincosq4sgn  15488  fsumdvdsmul  15650  lgsdinn0  15712  pw1nct  16300  iswomninnlem  16348