Theorem 3bitr4rd 301

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr4d.1	|- ( ph -> ( ps <-> ch ) )
3bitr4d.2	|- ( ph -> ( th <-> ps ) )
3bitr4d.3	|- ( ph -> ( ta <-> ch ) )

Assertion

Ref	Expression
3bitr4rd	|- ( ph -> ( ta <-> th ) )

Proof of Theorem 3bitr4rd

Step	Hyp	Ref	Expression
1		3bitr4d.3	. . 3 |- ( ph -> ( ta <-> ch ) )
2		3bitr4d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3	1, 2	bitr4d 271	. 2 |- ( ph -> ( ta <-> ps ) )
4		3bitr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
5	3, 4	bitr4d 271	1 |- ( ph -> ( ta <-> th ) )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  inimasn  5550  isof1oidb  6574  oacan  7628  ecdmn0  7789  wemapwe  8594  r1pw  8708  adderpqlem  9776  mulerpqlem  9777  lterpq  9792  ltanq  9793  genpass  9831  readdcan  10210  lemuldiv  10903  msq11  10924  avglt2  11271  qbtwnre  12030  iooshf  12252  clim2c  14236  lo1o1  14263  climabs0  14316  reef11  14849  absefib  14928  efieq1re  14929  nndivides  14990  oddnn02np1  15072  oddge22np1  15073  evennn02n  15074  evennn2n  15075  halfleoddlt  15086  pc2dvds  15583  pcmpt  15596  subsubc  16513  odmulgid  17971  gexdvds  17999  submcmn2  18244  obslbs  20074  cnntr  21079  cndis  21095  cnindis  21096  cnpdis  21097  lmres  21104  cmpfi  21211  ist0-4  21532  txhmeo  21606  tsmssubm  21946  blin  22226  cncfmet  22711  icopnfcnv  22741  lmmbrf  23060  iscauf  23078  causs  23096  mbfposr  23419  itg2gt0  23527  limcflf  23645  limcres  23650  lhop1  23777  dvdsr1p  23921  fsumvma2  24939  vmasum  24941  chpchtsum  24944  bposlem1  25009  iscgrgd  25408  tgcgr4  25426  lnrot1  25518  eqeelen  25784  nbusgreledg  26249  nb3grprlem2  26283  wspthsnwspthsnon  26811  rusgrnumwwlks  26869  clwlkclwwlk2  26904  dmdmd  29159  funcnvmptOLD  29467  funcnvmpt  29468  1stpreimas  29483  xrdifh  29542  ismntop  30070  eulerpartlemgh  30440  signslema  30639  topdifinfindis  33194  leceifl  33398  lindsenlbs  33404  iblabsnclem  33473  ftc1anclem6  33490  areacirclem5  33504  areacirc  33505  lsatfixedN  34296  cdlemg10c  35927  diaglbN  36344  dih1  36575  dihglbcpreN  36589  mapdcv  36949  ellz1  37330  islssfg  37640  proot1ex  37779  eliooshift  39729  clim2cf  39882  sfprmdvdsmersenne  41520  odd2np1ALTV  41585