Theorem bitr2id 287

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 286	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃))
4	3	bicomd 226	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bitr3di  289  necon1abid  2995  necon4abid  2997  uniiunlem  4040  r19.9rzv  4465  2reu4lem  4483  intprg  4945  inimasn  6152  fnresdisj  6655  fnsnfv  6960  f1oiso  7349  reldm  8039  rdglim2  8417  mptelixpg  8931  1idpr  11020  nndiv  12288  fz1sbc  13635  grpid  19048  isrnghm  20530  rnghmval2  20533  znleval  21715  fbunfip  24037  lmflf  24173  metcld2  25477  lgsne0  27510  sltssnb  27973  isuvtx  29756  loopclwwlkn1b  30404  clwwlknun  30474  frgrncvvdeqlem2  30662  isph  31185  ofpreima  33021  fdifsupp  33041  ressply1mon1p  33867  eulerpartlemd  34765  bnj168  35128  cardpred  35492  opelco3  36275  qdiffALT  38000  wl-2sb6d  38241  poimirlem26  38325  cnambfre  38347  heibor1  38489  opltn0  39992  cvrnbtwn2  40077  cvrnbtwn4  40081  atlltn0  40108  pmapjat1  40655  dih1dimatlem  42131  2rexfrabdioph  43551  dnwech  43803  rfovcnvf1od  44758  uneqsn  44779  lighneallem2  48386  stgredgiun  48751  isinito2lem  50304