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  904  19.16  1601  19.19  1712  cbvab  2353  necon1bbiidc  2461  rspc2gv  2919  elabgt  2944  sbceq1a  3038  sbcralt  3105  sbcrext  3106  sbccsbg  3153  sbccsb2g  3154  iunpw  4571  tfis  4675  reldmm  4942  xp11m  5167  ressn  5269  fnssresb  5435  fun11iun  5595  funimass4  5686  dffo4  5785  f1ompt  5788  fliftf  5929  resoprab2  6107  ralrnmpo  6125  rexrnmpo  6126  1stconst  6373  2ndconst  6374  dfsmo2  6439  smoiso  6454  brecop  6780  ixpsnf1o  6891  ac6sfi  7068  ismkvnex  7330  nninfwlporlemd  7347  prarloclemn  7694  axcaucvglemres  8094  reapti  8734  indstr  9796  iccneg  10193  sqap0  10836  wrdmap  11111  wrdind  11262  sqrt00  11559  minclpr  11756  fprodseq  12102  absefib  12290  efieq1re  12291  prmind2  12650  gsumval2  13438  eqgval  13768  isnzr2  14156  sincosq3sgn  15510  sincosq4sgn  15511  fsumdvdsmul  15673  lgsdinn0  15735  pw1nct  16398  iswomninnlem  16447