Theorem bitr4d 180

Description: Deduction form of bitr4i 176. (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 129	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 177	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3bitr2d  205  3bitr2rd  206  3bitr4d  209  3bitr4rd  210  bianabs  543  imordc  796  3anibar  1072  xor2dc  1281  bilukdc  1287  reuhypd  4203  opelresi  4623  iota1  4881  funbrfv2b  5218  dffn5im  5219  fneqeql  5275  f1ompt  5320  dff13  5407  fliftcnv  5435  isotr  5456  isoini  5457  caovord3  5674  releldm2  5811  tpostpos  5879  nnaordi  6081  iserd  6132  ecdmn0m  6148  qliftel  6186  qliftfun  6188  qliftf  6191  ecopovsym  6202  recmulnqg  6489  nqtri3or  6494  ltmnqg  6499  mullocprlem  6668  addextpr  6719  gt0srpr  6833  ltsosr  6849  ltasrg  6855  xrlenlt  7084  letri3  7099  subadd  7214  ltsubadd2  7428  lesubadd2  7430  suble  7435  ltsub23  7437  ltaddpos2  7448  ltsubpos  7449  subge02  7473  ltaddsublt  7562  reapneg  7588  apsym  7597  apti  7613  leltap  7615  ap0gt0  7629  divmulap  7654  divmulap3  7656  rec11rap  7687  ltdiv1  7834  ltdivmul2  7844  ledivmul2  7846  ltrec  7849  nnle1eq1  7938  avgle1  8165  avgle2  8166  nn0le0eq0  8210  znnnlt1  8293  zleltp1  8299  elz2  8312  uzm1  8503  uzin  8505  difrp  8619  xrletri3  8721  xltnegi  8748  elioo5  8802  elfz5  8882  fzdifsuc  8943  elfzm11  8953  uzsplit  8954  elfzonelfzo  9086  qtri3or  9098  flqbi  9132  flqbi2  9133  sqap0  9320  lt2sq  9327  le2sq  9328  shftfib  9424  mulreap  9464  caucvgrelemcau  9579  caucvgre  9580  elicc4abs  9690  abs2difabs  9704  cau4  9712  clim2  9804  climeq  9820  algcvgblem  9888