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  4038  r19.9rzv  4451  2reu4lem  4473  intprg  4933  inimasn  6111  fnresdisj  6609  fnsnfv  6910  f1oiso  7294  reldm  7985  rdglim2  8360  mptelixpg  8868  1idpr  10930  nndiv  12181  fz1sbc  13510  grpid  18898  isrnghm  20369  rnghmval2  20372  znleval  21501  fbunfip  23794  lmflf  23930  metcld2  25244  lgsne0  27283  ssltsnb  27742  isuvtx  29384  loopclwwlkn1b  30033  clwwlknun  30103  frgrncvvdeqlem2  30291  isph  30813  ofpreima  32658  fdifsupp  32677  ressply1mon1p  33542  eulerpartlemd  34390  bnj168  34753  cardpred  35114  opelco3  35830  wl-2sb6d  37613  poimirlem26  37696  cnambfre  37718  heibor1  37860  opltn0  39299  cvrnbtwn2  39384  cvrnbtwn4  39388  atlltn0  39415  pmapjat1  39962  dih1dimatlem  41438  2rexfrabdioph  42903  dnwech  43155  rfovcnvf1od  44111  uneqsn  44132  lighneallem2  47720  stgredgiun  48072  isinito2lem  49613