Theorem bitr3d 281

Description: Deduction form of bitr3i 277. (Contributed by NM, 14-May-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 223	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
3		bitr3d.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 279	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  3bitrrd  306  3bitr3d  309  3bitr3rd  310  biass  384  sbcom2  2170  19.21t  2203  19.23t  2207  sbco2  2513  sbco3  2515  sbal1  2530  sbal2  2531  clelab  2884  ceqsralt  3513  csbiebt  3937  prsspwg  4827  ssprss  4828  reusv2lem5  5407  copsex2t  5502  ordtri2  6420  onmindif  6477  fnssresb  6690  fcnvres  6785  foelcdmi  6969  funimass5  7074  fmptco  7148  cbvfo  7308  isocnv  7349  isoini  7357  isoselem  7360  riota2df  7410  ovmpodxf  7582  caovcanrd  7635  onmindif2  7826  ordunisuc2  7864  dfom2  7888  frxp2  8167  xpord2pred  8168  xpord3pred  8175  ordge1n0  8530  ondif2  8538  oa00  8595  odi  8615  oeoe  8635  eceqoveq  8860  isfinite2  9331  unfilem1  9340  fodomfib  9366  fodomfibOLD  9368  inficl  9462  dffi3  9468  ordiso2  9552  ordtypelem9  9563  cantnfle  9708  cantnf  9730  wemapwe  9734  rankr1a  9873  bnd2  9930  iscard  10012  domtri2  10026  nnsdomel  10027  cardaleph  10126  dfac12lem2  10182  cfss  10302  axcc3  10475  fodomb  10563  iundom2g  10577  inar1  10812  ltpiord  10924  ordpinq  10980  suplem2pr  11090  enreceq  11103  subeq0  11532  negcon1  11558  subexsub  11678  subeqrev  11682  lesub  11739  ltsub13  11741  subge0  11773  mul0or  11900  mulcan1g  11913  div11OLD  11948  divmuleq  11969  mdiv  12100  ltmuldiv2  12139  lemuldiv2  12146  nn1suc  12285  addltmul  12499  elnnnn0  12566  znn0sub  12661  prime  12696  zbtwnre  12985  xadddi2  13335  supxrbnd  13366  fz1n  13578  fzrev3  13626  fzo0n  13717  fzonlt0  13718  ico01fl0  13855  divfl0  13860  modsubdir  13977  om2uzlt2i  13988  hashf1lem1  14490  wrdlenge1n0  14584  pfxccat3a  14772  cnpart  15275  sqrt11  15297  sqrtsq2  15303  absdiflt  15352  absdifle  15353  sqreulem  15394  sqreu  15395  eqsqrtor  15401  clim2  15536  climshft2  15614  isercoll  15700  sumrb  15745  supcvg  15888  prodrblem2  15963  sinbnd  16212  cosbnd  16213  sqrt2irr  16281  dvdscmulr  16318  dvdsmulcr  16319  oddm1even  16376  bitsmod  16469  bitsinv1lem  16474  qredeq  16690  cncongr2  16701  isprm3  16716  prmrp  16745  crth  16811  pcdvdsb  16902  pceq0  16904  unbenlem  16941  ramcl  17062  pwselbasb  17534  pwsle  17538  imasleval  17587  xpsfrnel2  17610  acsfn  17703  ismon2  17781  isepi2  17788  epii  17790  fthsect  17978  fthmon  17980  isipodrs  18594  ipodrsfi  18596  gsumval2a  18710  imasmnd2  18799  grpid  19005  grpidrcan  19033  grpidlcan  19034  grplmulf1o  19043  grpraddf1o  19044  imasgrp2  19085  eqg0subg  19226  ghmeqker  19273  gacan  19335  odmulgeq  19589  pgpssslw  19646  efgsfo  19771  efgred  19780  abladdsub4  19843  subgdmdprd  20068  imasrng  20194  imasring  20343  0ring01eqbi  20548  domneq0r  20740  lspsnss2  21020  znf1o  21587  znfld  21596  znunit  21599  znrrg  21601  iporthcom  21670  ip2eq  21688  obsne0  21762  lindfmm  21864  lindsmm  21865  lsslinds  21868  gsumbagdiaglem  21967  psdmul  22187  eltg3  22984  eltop  22996  eltop2  22997  eltop3  22998  lmbrf  23283  cncnpi  23301  dfconn2  23442  1stcfb  23468  elptr  23596  xkoccn  23642  txcn  23649  hausdiag  23668  hmeoimaf1o  23793  isfbas  23852  ufileu  23942  alexsubALTlem4  24073  tsmsf1o  24168  ismet2  24358  imasdsf1olem  24398  imasf1oxmet  24400  imasf1omet  24401  xmseq0  24489  imasf1oxms  24517  metucn  24599  nrmmetd  24602  nmgt0  24658  nlmmul0or  24719  xrsxmet  24844  metdseq0  24889  elpi1i  25092  cphsqrtcl2  25233  tcphcph  25284  lmmbrf  25309  caucfil  25330  lmclim  25350  cmsss  25398  srabn  25407  ovolfioo  25515  ovolficc  25516  elovolmr  25524  ovolctb  25538  ovolicc2lem3  25567  mbfmulc2lem  25695  mbfimaopnlem  25703  itg2mulclem  25795  iblrelem  25840  ellimc2  25926  mdegle0  26130  fta1glem2  26222  dgreq0  26319  plydivlem4  26352  plydivex  26353  fta1  26364  quotcan  26365  logeftb  26639  quad2  26896  cubic2  26905  dquartlem1  26908  atandm4  26936  fsumharmonic  27069  wilthlem1  27125  basellem8  27145  mumullem2  27237  fsumdvdsmul  27252  chpchtsum  27277  logfaclbnd  27280  dchrelbas4  27301  lgsne0  27393  lgsqrlem2  27405  lgsdchrval  27412  lgsquadlem1  27438  lgsquadlem2  27439  2sqlem7  27482  addsqrexnreu  27500  dchrisum0lem1  27574  nogt01o  27755  slenlt  27811  addscan1  28041  mulscan2d  28219  mulscan1d  28220  muls0ord  28225  sltmuldiv2wd  28241  om2noseqlt2  28320  zn0subs  28403  trgcgrg  28537  tgcgr4  28553  tgcolg  28576  lmiinv  28814  iseqlg  28889  elntg2  29014  cusgruvtxb  29453  upgrewlkle2  29638  clwwlkn1  30069  eupth2lem3lem3  30258  eupth2lem3lem6  30261  frgr3vlem2  30302  grpoid  30548  nvmeq0  30686  nvgt0  30702  imsmetlem  30718  nmlnogt0  30825  ip2eqi  30884  hvaddcan2  31099  hvmulcan2  31101  hvaddsub4  31106  hi2eq  31133  pjhtheu  31422  lnopeqi  32036  riesz1  32093  jpi  32298  chcv2  32384  cvp  32403  atnemeq0  32405  brabgaf  32627  fmptcof2  32673  funcnvmpt  32683  nndiffz1  32794  nn0min  32826  xrge0addgt0  33004  lbslsp  33384  ressply1mon1p  33572  smatrcl  33756  lmlim  33907  carsggect  34299  eulerpartlems  34341  eulerpartlemgh  34359  ballotlemfc0  34473  ballotlemfcc  34474  sgnneg  34521  signsvfpn  34578  signsvfnn  34579  reprdifc  34620  bnj1280  35012  lfuhgr  35101  satffunlem1lem2  35387  elmrsubrn  35504  msubff1  35540  fz0n  35710  imageval  35911  nn0prpwlem  36304  filnetlem4  36363  onsuct0  36423  onint1  36431  dissneqlem  37322  fvineqsneu  37393  wl-sbalnae  37542  wl-ax11-lem8  37572  wl-ax11-lem10  37574  sin2h  37596  tan2h  37598  matunitlindflem1  37602  matunitlindflem2  37603  matunitlindf  37604  poimirlem18  37624  poimirlem21  37627  poimirlem24  37630  heicant  37641  mblfinlem3  37645  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  mbfresfi  37652  mbfposadd  37653  itg2addnclem  37657  itg2addnclem2  37658  itg2addnc  37660  itg2gt0cn  37661  itgaddnclem2  37665  ftc1anclem5  37683  areacirclem1  37694  areacirclem4  37697  areacirc  37699  isdmn3  38060  eldmres2  38256  cnvref4  38331  relbrcoss  38427  releldmqs  38639  lcvp  39021  lcv2  39023  lsatnem0  39026  atnem0  39299  cvlsupr2  39324  cvr2N  39393  athgt  39438  2llnmat  39506  pmap11  39744  pmapeq0  39748  2lnat  39766  paddclN  39824  pmapjat1  39835  ltrn2ateq  40162  dihcnvord  41256  dihcnv11  41257  dih0bN  41263  dih0sb  41267  dihlspsnat  41315  dihatexv2  41321  dihglblem6  41322  dochvalr  41339  dochn0nv  41357  djhcvat42  41397  dochsatshp  41433  dochshpsat  41436  dochkrsat2  41438  lcfl5a  41479  lcfl8a  41485  lclkrlem2a  41489  mapdcnvordN  41640  hdmap14lem4a  41853  hgmapeq0  41886  hdmaplkr  41895  hdmapellkr  41896  metakunt15  42200  cxp111d  42356  sn-ltmulgt11d  42468  frlmfielbas  42486  eu6w  42662  rmxycomplete  42905  gicabl  43087  minregex2  43524  ntrneiel  44070  ntrneik4w  44089  ntrneik4  44090  extoimad  44153  radcnvrat  44309  pm14.123b  44421  iotavalb  44425  infxrunb3  45373  climreeq  45568  clim2f  45591  clim2f2  45625  dfodd4  47583  oddprmne2  47639  nnsgrpnmnd  48021  ovmpordxf  48183  eenglngeehlnmlem2  48587  iscnrm3  48748