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  900  19.16  1565  19.19  1676  cbvab  2311  necon1bbiidc  2418  rspc2gv  2865  elabgt  2890  sbceq1a  2984  sbcralt  3051  sbcrext  3052  sbccsbg  3098  sbccsb2g  3099  iunpw  4492  tfis  4594  xp11m  5079  ressn  5181  fnssresb  5340  fun11iun  5494  funimass4  5579  dffo4  5677  f1ompt  5680  fliftf  5813  resoprab2  5985  ralrnmpo  6003  rexrnmpo  6004  1stconst  6236  2ndconst  6237  dfsmo2  6302  smoiso  6317  brecop  6639  ixpsnf1o  6750  ac6sfi  6912  ismkvnex  7167  nninfwlporlemd  7184  prarloclemn  7512  axcaucvglemres  7912  reapti  8550  indstr  9607  iccneg  10003  sqap0  10601  sqrt00  11063  minclpr  11259  fprodseq  11605  absefib  11792  efieq1re  11793  prmind2  12134  eqgval  13115  sincosq3sgn  14545  sincosq4sgn  14546  lgsdinn0  14745  pw1nct  15049  iswomninnlem  15094