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  575  imordc  829  3anibar  1106  xor2dc  1321  bilukdc  1327  reuhypd  4221  opelresi  4641  iota1  4901  funbrfv2b  5239  dffn5im  5240  fneqeql  5296  f1ompt  5341  dff13  5428  fliftcnv  5455  isotr  5476  isoini  5477  caovord3  5694  releldm2  5831  tpostpos  5902  nnaordi  6104  iserd  6155  ecdmn0m  6171  qliftel  6209  qliftfun  6211  qliftf  6214  ecopovsym  6225  supisolem  6421  cnvti  6432  recmulnqg  6581  nqtri3or  6586  ltmnqg  6591  mullocprlem  6760  addextpr  6811  gt0srpr  6925  ltsosr  6941  ltasrg  6947  xrlenlt  7177  letri3  7192  subadd  7311  ltsubadd2  7537  lesubadd2  7539  suble  7544  ltsub23  7546  ltaddpos2  7557  ltsubpos  7558  subge02  7582  ltaddsublt  7671  reapneg  7697  apsym  7706  apti  7722  leltap  7724  ap0gt0  7738  divmulap  7763  divmulap3  7765  rec11rap  7799  ltdiv1  7946  ltdivmul2  7956  ledivmul2  7958  ltrec  7961  suprleubex  8032  nnle1eq1  8063  avgle1  8271  avgle2  8272  nn0le0eq0  8316  znnnlt1  8399  zleltp1  8406  elz2  8419  uzm1  8649  uzin  8651  difrp  8770  xrletri3  8875  xltnegi  8902  elioo5  8956  elfz5  9037  fzdifsuc  9098  elfzm11  9108  uzsplit  9109  elfzonelfzo  9239  qtri3or  9252  qavgle  9267  flqbi  9292  flqbi2  9293  zmodid2  9354  q2submod  9387  sqap0  9542  lt2sq  9549  le2sq  9550  nn0opthlem1d  9647  ibcval5  9690  shftfib  9711  mulreap  9751  caucvgrelemcau  9866  caucvgre  9867  elicc4abs  9980  abs2difabs  9994  cau4  10002  maxclpr  10108  negfi  10110  lemininf  10115  clim2  10122  climeq  10138  dvdsval3  10199  dvdslelemd  10243  dvdsabseq  10247  dvdsflip  10251  dvdsssfz1  10252  zeo3  10267  ndvdsadd  10331  dvdssq  10420  algcvgblem  10431  lcmdvds  10461  ncoprmgcdgt1b  10472  isprm3  10500