Theorem bitr3d 190

Description: Deduction form of bitr3i 186. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr3d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr3d.2	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
bitr3d	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Proof of Theorem bitr3d

Step	Hyp	Ref	Expression
1		bitr3d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	bicomd 141	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
3		bitr3d.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 188	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitrrd  215  3bitr3d  218  3bitr3rd  219  pm5.16  840  biassdc  1444  pm5.24dc  1447  anxordi  1449  sbequ12a  1826  drex1  1851  sbcomxyyz  2032  sb9v  2038  csbiebt  3187  prsspwg  3875  ssprss  3876  bnd2  4310  copsex2t  4385  copsex2g  4386  fnssresb  5495  fcnvres  5575  foelcdmi  5755  dmfco  5773  funimass5  5826  fmptco  5874  cbvfo  5991  cbvexfo  5992  isocnv  6017  isoini  6024  isoselem  6026  riota2df  6060  ovmpodxf  6214  caovcanrd  6253  suppimacnvfn  6486  fidcenumlemrks  7270  ordiso2  7376  ltpiord  7687  dfplpq2  7722  dfmpq2  7723  enqeceq  7727  enq0eceq  7805  enreceq  8104  ltpsrprg  8171  mappsrprg  8172  cnegexlem3  8505  subeq0  8554  negcon1  8580  subexsub  8700  subeqrev  8704  lesub  8771  ltsub13  8773  subge0  8805  div11ap  9033  divmuleqap  9050  ltmuldiv2  9208  lemuldiv2  9215  nn1suc  9326  addltmul  9547  elnnnn0  9611  znn0sub  9715  prime  9750  indstr  10003  qapne  10049  qlttri2  10051  fz1n  10459  fzrev3  10505  fzo0n  10586  fzonlt0  10587  divfl0  10746  modqsubdir  10845  fzfig  10882  hashf1lem1  11301  wrdlenge1n0  11354  pfxccat3a  11526  sqrt11  11821  sqrtsq2  11825  absdiflt  11875  absdifle  11876  nnabscl  11883  minclpr  12021  xrnegiso  12047  xrnegcon1d  12049  clim2  12068  climshft2  12091  sumrbdc  12165  prodrbdclem2  12359  fprodssdc  12376  sinbnd  12538  cosbnd  12539  dvdscmulr  12606  dvdsmulcr  12607  oddm1even  12661  bitsmod  12742  bitsinv1lem  12747  qredeq  12893  cncongr2  12901  isprm3  12915  prmrp  12943  sqrt2irr  12960  crth  13025  pcdvdsb  13122  ballotfilemfc0  13284  ballotfilemfcc  13285  ssnnctlemct  13389  xpsfrnel2  13720  gzsumval2  13767  imasmnd2  13812  grpid  13897  grpidrcan  13923  grpidlcan  13924  grplmulf1o  13932  imasgrp2  13966  ghmeqker  14127  abladdsub4  14202  pwselbasb  14290  imasrng  14339  imasring  14453  lspsnss2  14840  znf1o  15070  znidom  15076  znunit  15078  znrrg  15079  eltg3  15249  eltop  15261  eltop2  15262  eltop3  15263  lmbrf  15407  cncnpi  15420  txcn  15467  hmeoimaf1o  15506  ismet2  15546  xmseq0  15660  wilthlem1  16198  fsumdvdsmul  16251  lgsne0  16328  lgsquadlem1  16367  lgsquadlem2  16368  2sqlem7  16411  clwwlkn1  16830  eupth2lem2dc  16871  eupth2lem3lem3fi  16882  eupth2lem3lem6fi  16883