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  2968  necon4abid  2970  uniiunlem  4020  r19.9rzv  4435  2reu4lem  4453  intprg  4913  inimasn  6109  fnresdisj  6607  fnsnfv  6908  f1oiso  7295  reldm  7986  rdglim2  8360  mptelixpg  8872  1idpr  10941  nndiv  12212  fz1sbc  13543  grpid  18940  isrnghm  20410  rnghmval2  20413  znleval  21523  fbunfip  23822  lmflf  23958  metcld2  25262  lgsne0  27286  sltssnb  27749  isuvtx  29452  loopclwwlkn1b  30100  clwwlknun  30170  frgrncvvdeqlem2  30358  isph  30881  ofpreima  32726  fdifsupp  32746  ressply1mon1p  33616  eulerpartlemd  34498  bnj168  34861  cardpred  35223  opelco3  35945  qdiffALT  37630  wl-2sb6d  37871  poimirlem26  37955  cnambfre  37977  heibor1  38119  opltn0  39624  cvrnbtwn2  39709  cvrnbtwn4  39713  atlltn0  39740  pmapjat1  40287  dih1dimatlem  41763  2rexfrabdioph  43212  dnwech  43464  rfovcnvf1od  44419  uneqsn  44440  lighneallem2  48057  stgredgiun  48422  isinito2lem  49961