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  2971  necon4abid  2973  uniiunlem  4028  r19.9rzv  4446  2reu4lem  4464  intprg  4924  inimasn  6112  fnresdisj  6610  fnsnfv  6911  f1oiso  7297  reldm  7988  rdglim2  8362  mptelixpg  8874  1idpr  10941  nndiv  12192  fz1sbc  13517  grpid  18909  isrnghm  20379  rnghmval2  20382  znleval  21511  fbunfip  23812  lmflf  23948  metcld2  25252  lgsne0  27286  sltssnb  27749  isuvtx  29452  loopclwwlkn1b  30101  clwwlknun  30171  frgrncvvdeqlem2  30359  isph  30882  ofpreima  32727  fdifsupp  32747  ressply1mon1p  33633  eulerpartlemd  34516  bnj168  34879  cardpred  35241  opelco3  35963  wl-2sb6d  37874  poimirlem26  37958  cnambfre  37980  heibor1  38122  opltn0  39627  cvrnbtwn2  39712  cvrnbtwn4  39716  atlltn0  39743  pmapjat1  40290  dih1dimatlem  41766  2rexfrabdioph  43227  dnwech  43479  rfovcnvf1od  44434  uneqsn  44455  lighneallem2  48040  stgredgiun  48392  isinito2lem  49931