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  4260  opelresi  4685  iota1  4951  funbrfv2b  5297  dffn5im  5298  fneqeql  5355  f1ompt  5398  dff13  5490  fliftcnv  5517  isotr  5538  isoini  5539  caovord3  5756  releldm2  5893  tpostpos  5964  nnaordi  6200  iserd  6251  ecdmn0m  6267  qliftel  6305  qliftfun  6307  qliftf  6310  ecopovsym  6321  mapen  6495  supisolem  6624  cnvti  6635  isomnimap  6714  recmulnqg  6871  nqtri3or  6876  ltmnqg  6881  mullocprlem  7050  addextpr  7101  gt0srpr  7215  ltsosr  7231  ltasrg  7237  xrlenlt  7472  letri3  7487  subadd  7606  ltsubadd2  7832  lesubadd2  7834  suble  7839  ltsub23  7841  ltaddpos2  7852  ltsubpos  7853  subge02  7877  ltaddsublt  7966  reapneg  7992  apsym  8001  apti  8017  leltap  8019  ap0gt0  8033  divmulap  8058  divmulap3  8060  rec11rap  8094  ltdiv1  8241  ltdivmul2  8251  ledivmul2  8253  ltrec  8256  suprleubex  8327  nnle1eq1  8358  avgle1  8566  avgle2  8567  nn0le0eq0  8611  znnnlt1  8708  zleltp1  8715  elz2  8728  uzm1  8958  uzin  8960  difrp  9079  xrletri3  9179  xltnegi  9206  elioo5  9260  elfz5  9341  fzdifsuc  9402  elfzm11  9412  uzsplit  9413  elfzonelfzo  9544  qtri3or  9557  qavgle  9573  flqbi  9600  flqbi2  9601  zmodid2  9662  q2submod  9695  sqap0  9872  lt2sq  9879  le2sq  9880  nn0opthlem1d  9977  ibcval5  10020  shftfib  10099  mulreap  10139  caucvgrelemcau  10254  caucvgre  10255  elicc4abs  10368  abs2difabs  10382  cau4  10390  maxclpr  10496  negfi  10498  lemininf  10503  clim2  10510  climeq  10526  dvdsval3  10594  dvdslelemd  10638  dvdsabseq  10642  dvdsflip  10646  dvdsssfz1  10647  zeo3  10662  ndvdsadd  10725  dvdssq  10814  algcvgblem  10825  lcmdvds  10855  ncoprmgcdgt1b  10866  isprm3  10894  phiprmpw  10992