Theorem bitr2d 283

Description: Deduction form of bitr2i 279. (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 282	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 226	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitrrd  309  3bitr2rd  311  pm5.18  384  ifptru  1091  sbequ12a  2289  elrnmpt1  5941  fndmdif  7041  weniso  7364  sbcopeq1a  8060  mpof1o2d  8137  xpord2pred  8162  snmapen  9066  dmttrcl  9722  cfss  10343  posdif  11809  lesub1  11810  lesub0  11833  possumd  11941  ltdivmul  12192  ledivmul  12193  zlem1lt  12748  zltlem1  12749  negelrp  13155  ioon0  13502  fzn  13673  fzrev2  13722  fz1sbc  13734  elfzp1b  13735  sumsqeq0  14322  fz1isolem  14606  sqrtle  15427  absgt0  15492  isershft  15831  incexc2  16007  dvdssubr  16475  gcdn0gt0  16690  divgcdcoprmex  16841  pcfac  17077  ramval  17186  isrnghm  20671  isorng  21118  iunocv  21987  ltbwe  22353  lmbrf  23578  perfcls  23683  ovolscalem1  25834  itg2mulclem  26067  sineq0  26852  efif1olem4  26873  logge0b  26959  loggt0b  26960  logle1b  26961  loglt1b  26962  atanord  27255  rlimcnp2  27294  bposlem7  27617  lgsprme0  27666  rpvmasum2  27839  ltsubsubs2bd  28470  posdifsd  28484  ltmuldivswd  28587  onsbnd2  28668  pw2gt0divsd  28831  pw2ge0divsd  28832  pw2ltsdiv1d  28838  z12bdaylem1  28856  elreno2  28881  trgcgrg  28978  legov3  29061  opphllem6  29228  plngcplem  29263  ebtwntg  29560  wwlksm1edg  30470  clwlkclwwlk2  30594  hial2eq2  31709  adjsym  32435  cnvadj  32494  eigvalcl  32563  mddmd  32903  mdslmd2i  32932  elat2  32942  indpreima  33474  xdivpnfrp  33541  ply1dg1rt  34154  esplyfval1  34247  unitdivcld  34575  infinfnum  35799  ioosconn  36054  nmulle  37008  poimirlem26  38607  areacirclem1  38669  isat3  40407  ishlat3N  40454  cvrval5  40515  llnexchb2  40969  lhpoc2N  41115  lhprelat3N  41140  lautcnvle  41189  lautcvr  41192  ltrncnvatb  41238  cdlemb3  41706  cdlemg17h  41768  dih0vbN  42382  djhcvat42  42515  dvh4dimat  42538  mapdordlem2  42737  aks6d1c5lem1  43229  eluzp1  43407  reltsub1  43480  reltsubadd2  43481  sn-ltmul2d  43580  fsuppind  43661  diophun  43827  jm2.19lem4  44042  ordeldifsucon  44304  orddif0suc  44313  uneqsn  45068  xrralrecnnge  46444  limsupre2lem  46777  tmachlem-agreeprod  47990  modmkpkne  48480  prprelb  48641  flsqrt5  48722  lincfsuppcl  49568