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 282	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃))
4	3	bicomd 222	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bitr3di  286  necon1abid  2984  necon4abid  2986  uniiunlem  4024  r19.9rzv  4436  2reu4lem  4462  intprg  4918  inimasn  6057  fnresdisj  6549  fnsnfv  6842  f1oiso  7216  reldm  7872  rdglim2  8248  mptelixpg  8698  1idpr  10778  nndiv  12011  fz1sbc  13323  grpid  18605  znleval  20752  fbunfip  23010  lmflf  23146  metcld2  24461  lgsne0  26473  isuvtx  27752  loopclwwlkn1b  28394  clwwlknun  28464  frgrncvvdeqlem2  28652  isph  29172  ofpreima  30990  eulerpartlemd  32321  bnj168  32697  cardpred  33050  opelco3  33737  wl-2sb6d  35701  poimirlem26  35791  cnambfre  35813  heibor1  35956  opltn0  37192  cvrnbtwn2  37277  cvrnbtwn4  37281  atlltn0  37308  pmapjat1  37855  dih1dimatlem  39331  2rexfrabdioph  40607  dnwech  40862  rfovcnvf1od  41574  uneqsn  41595  lighneallem2  45019  isrnghm  45411  rnghmval2  45414