Theorem bitr4id 199

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

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

Assertion

Ref	Expression
bitr4id	|- ( ph -> ( ps <-> th ) )

Proof of Theorem bitr4id

Step	Hyp	Ref	Expression
1		bitr4id.1	. 2 |- ( ph -> ( th <-> ch ) )
2		bitr4id.2	. . 3 |- ( ps <-> ch )
3	2	bicomi 132	. 2 |- ( ch <-> ps )
4	1, 3	bitr2di 197	1 |- ( ph -> ( ps <-> 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:  imimorbdc  897  baib  920  pm5.6dc  927  xornbidc  1402  mo2dc  2100  reu8  2960  sbc6g  3014  dfss4st  3397  r19.28m  3541  r19.45mv  3545  r19.44mv  3546  r19.27m  3547  ralsnsg  3660  ralsns  3661  iunconstm  3925  iinconstm  3926  exmidsssnc  4237  unisucg  4450  relsng  4767  funssres  5301  fncnv  5325  dff1o5  5516  funimass4  5614  fneqeql2  5674  fnniniseg2  5688  rexsupp  5689  unpreima  5690  dffo3  5712  funfvima  5797  dff13  5818  f1eqcocnv  5841  fliftf  5849  isocnv2  5862  eloprabga  6013  mpo2eqb  6036  opabex3d  6187  opabex3  6188  elxp6  6236  elxp7  6237  sbthlemi5  7036  sbthlemi6  7037  nninfwlporlemd  7247  genpdflem  7593  ltnqpr  7679  ltexprlemloc  7693  xrlenlt  8110  negcon2  8298  dfinfre  9002  sup3exmid  9003  elznn  9361  zq  9719  rpnegap  9780  infssuzex  10342  modqmuladdnn0  10479  shftdm  11006  rexfiuz  11173  rexanuz2  11175  sumsplitdc  11616  fsum2dlemstep  11618  odd2np1  12057  divalgb  12109  nninfctlemfo  12234  isprm4  12314  ctiunctlemudc  12681  grp1  13310  nmznsg  13421  qusecsub  13539  iscrng2  13649  opprsubgg  13718  opprsubrngg  13845  domnmuln0  13907  tx1cn  14591  tx2cn  14592  cnbl0  14856  cnblcld  14857  reopnap  14868  pilem1  15101  sinq34lt0t  15153  gausslemma2dlem1a  15385