Theorem bitr4d 189

Description: Deduction form of bitr4i 185. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem bitr4d

Step	Hyp	Ref	Expression
1		bitr4d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr4d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	2	bicomd 139	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 186	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3bitr2d  214  3bitr2rd  215  3bitr4d  218  3bitr4rd  219  bianabs  576  imordc  832  3anibar  1109  xor2dc  1324  bilukdc  1330  reuhypd  4266  opelresi  4691  iota1  4957  funbrfv2b  5306  dffn5im  5307  fneqeql  5364  f1ompt  5407  dff13  5502  fliftcnv  5529  isotr  5550  isoini  5552  caovord3  5769  releldm2  5906  tpostpos  5977  nnaordi  6213  iserd  6264  ecdmn0m  6280  qliftel  6318  qliftfun  6320  qliftf  6323  ecopovsym  6334  mapen  6508  supisolem  6640  cnvti  6651  isomnimap  6730  recmulnqg  6887  nqtri3or  6892  ltmnqg  6897  mullocprlem  7066  addextpr  7117  gt0srpr  7231  ltsosr  7247  ltasrg  7253  xrlenlt  7488  letri3  7503  subadd  7622  ltsubadd2  7848  lesubadd2  7850  suble  7855  ltsub23  7857  ltaddpos2  7868  ltsubpos  7869  subge02  7893  ltaddsublt  7982  reapneg  8008  apsym  8017  apti  8033  leltap  8035  ap0gt0  8049  divmulap  8074  divmulap3  8076  rec11rap  8110  ltdiv1  8257  ltdivmul2  8267  ledivmul2  8269  ltrec  8272  suprleubex  8343  nnle1eq1  8374  avgle1  8582  avgle2  8583  nn0le0eq0  8627  znnnlt1  8724  zleltp1  8731  elz2  8744  uzm1  8974  uzin  8976  difrp  9095  xrletri3  9195  xltnegi  9222  elioo5  9276  elfz5  9357  fzdifsuc  9418  elfzm11  9428  uzsplit  9429  elfzonelfzo  9562  qtri3or  9575  qavgle  9591  flqbi  9618  flqbi2  9619  zmodid2  9680  q2submod  9713  sqap0  9912  lt2sq  9919  le2sq  9920  nn0opthlem1d  10017  ibcval5  10060  zfz1isolemiso  10133  shftfib  10146  mulreap  10186  caucvgrelemcau  10301  caucvgre  10302  elicc4abs  10415  abs2difabs  10429  cau4  10437  maxclpr  10543  negfi  10545  lemininf  10550  clim2  10557  climeq  10573  dvdsval3  10667  dvdslelemd  10711  dvdsabseq  10715  dvdsflip  10719  dvdsssfz1  10720  zeo3  10735  ndvdsadd  10798  dvdssq  10887  algcvgblem  10898  lcmdvds  10928  ncoprmgcdgt1b  10939  isprm3  10967  phiprmpw  11065