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  2964  necon4abid  2966  uniiunlem  4035  r19.9rzv  4448  2reu4lem  4470  intprg  4929  inimasn  6100  fnresdisj  6597  fnsnfv  6896  f1oiso  7280  reldm  7971  rdglim2  8346  mptelixpg  8854  1idpr  10912  nndiv  12163  fz1sbc  13492  grpid  18880  isrnghm  20352  rnghmval2  20355  znleval  21484  fbunfip  23777  lmflf  23913  metcld2  25227  lgsne0  27266  ssltsnb  27725  isuvtx  29366  loopclwwlkn1b  30012  clwwlknun  30082  frgrncvvdeqlem2  30270  isph  30792  ofpreima  32637  fdifsupp  32656  ressply1mon1p  33521  eulerpartlemd  34369  bnj168  34732  cardpred  35092  opelco3  35787  wl-2sb6d  37571  poimirlem26  37665  cnambfre  37687  heibor1  37829  opltn0  39208  cvrnbtwn2  39293  cvrnbtwn4  39297  atlltn0  39324  pmapjat1  39871  dih1dimatlem  41347  2rexfrabdioph  42808  dnwech  43060  rfovcnvf1od  44016  uneqsn  44037  lighneallem2  47616  stgredgiun  47968  isinito2lem  49509