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  2356  necon1bbiidc  2464  rspc2gv  2923  elabgt  2948  sbceq1a  3042  sbcralt  3109  sbcrext  3110  sbccsbg  3157  sbccsb2g  3158  iunpw  4583  tfis  4687  reldmm  4956  xp11m  5182  ressn  5284  fnssresb  5451  fun11iun  5613  funimass4  5705  dffo4  5803  f1ompt  5806  fliftf  5950  resoprab2  6128  ralrnmpo  6146  rexrnmpo  6147  1stconst  6395  2ndconst  6396  dfsmo2  6496  smoiso  6511  brecop  6837  ixpsnf1o  6948  ac6sfi  7130  ismkvnex  7397  nninfwlporlemd  7414  prarloclemn  7762  axcaucvglemres  8162  reapti  8802  indstr  9870  iccneg  10267  sqap0  10912  wrdmap  11192  wrdind  11350  sqrt00  11661  minclpr  11858  fprodseq  12205  absefib  12393  efieq1re  12394  prmind2  12753  gsumval2  13541  eqgval  13871  isnzr2  14260  sincosq3sgn  15619  sincosq4sgn  15620  fsumdvdsmul  15785  lgsdinn0  15847  pw1nct  16705  iswomninnlem  16762