Theorem bitr2d 280

Description: Deduction form of bitr2i 276. (Contributed by NM, 9-Jun-2004.)

Hypotheses

Ref	Expression
bitr2d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr2d.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
bitr2d	⊢ (𝜑 → (𝜃 ↔ 𝜓))

Proof of Theorem bitr2d

Step	Hyp	Ref	Expression
1		bitr2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr2d.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
3	1, 2	bitrd 279	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 223	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3bitrrd  306  3bitr2rd  308  pm5.18  381  ifptru  1074  sbequ12a  2259  elrnmpt1  5907  fndmdif  6984  weniso  7297  sbcopeq1a  7990  xpord2pred  8084  snmapen  8970  dmttrcl  9621  cfss  10166  posdif  11620  lesub1  11621  lesub0  11644  possumd  11752  ltdivmul  12007  ledivmul  12008  zlem1lt  12534  zltlem1  12535  negelrp  12935  ioon0  13281  fzn  13450  fzrev2  13498  fz1sbc  13510  elfzp1b  13511  sumsqeq0  14096  fz1isolem  14378  sqrtle  15177  absgt0  15242  isershft  15581  incexc2  15755  dvdssubr  16226  gcdn0gt0  16439  divgcdcoprmex  16587  pcfac  16821  ramval  16930  isrnghm  20369  isorng  20786  iunocv  21628  ltbwe  21989  lmbrf  23185  perfcls  23290  ovolscalem1  25451  itg2mulclem  25684  sineq0  26470  efif1olem4  26491  logge0b  26577  loggt0b  26578  logle1b  26579  loglt1b  26580  atanord  26874  rlimcnp2  26913  bposlem7  27238  lgsprme0  27287  rpvmasum2  27460  sltsubsub2bd  28034  posdifsd  28047  sltmuldivwd  28150  pw2gt0divsd  28378  pw2ge0divsd  28379  pw2sltdiv1d  28385  trgcgrg  28503  legov3  28586  opphllem6  28740  ebtwntg  28971  wwlksm1edg  29870  clwlkclwwlk2  29994  hial2eq2  31098  adjsym  31824  cnvadj  31883  eigvalcl  31952  mddmd  32292  mdslmd2i  32321  elat2  32331  indpreima  32857  xdivpnfrp  32924  ply1dg1rt  33554  unitdivcld  33925  ioosconn  35302  poimirlem26  37696  areacirclem1  37758  isat3  39416  ishlat3N  39463  cvrval5  39524  llnexchb2  39978  lhpoc2N  40124  lhprelat3N  40149  lautcnvle  40198  lautcvr  40201  ltrncnvatb  40247  cdlemb3  40715  cdlemg17h  40777  dih0vbN  41391  djhcvat42  41524  dvh4dimat  41547  mapdordlem2  41746  aks6d1c5lem1  42239  f1o2d2  42341  eluzp1  42415  reltsub1  42494  reltsubadd2  42495  sn-ltmul2d  42581  fsuppind  42698  diophun  42880  jm2.19lem4  43099  ordeldifsucon  43366  orddif0suc  43375  uneqsn  44132  xrralrecnnge  45502  limsupre2lem  45836  modmkpkne  47475  prprelb  47630  flsqrt5  47708  lincfsuppcl  48528