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  4297  prelpw  4300  reuhypd  4563  opelresi  5019  iota1  5296  funbrfv2b  5683  dffn5im  5684  fneqeql  5748  f1ompt  5791  dff13  5901  fliftcnv  5928  isotr  5949  isoini  5951  caovord3  6188  releldm2  6340  tpostpos  6421  nnsssuc  6661  nnaordi  6667  iserd  6719  ecdmn0m  6737  qliftel  6775  qliftfun  6777  qliftf  6780  ecopovsym  6791  pw2f1odclem  7008  mapen  7020  supisolem  7191  cnvti  7202  omp1eomlem  7277  ctssdc  7296  isomnimap  7320  ismkvmap  7337  iswomnimap  7349  netap  7456  2omotaplemap  7459  recmulnqg  7594  nqtri3or  7599  ltmnqg  7604  mullocprlem  7773  addextpr  7824  gt0srpr  7951  ltsosr  7967  ltasrg  7973  map2psrprg  8008  xrlenlt  8227  letri3  8243  subadd  8365  ltsubadd2  8596  lesubadd2  8598  suble  8603  ltsub23  8605  ltaddpos2  8616  ltsubpos  8617  subge02  8641  ltaddsublt  8734  reapneg  8760  apsym  8769  apti  8785  leltap  8788  ap0gt0  8803  divmulap  8838  divmulap3  8840  rec11rap  8874  ltdiv1  9031  ltdivmul2  9041  ledivmul2  9043  ltrec  9046  suprleubex  9117  nnle1eq1  9150  avgle1  9368  avgle2  9369  nn0le0eq0  9413  znnnlt1  9510  zleltp1  9518  elz2  9534  uzm1  9770  uzin  9772  difrp  9905  xrletri3  10017  xgepnf  10029  xltnegi  10048  xltadd1  10089  xposdif  10095  xleaddadd  10100  elioo5  10146  elfz5  10230  fzdifsuc  10294  elfzm11  10304  uzsplit  10305  elfzonelfzo  10453  qtri3or  10477  qavgle  10495  flqbi  10527  flqbi2  10528  fldiv4lem1div2uz2  10543  zmodid2  10591  q2submod  10624  sqap0  10845  lt2sq  10852  le2sq  10853  nn0opthlem1d  10959  bcval5  11002  zfz1isolemiso  11079  pfxsuffeqwrdeq  11251  shftfib  11355  mulreap  11396  caucvgrelemcau  11512  caucvgre  11513  elicc4abs  11626  abs2difabs  11640  cau4  11648  maxclpr  11754  negfi  11760  lemininf  11766  mul0inf  11773  xrlemininf  11803  xrminltinf  11804  clim2  11815  climeq  11831  fisumss  11924  fsumabs  11997  isumshft  12022  absefib  12303  dvdsval3  12323  dvdslelemd  12375  dvdsabseq  12379  dvdsflip  12383  dvdsssfz1  12384  zeo3  12400  ndvdsadd  12463  bitscmp  12490  dvdssq  12573  algcvgblem  12592  lcmdvds  12622  ncoprmgcdgt1b  12633  isprm3  12661  phiprmpw  12765  prmdiv  12778  pc11  12875  pcz  12876  pockthlem  12900  1arith  12911  ercpbllemg  13384  grpinvcnv  13622  eqger  13782  ablsubadd  13870  dvdsr02  14090  opprunitd  14095  unitsubm  14104  issubrg3  14232  aprval  14267  rnglidlmmgm  14481  znleval2  14639  discld  14831  isneip  14841  restopnb  14876  restopn2  14878  restdis  14879  lmbr2  14909  cnptoprest  14934  cnptoprest2  14935  tx1cn  14964  tx2cn  14965  txcnmpt  14968  txrest  14971  elbl2ps  15087  elbl2  15088  blcomps  15091  blcom  15092  xblpnfps  15093  xblpnf  15094  blpnf  15095  xmeter  15131  bdxmet  15196  metrest  15201  xmetxp  15202  metcn  15209  cncfcdm  15277  reefiso  15472  gausslemma2dlem0c  15751  lgseisenlem3  15772  lgsquadlem1  15777  m1lgs  15785  2lgsoddprmlem2  15806  ausgrusgrben  15987