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  4050  r19.9rzv  4463  2reu4lem  4485  intprg  4945  inimasn  6129  fnresdisj  6638  fnsnfv  6940  f1oiso  7326  reldm  8023  rdglim2  8400  mptelixpg  8908  1idpr  10982  nndiv  12232  fz1sbc  13561  grpid  18907  isrnghm  20350  rnghmval2  20353  znleval  21464  fbunfip  23756  lmflf  23892  metcld2  25207  lgsne0  27246  isuvtx  29322  loopclwwlkn1b  29971  clwwlknun  30041  frgrncvvdeqlem2  30229  isph  30751  ofpreima  32589  fdifsupp  32608  ressply1mon1p  33537  eulerpartlemd  34357  bnj168  34720  cardpred  35080  opelco3  35762  wl-2sb6d  37546  poimirlem26  37640  cnambfre  37662  heibor1  37804  opltn0  39183  cvrnbtwn2  39268  cvrnbtwn4  39272  atlltn0  39299  pmapjat1  39847  dih1dimatlem  41323  2rexfrabdioph  42784  dnwech  43037  rfovcnvf1od  43993  uneqsn  44014  lighneallem2  47607  stgredgiun  47957  isinito2lem  49487