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  900  19.16  1569  19.19  1680  cbvab  2320  necon1bbiidc  2428  rspc2gv  2880  elabgt  2905  sbceq1a  2999  sbcralt  3066  sbcrext  3067  sbccsbg  3113  sbccsb2g  3114  iunpw  4515  tfis  4619  xp11m  5108  ressn  5210  fnssresb  5370  fun11iun  5525  funimass4  5611  dffo4  5710  f1ompt  5713  fliftf  5846  resoprab2  6019  ralrnmpo  6037  rexrnmpo  6038  1stconst  6279  2ndconst  6280  dfsmo2  6345  smoiso  6360  brecop  6684  ixpsnf1o  6795  ac6sfi  6959  ismkvnex  7221  nninfwlporlemd  7238  prarloclemn  7566  axcaucvglemres  7966  reapti  8606  indstr  9667  iccneg  10064  sqap0  10698  wrdmap  10966  sqrt00  11205  minclpr  11402  fprodseq  11748  absefib  11936  efieq1re  11937  prmind2  12288  gsumval2  13040  eqgval  13353  isnzr2  13740  sincosq3sgn  15064  sincosq4sgn  15065  fsumdvdsmul  15227  lgsdinn0  15289  pw1nct  15647  iswomninnlem  15693