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  613  imordc  902  ifpnst  994  3anibar  1189  xor2dc  1432  bilukdc  1438  snelpwg  4300  prelpw  4303  reuhypd  4566  opelresi  5022  iota1  5299  funbrfv2b  5686  dffn5im  5687  fneqeql  5751  f1ompt  5794  dff13  5904  fliftcnv  5931  isotr  5952  isoini  5954  caovord3  6191  releldm2  6343  tpostpos  6425  nnsssuc  6665  nnaordi  6671  iserd  6723  ecdmn0m  6741  qliftel  6779  qliftfun  6781  qliftf  6784  ecopovsym  6795  pw2f1odclem  7015  mapen  7027  supisolem  7201  cnvti  7212  omp1eomlem  7287  ctssdc  7306  isomnimap  7330  ismkvmap  7347  iswomnimap  7359  netap  7466  2omotaplemap  7469  recmulnqg  7604  nqtri3or  7609  ltmnqg  7614  mullocprlem  7783  addextpr  7834  gt0srpr  7961  ltsosr  7977  ltasrg  7983  map2psrprg  8018  xrlenlt  8237  letri3  8253  subadd  8375  ltsubadd2  8606  lesubadd2  8608  suble  8613  ltsub23  8615  ltaddpos2  8626  ltsubpos  8627  subge02  8651  ltaddsublt  8744  reapneg  8770  apsym  8779  apti  8795  leltap  8798  ap0gt0  8813  divmulap  8848  divmulap3  8850  rec11rap  8884  ltdiv1  9041  ltdivmul2  9051  ledivmul2  9053  ltrec  9056  suprleubex  9127  nnle1eq1  9160  avgle1  9378  avgle2  9379  nn0le0eq0  9423  znnnlt1  9520  zleltp1  9528  elz2  9544  uzm1  9780  uzin  9782  difrp  9920  xrletri3  10032  xgepnf  10044  xltnegi  10063  xltadd1  10104  xposdif  10110  xleaddadd  10115  elioo5  10161  elfz5  10245  fzdifsuc  10309  elfzm11  10319  uzsplit  10320  elfzonelfzo  10468  qtri3or  10493  qavgle  10511  flqbi  10543  flqbi2  10544  fldiv4lem1div2uz2  10559  zmodid2  10607  q2submod  10640  sqap0  10861  lt2sq  10868  le2sq  10869  nn0opthlem1d  10975  bcval5  11018  zfz1isolemiso  11096  pfxsuffeqwrdeq  11272  shftfib  11377  mulreap  11418  caucvgrelemcau  11534  caucvgre  11535  elicc4abs  11648  abs2difabs  11662  cau4  11670  maxclpr  11776  negfi  11782  lemininf  11788  mul0inf  11795  xrlemininf  11825  xrminltinf  11826  clim2  11837  climeq  11853  fisumss  11946  fsumabs  12019  isumshft  12044  absefib  12325  dvdsval3  12345  dvdslelemd  12397  dvdsabseq  12401  dvdsflip  12405  dvdsssfz1  12406  zeo3  12422  ndvdsadd  12485  bitscmp  12512  dvdssq  12595  algcvgblem  12614  lcmdvds  12644  ncoprmgcdgt1b  12655  isprm3  12683  phiprmpw  12787  prmdiv  12800  pc11  12897  pcz  12898  pockthlem  12922  1arith  12933  ercpbllemg  13406  grpinvcnv  13644  eqger  13804  ablsubadd  13892  dvdsr02  14112  opprunitd  14117  unitsubm  14126  issubrg3  14254  aprval  14289  rnglidlmmgm  14503  znleval2  14661  discld  14853  isneip  14863  restopnb  14898  restopn2  14900  restdis  14901  lmbr2  14931  cnptoprest  14956  cnptoprest2  14957  tx1cn  14986  tx2cn  14987  txcnmpt  14990  txrest  14993  elbl2ps  15109  elbl2  15110  blcomps  15113  blcom  15114  xblpnfps  15115  xblpnf  15116  blpnf  15117  xmeter  15153  bdxmet  15218  metrest  15223  xmetxp  15224  metcn  15231  cncfcdm  15299  reefiso  15494  gausslemma2dlem0c  15773  lgseisenlem3  15794  lgsquadlem1  15799  m1lgs  15807  2lgsoddprmlem2  15828  ausgrusgrben  16012