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  906  19.16  1603  19.19  1714  cbvab  2355  necon1bbiidc  2463  rspc2gv  2922  elabgt  2947  sbceq1a  3041  sbcralt  3108  sbcrext  3109  sbccsbg  3156  sbccsb2g  3157  iunpw  4577  tfis  4681  reldmm  4950  xp11m  5175  ressn  5277  fnssresb  5444  fun11iun  5604  funimass4  5696  dffo4  5795  f1ompt  5798  fliftf  5940  resoprab2  6118  ralrnmpo  6136  rexrnmpo  6137  1stconst  6386  2ndconst  6387  dfsmo2  6453  smoiso  6468  brecop  6794  ixpsnf1o  6905  ac6sfi  7087  ismkvnex  7354  nninfwlporlemd  7371  prarloclemn  7719  axcaucvglemres  8119  reapti  8759  indstr  9827  iccneg  10224  sqap0  10869  wrdmap  11149  wrdind  11307  sqrt00  11605  minclpr  11802  fprodseq  12149  absefib  12337  efieq1re  12338  prmind2  12697  gsumval2  13485  eqgval  13815  isnzr2  14204  sincosq3sgn  15558  sincosq4sgn  15559  fsumdvdsmul  15721  lgsdinn0  15783  pw1nct  16630  iswomninnlem  16679