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  2293  elrnmpt1  5949  fndmdif  7064  weniso  7387  sbcopeq1a  8085  mpof1o2d  8164  xpord2pred  8189  snmapen  9094  dmttrcl  9749  cfss  10370  posdif  11836  lesub1  11837  lesub0  11860  possumd  11968  ltdivmul  12219  ledivmul  12220  zlem1lt  12775  zltlem1  12776  negelrp  13182  ioon0  13529  fzn  13700  fzrev2  13749  fz1sbc  13761  elfzp1b  13762  sumsqeq0  14349  fz1isolem  14633  sqrtle  15456  absgt0  15521  isershft  15860  incexc2  16036  dvdssubr  16504  gcdn0gt0  16719  divgcdcoprmex  16870  pcfac  17106  ramval  17215  isrnghm  20701  isorng  21148  iunocv  22017  ltbwe  22383  lmbrf  23608  perfcls  23713  ovolscalem1  25864  itg2mulclem  26097  sineq0  26882  efif1olem4  26903  logge0b  26989  loggt0b  26990  logle1b  26991  loglt1b  26992  atanord  27285  rlimcnp2  27324  bposlem7  27647  lgsprme0  27696  rpvmasum2  27869  ltsubsubs2bd  28500  posdifsd  28514  ltmuldivswd  28617  onsbnd2  28698  pw2gt0divsd  28861  pw2ge0divsd  28862  pw2ltsdiv1d  28868  z12bdaylem1  28886  elreno2  28911  trgcgrg  29008  legov3  29091  opphllem6  29258  plngcplem  29293  ebtwntg  29590  wwlksm1edg  30500  clwlkclwwlk2  30624  hial2eq2  31739  adjsym  32465  cnvadj  32524  eigvalcl  32593  mddmd  32933  mdslmd2i  32962  elat2  32972  indpreima  33502  xdivpnfrp  33569  ply1dg1rt  34182  esplyfval1  34275  unitdivcld  34603  infinfnum  35849  ioosconn  36179  nmulle  37144  poimirlem26  38756  areacirclem1  38818  isat3  40556  ishlat3N  40603  cvrval5  40664  llnexchb2  41118  lhpoc2N  41264  lhprelat3N  41289  lautcnvle  41338  lautcvr  41341  ltrncnvatb  41387  cdlemb3  41855  cdlemg17h  41917  dih0vbN  42531  djhcvat42  42664  dvh4dimat  42687  mapdordlem2  42886  aks6d1c5lem1  43378  eluzp1  43557  reltsub1  43630  reltsubadd2  43631  sn-ltmul2d  43730  fsuppind  43811  diophun  43977  jm2.19lem4  44192  ordeldifsucon  44453  orddif0suc  44462  uneqsn  45217  xrralrecnnge  46606  limsupre2lem  46939  tmachlem-agreeprod  48152  modmkpkne  48642  prprelb  48803  flsqrt5  48884  lincfsuppcl  49730  prelrrx2b  50032