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  899  19.16  1555  19.19  1666  cbvab  2301  necon1bbiidc  2408  rspc2gv  2855  elabgt  2880  sbceq1a  2974  sbcralt  3041  sbcrext  3042  sbccsbg  3088  sbccsb2g  3089  iunpw  4482  tfis  4584  xp11m  5069  ressn  5171  fnssresb  5330  fun11iun  5484  funimass4  5568  dffo4  5666  f1ompt  5669  fliftf  5802  resoprab2  5974  ralrnmpo  5991  rexrnmpo  5992  1stconst  6224  2ndconst  6225  dfsmo2  6290  smoiso  6305  brecop  6627  ixpsnf1o  6738  ac6sfi  6900  ismkvnex  7155  nninfwlporlemd  7172  prarloclemn  7500  axcaucvglemres  7900  reapti  8538  indstr  9595  iccneg  9991  sqap0  10589  sqrt00  11051  minclpr  11247  fprodseq  11593  absefib  11780  efieq1re  11781  prmind2  12122  eqgval  13087  sincosq3sgn  14334  sincosq4sgn  14335  lgsdinn0  14534  pw1nct  14837  iswomninnlem  14882