Theorem bitr3id 194

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

Hypotheses

Ref	Expression
bitr3id.1	|- ( ps <-> ph )
bitr3id.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
bitr3id	|- ( ch -> ( ph <-> th ) )

Proof of Theorem bitr3id

Step	Hyp	Ref	Expression
1		bitr3id.1	. . 3 |- ( ps <-> ph )
2	1	bicomi 132	. 2 |- ( ph <-> ps )
3		bitr3id.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	bitrid 192	1 |- ( ch -> ( ph <-> th ) )

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  907  19.16  1604  19.19  1714  cbvab  2360  necon1bbiidc  2475  rspc2gv  2936  elabgt  2961  sbceq1a  3055  sbcralt  3122  sbcrext  3123  sbccsbg  3170  sbccsb2g  3171  iunpw  4606  tfis  4710  reldmm  4980  xp11m  5206  ressn  5308  fnssresb  5475  fun11iun  5640  funimass4  5732  dffo4  5830  f1ompt  5833  dfimafnf  5928  fliftf  5978  resoprab2  6158  ralrnmpo  6176  rexrnmpo  6177  1stconst  6430  2ndconst  6431  dfsmo2  6531  smoiso  6546  brecop  6872  ixpsnf1o  6984  ac6sfi  7168  ismkvnex  7459  nninfwlporlemd  7476  prarloclemn  7830  axcaucvglemres  8230  reapti  8871  indstr  9946  iccneg  10344  sqap0  10995  wrdmap  11284  wrdind  11442  sqrt00  11754  minclpr  11951  fprodseq  12298  absefib  12486  efieq1re  12487  prmind2  12846  ballotfilemsima  13207  gsumval2  13664  eqgval  13980  isnzr2  14433  sincosq3sgn  15823  sincosq4sgn  15824  fsumdvdsmul  15989  lgsdinn0  16051  pw1nct  16917  iswomninnlem  16974