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  3396  r19.28m  3540  r19.45mv  3544  r19.44mv  3545  r19.27m  3546  ralsnsg  3659  ralsns  3660  iunconstm  3924  iinconstm  3925  exmidsssnc  4236  unisucg  4449  relsng  4766  funssres  5300  fncnv  5324  dff1o5  5513  funimass4  5611  fneqeql2  5671  fnniniseg2  5685  rexsupp  5686  unpreima  5687  dffo3  5709  funfvima  5794  dff13  5815  f1eqcocnv  5838  fliftf  5846  isocnv2  5859  eloprabga  6009  mpo2eqb  6032  opabex3d  6178  opabex3  6179  elxp6  6227  elxp7  6228  sbthlemi5  7027  sbthlemi6  7028  nninfwlporlemd  7238  genpdflem  7574  ltnqpr  7660  ltexprlemloc  7674  xrlenlt  8091  negcon2  8279  dfinfre  8983  sup3exmid  8984  elznn  9342  zq  9700  rpnegap  9761  infssuzex  10323  modqmuladdnn0  10460  shftdm  10987  rexfiuz  11154  rexanuz2  11156  sumsplitdc  11597  fsum2dlemstep  11599  odd2np1  12038  divalgb  12090  nninfctlemfo  12207  isprm4  12287  ctiunctlemudc  12654  grp1  13238  nmznsg  13343  qusecsub  13461  iscrng2  13571  opprsubgg  13640  opprsubrngg  13767  domnmuln0  13829  tx1cn  14505  tx2cn  14506  cnbl0  14770  cnblcld  14771  reopnap  14782  pilem1  15015  sinq34lt0t  15067  gausslemma2dlem1a  15299