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  901  3anibar  1170  xor2dc  1412  bilukdc  1418  snelpwg  4275  prelpw  4278  reuhypd  4539  opelresi  4992  iota1  5269  funbrfv2b  5651  dffn5im  5652  fneqeql  5716  f1ompt  5759  dff13  5865  fliftcnv  5892  isotr  5913  isoini  5915  caovord3  6150  releldm2  6301  tpostpos  6380  nnsssuc  6618  nnaordi  6624  iserd  6676  ecdmn0m  6694  qliftel  6732  qliftfun  6734  qliftf  6737  ecopovsym  6748  pw2f1odclem  6963  mapen  6975  supisolem  7143  cnvti  7154  omp1eomlem  7229  ctssdc  7248  isomnimap  7272  ismkvmap  7289  iswomnimap  7301  netap  7408  2omotaplemap  7411  recmulnqg  7546  nqtri3or  7551  ltmnqg  7556  mullocprlem  7725  addextpr  7776  gt0srpr  7903  ltsosr  7919  ltasrg  7925  map2psrprg  7960  xrlenlt  8179  letri3  8195  subadd  8317  ltsubadd2  8548  lesubadd2  8550  suble  8555  ltsub23  8557  ltaddpos2  8568  ltsubpos  8569  subge02  8593  ltaddsublt  8686  reapneg  8712  apsym  8721  apti  8737  leltap  8740  ap0gt0  8755  divmulap  8790  divmulap3  8792  rec11rap  8826  ltdiv1  8983  ltdivmul2  8993  ledivmul2  8995  ltrec  8998  suprleubex  9069  nnle1eq1  9102  avgle1  9320  avgle2  9321  nn0le0eq0  9365  znnnlt1  9462  zleltp1  9470  elz2  9486  uzm1  9721  uzin  9723  difrp  9856  xrletri3  9968  xgepnf  9980  xltnegi  9999  xltadd1  10040  xposdif  10046  xleaddadd  10051  elioo5  10097  elfz5  10181  fzdifsuc  10245  elfzm11  10255  uzsplit  10256  elfzonelfzo  10403  qtri3or  10427  qavgle  10445  flqbi  10477  flqbi2  10478  fldiv4lem1div2uz2  10493  zmodid2  10541  q2submod  10574  sqap0  10795  lt2sq  10802  le2sq  10803  nn0opthlem1d  10909  bcval5  10952  zfz1isolemiso  11028  pfxsuffeqwrdeq  11196  shftfib  11300  mulreap  11341  caucvgrelemcau  11457  caucvgre  11458  elicc4abs  11571  abs2difabs  11585  cau4  11593  maxclpr  11699  negfi  11705  lemininf  11711  mul0inf  11718  xrlemininf  11748  xrminltinf  11749  clim2  11760  climeq  11776  fisumss  11869  fsumabs  11942  isumshft  11967  absefib  12248  dvdsval3  12268  dvdslelemd  12320  dvdsabseq  12324  dvdsflip  12328  dvdsssfz1  12329  zeo3  12345  ndvdsadd  12408  bitscmp  12435  dvdssq  12518  algcvgblem  12537  lcmdvds  12567  ncoprmgcdgt1b  12578  isprm3  12606  phiprmpw  12710  prmdiv  12723  pc11  12820  pcz  12821  pockthlem  12845  1arith  12856  ercpbllemg  13329  grpinvcnv  13567  eqger  13727  ablsubadd  13815  dvdsr02  14034  opprunitd  14039  unitsubm  14048  issubrg3  14176  aprval  14211  rnglidlmmgm  14425  znleval2  14583  discld  14775  isneip  14785  restopnb  14820  restopn2  14822  restdis  14823  lmbr2  14853  cnptoprest  14878  cnptoprest2  14879  tx1cn  14908  tx2cn  14909  txcnmpt  14912  txrest  14915  elbl2ps  15031  elbl2  15032  blcomps  15035  blcom  15036  xblpnfps  15037  xblpnf  15038  blpnf  15039  xmeter  15075  bdxmet  15140  metrest  15145  xmetxp  15146  metcn  15153  cncfcdm  15221  reefiso  15416  gausslemma2dlem0c  15695  lgseisenlem3  15716  lgsquadlem1  15721  m1lgs  15729  2lgsoddprmlem2  15750  ausgrusgrben  15931