Theorem bitr3id 194

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
bitr3id	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem bitr3id

Step	Hyp	Ref	Expression
1		bitr3id.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 132	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3id.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrid 192	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:  3bitr3g  222  imbibi  252  ianordc  903  19.16  1581  19.19  1692  cbvab  2333  necon1bbiidc  2441  rspc2gv  2899  elabgt  2924  sbceq1a  3018  sbcralt  3085  sbcrext  3086  sbccsbg  3133  sbccsb2g  3134  iunpw  4548  tfis  4652  xp11m  5143  ressn  5245  fnssresb  5411  fun11iun  5569  funimass4  5657  dffo4  5756  f1ompt  5759  fliftf  5896  resoprab2  6072  ralrnmpo  6090  rexrnmpo  6091  1stconst  6337  2ndconst  6338  dfsmo2  6403  smoiso  6418  brecop  6742  ixpsnf1o  6853  ac6sfi  7028  ismkvnex  7290  nninfwlporlemd  7307  prarloclemn  7654  axcaucvglemres  8054  reapti  8694  indstr  9756  iccneg  10153  sqap0  10795  wrdmap  11069  wrdind  11220  sqrt00  11517  minclpr  11714  fprodseq  12060  absefib  12248  efieq1re  12249  prmind2  12608  gsumval2  13396  eqgval  13726  isnzr2  14113  sincosq3sgn  15467  sincosq4sgn  15468  fsumdvdsmul  15630  lgsdinn0  15692  pw1nct  16280  iswomninnlem  16328