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  4053  r19.9rzv  4466  2reu4lem  4488  intprg  4948  inimasn  6132  fnresdisj  6641  fnsnfv  6943  f1oiso  7329  reldm  8026  rdglim2  8403  mptelixpg  8911  1idpr  10989  nndiv  12239  fz1sbc  13568  grpid  18914  isrnghm  20357  rnghmval2  20360  znleval  21471  fbunfip  23763  lmflf  23899  metcld2  25214  lgsne0  27253  isuvtx  29329  loopclwwlkn1b  29978  clwwlknun  30048  frgrncvvdeqlem2  30236  isph  30758  ofpreima  32596  fdifsupp  32615  ressply1mon1p  33544  eulerpartlemd  34364  bnj168  34727  cardpred  35087  opelco3  35769  wl-2sb6d  37553  poimirlem26  37647  cnambfre  37669  heibor1  37811  opltn0  39190  cvrnbtwn2  39275  cvrnbtwn4  39279  atlltn0  39306  pmapjat1  39854  dih1dimatlem  41330  2rexfrabdioph  42791  dnwech  43044  rfovcnvf1od  44000  uneqsn  44021  lighneallem2  47611  stgredgiun  47961  isinito2lem  49491