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  2979  necon4abid  2981  uniiunlem  4087  r19.9rzv  4500  2reu4lem  4522  intprg  4981  inimasn  6176  fnresdisj  6688  fnsnfv  6988  f1oiso  7371  reldm  8069  rdglim2  8472  mptelixpg  8975  1idpr  11069  nndiv  12312  fz1sbc  13640  grpid  18993  isrnghm  20441  rnghmval2  20444  znleval  21573  fbunfip  23877  lmflf  24013  metcld2  25341  lgsne0  27379  isuvtx  29412  loopclwwlkn1b  30061  clwwlknun  30131  frgrncvvdeqlem2  30319  isph  30841  ofpreima  32675  fdifsupp  32694  ressply1mon1p  33593  eulerpartlemd  34368  bnj168  34744  cardpred  35104  opelco3  35775  wl-2sb6d  37559  poimirlem26  37653  cnambfre  37675  heibor1  37817  opltn0  39191  cvrnbtwn2  39276  cvrnbtwn4  39280  atlltn0  39307  pmapjat1  39855  dih1dimatlem  41331  2rexfrabdioph  42807  dnwech  43060  rfovcnvf1od  44017  uneqsn  44038  lighneallem2  47593  stgredgiun  47925