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  2978  necon4abid  2980  uniiunlem  4084  r19.9rzv  4499  2reu4lem  4525  intprg  4985  inimasn  6155  fnresdisj  6670  fnsnfv  6970  f1oiso  7351  reldm  8034  rdglim2  8438  mptelixpg  8935  1idpr  11030  nndiv  12265  fz1sbc  13584  grpid  18903  isrnghm  20339  rnghmval2  20342  znleval  21421  fbunfip  23694  lmflf  23830  metcld2  25156  lgsne0  27183  isuvtx  29087  loopclwwlkn1b  29730  clwwlknun  29800  frgrncvvdeqlem2  29988  isph  30510  ofpreima  32325  ressply1mon1p  33099  eulerpartlemd  33831  bnj168  34207  cardpred  34559  opelco3  35218  wl-2sb6d  36890  poimirlem26  36981  cnambfre  37003  heibor1  37145  opltn0  38527  cvrnbtwn2  38612  cvrnbtwn4  38616  atlltn0  38643  pmapjat1  39191  dih1dimatlem  40667  2rexfrabdioph  42000  dnwech  42256  rfovcnvf1od  43221  uneqsn  43242  lighneallem2  46736