Theorem bitr3id 194

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr3id.1	⊢ (𝜓 ↔ 𝜑)
bitr3id.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
bitr3id	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem bitr3id

Step	Hyp	Ref	Expression
1		bitr3id.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 132	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3id.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrid 192	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

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  911  19.16  1608  19.19  1718  cbvab  2364  necon1bbiidc  2481  rspc2gv  2942  elabgt  2967  sbceq1a  3061  sbcralt  3128  sbcrext  3129  sbccsbg  3176  sbccsb2g  3177  iunpw  4624  tfis  4728  reldmm  4998  xp11m  5224  ressn  5326  fnssresb  5493  fun11iun  5658  funimass4  5750  dffo4  5850  f1ompt  5853  dfimafnf  5949  fliftf  5999  resoprab2  6179  ralrnmpo  6197  rexrnmpo  6198  1stconst  6451  2ndconst  6452  dfsmo2  6552  smoiso  6567  brecop  6893  ixpsnf1o  7012  ac6sfi  7196  ismkvnex  7489  nninfwlporlemd  7506  prarloclemn  7860  axcaucvglemres  8260  reapti  8901  indstr  9976  iccneg  10374  sqap0  11026  wrdmap  11319  wrdind  11477  sqrt00  11789  minclpr  11986  fprodseq  12333  absefib  12521  efieq1re  12522  prmind2  12881  ballotfilemsima  13242  gzsumval2  13697  eqgval  14009  isnzr2  14474  sincosq3sgn  15912  sincosq4sgn  15913  fsumdvdsmul  16088  lgsdinn0  16150  pw1nct  17016  iswomninnlem  17073