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  611  imordc  898  3anibar  1167  xor2dc  1401  bilukdc  1407  reuhypd  4489  opelresi  4936  iota1  5210  funbrfv2b  5581  dffn5im  5582  fneqeql  5645  f1ompt  5688  dff13  5790  fliftcnv  5817  isotr  5838  isoini  5840  caovord3  6070  releldm2  6210  tpostpos  6289  nnsssuc  6527  nnaordi  6533  iserd  6585  ecdmn0m  6603  qliftel  6641  qliftfun  6643  qliftf  6646  ecopovsym  6657  pw2f1odclem  6862  mapen  6874  supisolem  7037  cnvti  7048  omp1eomlem  7123  ctssdc  7142  isomnimap  7165  ismkvmap  7182  iswomnimap  7194  netap  7283  2omotaplemap  7286  recmulnqg  7420  nqtri3or  7425  ltmnqg  7430  mullocprlem  7599  addextpr  7650  gt0srpr  7777  ltsosr  7793  ltasrg  7799  map2psrprg  7834  xrlenlt  8052  letri3  8068  subadd  8190  ltsubadd2  8420  lesubadd2  8422  suble  8427  ltsub23  8429  ltaddpos2  8440  ltsubpos  8441  subge02  8465  ltaddsublt  8558  reapneg  8584  apsym  8593  apti  8609  leltap  8612  ap0gt0  8627  divmulap  8662  divmulap3  8664  rec11rap  8698  ltdiv1  8855  ltdivmul2  8865  ledivmul2  8867  ltrec  8870  suprleubex  8941  nnle1eq1  8973  avgle1  9189  avgle2  9190  nn0le0eq0  9234  znnnlt1  9331  zleltp1  9338  elz2  9354  uzm1  9588  uzin  9590  difrp  9722  xrletri3  9834  xgepnf  9846  xltnegi  9865  xltadd1  9906  xposdif  9912  xleaddadd  9917  elioo5  9963  elfz5  10047  fzdifsuc  10111  elfzm11  10121  uzsplit  10122  elfzonelfzo  10260  qtri3or  10273  qavgle  10289  flqbi  10321  flqbi2  10322  zmodid2  10383  q2submod  10416  sqap0  10618  lt2sq  10625  le2sq  10626  nn0opthlem1d  10732  bcval5  10775  zfz1isolemiso  10851  shftfib  10864  mulreap  10905  caucvgrelemcau  11021  caucvgre  11022  elicc4abs  11135  abs2difabs  11149  cau4  11157  maxclpr  11263  negfi  11268  lemininf  11274  mul0inf  11281  xrlemininf  11311  xrminltinf  11312  clim2  11323  climeq  11339  fisumss  11432  fsumabs  11505  isumshft  11530  absefib  11810  dvdsval3  11830  dvdslelemd  11881  dvdsabseq  11885  dvdsflip  11889  dvdsssfz1  11890  zeo3  11905  ndvdsadd  11968  dvdssq  12064  algcvgblem  12081  lcmdvds  12111  ncoprmgcdgt1b  12122  isprm3  12150  phiprmpw  12254  prmdiv  12267  pc11  12363  pcz  12364  pockthlem  12388  1arith  12399  ercpbllemg  12806  grpinvcnv  13012  eqger  13163  ablsubadd  13251  dvdsr02  13455  opprunitd  13460  unitsubm  13469  issubrg3  13594  aprval  13598  rnglidlmmgm  13812  discld  14096  isneip  14106  restopnb  14141  restopn2  14143  restdis  14144  lmbr2  14174  cnptoprest  14199  cnptoprest2  14200  tx1cn  14229  tx2cn  14230  txcnmpt  14233  txrest  14236  elbl2ps  14352  elbl2  14353  blcomps  14356  blcom  14357  xblpnfps  14358  xblpnf  14359  blpnf  14360  xmeter  14396  bdxmet  14461  metrest  14466  xmetxp  14467  metcn  14474  cncfcdm  14529  reefiso  14658  m1lgs  14913  2lgsoddprmlem2  14915