Theorem bitr2id 284

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

Hypotheses

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

Assertion

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

Proof of Theorem bitr2id

Step	Hyp	Ref	Expression
1		bitr2id.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		bitr2id.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	bitrid 283	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃))
4	3	bicomd 223	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  bitr3di  286  necon1abid  2963  necon4abid  2965  uniiunlem  4040  r19.9rzv  4453  2reu4lem  4475  intprg  4934  inimasn  6109  fnresdisj  6606  fnsnfv  6906  f1oiso  7292  reldm  7986  rdglim2  8361  mptelixpg  8869  1idpr  10942  nndiv  12192  fz1sbc  13521  grpid  18872  isrnghm  20344  rnghmval2  20347  znleval  21479  fbunfip  23772  lmflf  23908  metcld2  25223  lgsne0  27262  isuvtx  29358  loopclwwlkn1b  30004  clwwlknun  30074  frgrncvvdeqlem2  30262  isph  30784  ofpreima  32622  fdifsupp  32641  ressply1mon1p  33513  eulerpartlemd  34333  bnj168  34696  cardpred  35056  opelco3  35747  wl-2sb6d  37531  poimirlem26  37625  cnambfre  37647  heibor1  37789  opltn0  39168  cvrnbtwn2  39253  cvrnbtwn4  39257  atlltn0  39284  pmapjat1  39832  dih1dimatlem  41308  2rexfrabdioph  42769  dnwech  43021  rfovcnvf1od  43977  uneqsn  43998  lighneallem2  47591  stgredgiun  47941  isinito2lem  49471