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  901  19.16  1579  19.19  1690  cbvab  2330  necon1bbiidc  2438  rspc2gv  2890  elabgt  2915  sbceq1a  3009  sbcralt  3076  sbcrext  3077  sbccsbg  3123  sbccsb2g  3124  iunpw  4531  tfis  4635  xp11m  5126  ressn  5228  fnssresb  5393  fun11iun  5550  funimass4  5636  dffo4  5735  f1ompt  5738  fliftf  5875  resoprab2  6049  ralrnmpo  6067  rexrnmpo  6068  1stconst  6314  2ndconst  6315  dfsmo2  6380  smoiso  6395  brecop  6719  ixpsnf1o  6830  ac6sfi  7002  ismkvnex  7264  nninfwlporlemd  7281  prarloclemn  7619  axcaucvglemres  8019  reapti  8659  indstr  9721  iccneg  10118  sqap0  10758  wrdmap  11032  sqrt00  11395  minclpr  11592  fprodseq  11938  absefib  12126  efieq1re  12127  prmind2  12486  gsumval2  13273  eqgval  13603  isnzr2  13990  sincosq3sgn  15344  sincosq4sgn  15345  fsumdvdsmul  15507  lgsdinn0  15569  pw1nct  16014  iswomninnlem  16062