Theorem bitr4d 191

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitr2d  216  3bitr2rd  217  3bitr4d  220  3bitr4rd  221  mpbirand  441  mpbiran2d  442  bianabs  615  imordc  905  ifpnst  997  3anibar  1192  xor2dc  1435  bilukdc  1441  snelpwg  4325  prelpw  4328  reuhypd  4591  opelresi  5048  iota1  5326  funbrfv2b  5720  dffn5im  5721  fneqeql  5785  f1ompt  5827  dff13  5940  fliftcnv  5967  isotr  5988  isoini  5990  caovord3  6227  releldm2  6378  tpostpos  6494  nnsssuc  6734  nnaordi  6740  iserd  6792  ecdmn0m  6810  qliftel  6848  qliftfun  6850  qliftf  6853  ecopovsym  6864  pw2f1odclem  7086  mapen  7098  suppeqfsuppbi  7247  supisolem  7298  cnvti  7309  omp1eomlem  7384  ctssdc  7403  isomnimap  7427  ismkvmap  7444  iswomnimap  7456  netap  7567  2omotaplemap  7570  recmulnqg  7705  nqtri3or  7710  ltmnqg  7715  mullocprlem  7884  addextpr  7935  gt0srpr  8062  ltsosr  8078  ltasrg  8084  map2psrprg  8119  xrlenlt  8337  letri3  8353  subadd  8475  ltsubadd2  8706  lesubadd2  8708  suble  8713  ltsub23  8715  ltaddpos2  8726  ltsubpos  8727  subge02  8751  ltaddsublt  8844  reapneg  8870  apsym  8879  apti  8895  leltap  8898  ap0gt0  8913  divmulap  8948  divmulap3  8950  rec11rap  8984  ltdiv1  9141  ltdivmul2  9151  ledivmul2  9153  ltrec  9156  suprleubex  9227  nnle1eq1  9260  avgle1  9478  avgle2  9479  nn0le0eq0  9523  znnnlt1  9624  zleltp1  9632  elz2  9648  uzm1  9884  uzin  9886  difrp  10024  xrletri3  10136  xgepnf  10148  xltnegi  10167  xltadd1  10208  xposdif  10214  xleaddadd  10219  elioo5  10265  elfz5  10350  fzdifsuc  10414  elfzm11  10424  uzsplit  10425  elfzonelfzo  10574  qtri3or  10599  qavgle  10617  flqbi  10649  flqbi2  10650  fldiv4lem1div2uz2  10665  zmodid2  10713  q2submod  10746  sqap0  10967  lt2sq  10974  le2sq  10975  nn0opthlem1d  11081  bcval5  11124  zfz1isolemiso  11207  pfxsuffeqwrdeq  11386  shftfib  11504  mulreap  11545  caucvgrelemcau  11661  caucvgre  11662  elicc4abs  11775  abs2difabs  11789  cau4  11797  maxclpr  11903  negfi  11909  lemininf  11915  mul0inf  11922  xrlemininf  11952  xrminltinf  11953  clim2  11964  climeq  11980  fisumss  12074  fsumabs  12147  isumshft  12172  absefib  12453  dvdsval3  12473  dvdslelemd  12525  dvdsabseq  12529  dvdsflip  12533  dvdsssfz1  12534  zeo3  12550  ndvdsadd  12613  bitscmp  12640  dvdssq  12723  algcvgblem  12742  lcmdvds  12772  ncoprmgcdgt1b  12783  isprm3  12811  phiprmpw  12915  prmdiv  12928  pc11  13025  pcz  13026  pockthlem  13050  1arith  13061  ercpbllemg  13535  grpinvcnv  13773  eqger  13933  ablsubadd  14021  dvdsr02  14242  opprunitd  14247  unitsubm  14256  issubrg3  14384  aprval  14420  rnglidlmmgm  14636  znleval2  14794  discld  14993  isneip  15003  restopnb  15038  restopn2  15040  restdis  15041  lmbr2  15071  cnptoprest  15096  cnptoprest2  15097  tx1cn  15126  tx2cn  15127  txcnmpt  15130  txrest  15133  elbl2ps  15249  elbl2  15250  blcomps  15253  blcom  15254  xblpnfps  15255  xblpnf  15256  blpnf  15257  xmeter  15293  bdxmet  15358  metrest  15363  xmetxp  15364  metcn  15371  cncfcdm  15439  reefiso  15634  gausslemma2dlem0c  15916  lgseisenlem3  15937  lgsquadlem1  15942  m1lgs  15950  2lgsoddprmlem2  15971  ausgrusgrben  16155  eupth2lemsfi  16465