Theorem bitr3i 242

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
bitr3i	|- (ph <-> ch)

Proof of Theorem bitr3i

Step	Hyp	Ref	Expression
1		bitr3i.1	. . 3 |- (ps <-> ph)
2	1	bicomi 193	. 2 |- (ph <-> ps)
3		bitr3i.2	. 2 |- (ps <-> ch)
4	2, 3	bitri 240	1 |- (ph <-> ch)

Syntax hints:   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  3bitrri  263  3bitr3i  266  3bitr3ri  267  xchnxbi  299  ianor  474  orordi  516  orordir  517  anandi  801  anandir  802  trunantru  1354  falnanfal  1357  cadan  1392  had0  1403  nic-axALT  1439  sbelx  2124  2mos  2283  2eu6  2289  abeq1i  2462  necon1bbii  2569  r19.41  2764  2ralor  2781  rexcom4a  2880  moeq  3013  euind  3024  2reuswap  3039  2reu5  3045  sbcid  3063  sbcco2  3070  sbc7  3074  sbcie2g  3080  eqsbc1  3086  sbcralt  3119  csbid  3144  cbvralcsf  3199  cbvrabcsf  3202  abss  3336  ssab  3337  difrab  3530  neq0  3561  vdif0  3611  ssunsn2  3866  sspr  3870  sstp  3871  prsspw  3879  disj5  3891  uniintsn  3964  dfpw12  4302  insklem  4305  nnsucelrlem3  4427  ltfinex  4465  dfevenfin2  4513  dfoddfin2  4514  proj1op  4601  proj2op  4602  unopab  4639  brab1  4685  opelssetsn  4761  eliunxp  4822  ralxp  4826  rexxp  4827  opelco  4885  cnvco  4895  dmun  4913  elimapw12  4946  iss  5001  imai  5011  imasn  5019  cotr  5027  cnvsym  5028  intasym  5029  intirr  5030  rninxp  5061  dffun2  5120  dffun3  5121  fin  5247  funimass4  5369  fnressn  5439  fvi  5443  resoprab  5582  ov6g  5601  fmpt2x  5731  braddcfn  5827  fnsex  5833  brpprod  5840  fnfullfunlem1  5857  fvfullfunlem2  5863  clos1induct  5881  transex  5911  connexex  5914  foundex  5915  qsexg  5983  enex  6032  xpassen  6058  enpw1pw  6076  enprmaplem1  6077  ovmuc  6131  ovcelem1  6172  ceex  6175  tcfnex  6245  nmembers1lem1  6269  frecxp  6315  fnfreclem2  6319  fnfreclem3  6320