Theorem bitr4id 199

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

Ref	Expression
bitr4id.2	⊢ (𝜓 ↔ 𝜒)
bitr4id.1	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
bitr4id	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4id

Step	Hyp	Ref	Expression
1		bitr4id.1	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
2		bitr4id.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	2	bicomi 132	. 2 ⊢ (𝜒 ↔ 𝜓)
4	1, 3	bitr2di 197	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imimorbdc  904  baib  927  pm5.6dc  934  ifptru  998  ifpfal  999  xornbidc  1436  mo2dc  2138  reu8  3016  sbc6g  3070  dfss4st  3458  r19.28m  3603  r19.45mv  3607  r19.44mv  3608  r19.27m  3609  ralsnsg  3731  ralsns  3732  eldifvsn  3831  iunconstm  4004  iinconstm  4005  exmidsssnc  4321  unisucg  4540  relsng  4858  funssres  5400  fncnv  5427  dff1o5  5628  funimass4  5732  fneqeql2  5792  fnniniseg2  5806  unpreima  5807  dffo3  5829  funfvima  5923  dff13  5947  f1eqcocnv  5970  fliftf  5978  isocnv2  5991  eloprabga  6148  mpo2eqb  6171  opabex3d  6323  opabex3  6324  elxp6  6376  elxp7  6377  mptsuppd  6469  sbthlemi5  7244  sbthlemi6  7245  nninfwlporlemd  7476  genpdflem  7838  ltnqpr  7924  ltexprlemloc  7938  xrlenlt  8354  negcon2  8543  dfinfre  9250  sup3exmid  9251  elznn  9613  zq  9979  rpnegap  10040  infssuzex  10618  modqmuladdnn0  10757  shftdm  11535  rexfiuz  11702  rexanuz2  11704  sumsplitdc  12146  fsum2dlemstep  12148  odd2np1  12587  divalgb  12639  nninfctlemfo  12764  isprm4  12844  ctiunctlemudc  13275  grp1  13864  nmznsg  13969  qusecsub  14087  iscrng2  14261  opprsubgg  14331  opprsubrngg  14460  domnmuln0  14523  ringunitsap0  14535  drnguiap  14550  tx1cn  15263  tx2cn  15264  cnbl0  15528  cnblcld  15529  reopnap  15540  pilem1  15773  sinq34lt0t  15825  gausslemma2dlem1a  16060  vtxd0nedgbfi  16423