Theorem bitr3id 193

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 131	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3id.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	syl5bb 191	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr3g  221  ianordc  894  19.16  1548  19.19  1659  cbvab  2294  necon1bbiidc  2401  rspc2gv  2846  elabgt  2871  sbceq1a  2964  sbcralt  3031  sbcrext  3032  sbccsbg  3078  sbccsb2g  3079  iunpw  4465  tfis  4567  xp11m  5049  ressn  5151  fnssresb  5310  fun11iun  5463  funimass4  5547  dffo4  5644  f1ompt  5647  fliftf  5778  resoprab2  5950  ralrnmpo  5967  rexrnmpo  5968  1stconst  6200  2ndconst  6201  dfsmo2  6266  smoiso  6281  brecop  6603  ixpsnf1o  6714  ac6sfi  6876  ismkvnex  7131  nninfwlporlemd  7148  prarloclemn  7461  axcaucvglemres  7861  reapti  8498  indstr  9552  iccneg  9946  sqap0  10542  sqrt00  11004  minclpr  11200  fprodseq  11546  absefib  11733  efieq1re  11734  prmind2  12074  sincosq3sgn  13543  sincosq4sgn  13544  lgsdinn0  13743  pw1nct  14036  iswomninnlem  14081