Theorem 3bitr4rd 286

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

Hypotheses

Ref	Expression
3bitr4d.1
3bitr4d.2
3bitr4d.3

Assertion

Ref	Expression
3bitr4rd

Proof of Theorem 3bitr4rd

Step	Hyp	Ref	Expression
1		3bitr4d.3	. . 3
2		3bitr4d.1	. . 3
3	1, 2	bitr4d 256	. 2
4		3bitr4d.2	. 2
5	3, 4	bitr4d 256	1

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

This theorem is referenced by:  inimasn  5428  oacan  7216  ecdmn0  7373  wemapwe  8160  wemapweOLD  8161  r1pw  8284  adderpqlem  9353  mulerpqlem  9354  lterpq  9369  ltanq  9370  genpass  9408  readdcan  9775  lemuldiv  10449  msq11  10471  avglt2  10802  qbtwnre  11427  iooshf  11632  clim2c  13328  lo1o1  13355  climabs0  13408  reef11  13854  absefib  13933  efieq1re  13934  pc2dvds  14402  pcmpt  14411  subsubc  15222  odmulgid  16576  gexdvds  16604  submcmn2  16847  obslbs  18761  cnntr  19776  cndis  19792  cnindis  19793  cnpdis  19794  lmres  19801  cmpfi  19908  ist0-4  20230  txhmeo  20304  tsmssubm  20644  blin  20924  cncfmet  21412  icopnfcnv  21442  lmmbrf  21701  iscauf  21719  causs  21737  mbfposr  22059  itg2gt0  22167  limcflf  22285  limcres  22290  lhop1  22415  dvdsr1p  22562  fsumvma2  23489  vmasum  23491  chpchtsum  23494  bposlem1  23559  iscgrgd  23905  lnrot1  24003  eqeelen  24207  nbgraeledg  24430  nb3graprlem2  24452  cusgra3v  24464  cusgrauvtxb  24496  clwlkisclwwlk2  24790  el2spthonot0  24871  rusgranumwlks  24956  dmdmd  27219  funcnvmptOLD  27509  funcnvmpt  27510  xrdifh  27591  ismntop  28004  eulerpartlemgh  28317  signslema  28519  leceifl  30044  iblabsnclem  30078  ftc1anclem6  30095  areacirclem5  30111  areacirc  30112  ellz1  30700  islssfg  31016  proot1ex  31161  eliooshift  31541  clim2cf  31656  lsatfixedN  34734  cdlemg10c  36365  diaglbN  36782  dih1  37013  dihglbcpreN  37027  mapdcv  37387

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 185