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  4296  prelpw  4299  reuhypd  4562  opelresi  5016  iota1  5293  funbrfv2b  5680  dffn5im  5681  fneqeql  5745  f1ompt  5788  dff13  5898  fliftcnv  5925  isotr  5946  isoini  5948  caovord3  6185  releldm2  6337  tpostpos  6416  nnsssuc  6656  nnaordi  6662  iserd  6714  ecdmn0m  6732  qliftel  6770  qliftfun  6772  qliftf  6775  ecopovsym  6786  pw2f1odclem  7003  mapen  7015  supisolem  7183  cnvti  7194  omp1eomlem  7269  ctssdc  7288  isomnimap  7312  ismkvmap  7329  iswomnimap  7341  netap  7448  2omotaplemap  7451  recmulnqg  7586  nqtri3or  7591  ltmnqg  7596  mullocprlem  7765  addextpr  7816  gt0srpr  7943  ltsosr  7959  ltasrg  7965  map2psrprg  8000  xrlenlt  8219  letri3  8235  subadd  8357  ltsubadd2  8588  lesubadd2  8590  suble  8595  ltsub23  8597  ltaddpos2  8608  ltsubpos  8609  subge02  8633  ltaddsublt  8726  reapneg  8752  apsym  8761  apti  8777  leltap  8780  ap0gt0  8795  divmulap  8830  divmulap3  8832  rec11rap  8866  ltdiv1  9023  ltdivmul2  9033  ledivmul2  9035  ltrec  9038  suprleubex  9109  nnle1eq1  9142  avgle1  9360  avgle2  9361  nn0le0eq0  9405  znnnlt1  9502  zleltp1  9510  elz2  9526  uzm1  9761  uzin  9763  difrp  9896  xrletri3  10008  xgepnf  10020  xltnegi  10039  xltadd1  10080  xposdif  10086  xleaddadd  10091  elioo5  10137  elfz5  10221  fzdifsuc  10285  elfzm11  10295  uzsplit  10296  elfzonelfzo  10444  qtri3or  10468  qavgle  10486  flqbi  10518  flqbi2  10519  fldiv4lem1div2uz2  10534  zmodid2  10582  q2submod  10615  sqap0  10836  lt2sq  10843  le2sq  10844  nn0opthlem1d  10950  bcval5  10993  zfz1isolemiso  11069  pfxsuffeqwrdeq  11238  shftfib  11342  mulreap  11383  caucvgrelemcau  11499  caucvgre  11500  elicc4abs  11613  abs2difabs  11627  cau4  11635  maxclpr  11741  negfi  11747  lemininf  11753  mul0inf  11760  xrlemininf  11790  xrminltinf  11791  clim2  11802  climeq  11818  fisumss  11911  fsumabs  11984  isumshft  12009  absefib  12290  dvdsval3  12310  dvdslelemd  12362  dvdsabseq  12366  dvdsflip  12370  dvdsssfz1  12371  zeo3  12387  ndvdsadd  12450  bitscmp  12477  dvdssq  12560  algcvgblem  12579  lcmdvds  12609  ncoprmgcdgt1b  12620  isprm3  12648  phiprmpw  12752  prmdiv  12765  pc11  12862  pcz  12863  pockthlem  12887  1arith  12898  ercpbllemg  13371  grpinvcnv  13609  eqger  13769  ablsubadd  13857  dvdsr02  14077  opprunitd  14082  unitsubm  14091  issubrg3  14219  aprval  14254  rnglidlmmgm  14468  znleval2  14626  discld  14818  isneip  14828  restopnb  14863  restopn2  14865  restdis  14866  lmbr2  14896  cnptoprest  14921  cnptoprest2  14922  tx1cn  14951  tx2cn  14952  txcnmpt  14955  txrest  14958  elbl2ps  15074  elbl2  15075  blcomps  15078  blcom  15079  xblpnfps  15080  xblpnf  15081  blpnf  15082  xmeter  15118  bdxmet  15183  metrest  15188  xmetxp  15189  metcn  15196  cncfcdm  15264  reefiso  15459  gausslemma2dlem0c  15738  lgseisenlem3  15759  lgsquadlem1  15764  m1lgs  15772  2lgsoddprmlem2  15793  ausgrusgrben  15974