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  2993  necon4abid  2995  uniiunlem  4034  r19.9rzv  4460  2reu4lem  4478  intprg  4940  inimasn  6141  fnresdisj  6647  fnsnfv  6952  f1oiso  7347  reldm  8038  rdglim2  8418  mptelixpg  8941  1idpr  11085  nndiv  12353  fz1sbc  13702  grpid  19147  isrnghm  20632  rnghmval2  20635  znleval  21821  fbunfip  24149  lmflf  24285  metcld2  25589  lgsne0  27625  sltssnb  28088  isuvtx  29909  loopclwwlkn1b  30566  clwwlknun  30636  frgrncvvdeqlem2  30834  isph  31357  ofpreima  33192  fdifsupp  33211  ressply1mon1p  34033  eulerpartlemd  34932  bnj168  35295  cardpred  35651  opelco3  36461  qdiffALT  38169  wl-2sb6d  38410  poimirlem26  38484  cnambfre  38506  heibor1  38664  opltn0  40167  cvrnbtwn2  40252  cvrnbtwn4  40256  atlltn0  40283  pmapjat1  40830  dih1dimatlem  42306  2rexfrabdioph  43741  dnwech  43993  rfovcnvf1od  44948  uneqsn  44969  lighneallem2  48613  stgredgiun  48978  isinito2lem  50528