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  907  19.16  1604  19.19  1714  cbvab  2360  necon1bbiidc  2475  rspc2gv  2935  elabgt  2960  sbceq1a  3054  sbcralt  3121  sbcrext  3122  sbccsbg  3169  sbccsb2g  3170  iunpw  4603  tfis  4707  reldmm  4977  xp11m  5203  ressn  5305  fnssresb  5472  fun11iun  5637  funimass4  5729  dffo4  5827  f1ompt  5830  fliftf  5974  resoprab2  6152  ralrnmpo  6170  rexrnmpo  6171  1stconst  6419  2ndconst  6420  dfsmo2  6520  smoiso  6535  brecop  6861  ixpsnf1o  6973  ac6sfi  7157  ismkvnex  7448  nninfwlporlemd  7465  prarloclemn  7819  axcaucvglemres  8219  reapti  8858  indstr  9931  iccneg  10328  sqap0  10975  wrdmap  11264  wrdind  11422  sqrt00  11733  minclpr  11930  fprodseq  12277  absefib  12465  efieq1re  12466  prmind2  12825  gsumval2  13631  eqgval  13961  isnzr2  14351  sincosq3sgn  15742  sincosq4sgn  15743  fsumdvdsmul  15908  lgsdinn0  15970  pw1nct  16826  iswomninnlem  16883