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 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  2974  necon4abid  2976  uniiunlem  4080  r19.9rzv  4495  2reu4lem  4521  intprg  4979  inimasn  6154  fnresdisj  6669  fnsnfv  6971  f1oiso  7353  reldm  8042  rdglim2  8446  mptelixpg  8945  1idpr  11044  nndiv  12280  fz1sbc  13601  grpid  18923  isrnghm  20369  rnghmval2  20372  znleval  21475  fbunfip  23760  lmflf  23896  metcld2  25222  lgsne0  27255  isuvtx  29195  loopclwwlkn1b  29839  clwwlknun  29909  frgrncvvdeqlem2  30097  isph  30619  ofpreima  32434  ressply1mon1p  33179  eulerpartlemd  33922  bnj168  34297  cardpred  34649  opelco3  35306  wl-2sb6d  36960  poimirlem26  37054  cnambfre  37076  heibor1  37218  opltn0  38599  cvrnbtwn2  38684  cvrnbtwn4  38688  atlltn0  38715  pmapjat1  39263  dih1dimatlem  40739  2rexfrabdioph  42138  dnwech  42394  rfovcnvf1od  43357  uneqsn  43378  lighneallem2  46869