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  904  19.16  1601  19.19  1712  cbvab  2353  necon1bbiidc  2461  rspc2gv  2919  elabgt  2944  sbceq1a  3038  sbcralt  3105  sbcrext  3106  sbccsbg  3153  sbccsb2g  3154  iunpw  4572  tfis  4676  reldmm  4945  xp11m  5170  ressn  5272  fnssresb  5438  fun11iun  5598  funimass4  5689  dffo4  5788  f1ompt  5791  fliftf  5932  resoprab2  6110  ralrnmpo  6128  rexrnmpo  6129  1stconst  6378  2ndconst  6379  dfsmo2  6444  smoiso  6459  brecop  6785  ixpsnf1o  6896  ac6sfi  7073  ismkvnex  7338  nninfwlporlemd  7355  prarloclemn  7702  axcaucvglemres  8102  reapti  8742  indstr  9805  iccneg  10202  sqap0  10845  wrdmap  11121  wrdind  11275  sqrt00  11572  minclpr  11769  fprodseq  12115  absefib  12303  efieq1re  12304  prmind2  12663  gsumval2  13451  eqgval  13781  isnzr2  14169  sincosq3sgn  15523  sincosq4sgn  15524  fsumdvdsmul  15686  lgsdinn0  15748  pw1nct  16482  iswomninnlem  16531