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  2175  19.21t  2208  19.23t  2212  sbco2  2510  sbco3  2512  sbal1  2527  sbal2  2528  clelab  2874  ceqsralt  3469  csbiebt  3877  prsspwg  4773  ssprss  4774  reusv2lem5  5338  copsex2t  5430  ordtri2  6337  onmindif  6396  fnssresb  6599  fcnvres  6696  foelcdmi  6878  funimass5  6983  fmptco  7057  cbvfo  7218  isocnv  7259  isoini  7267  isoselem  7270  riota2df  7321  ovmpodxf  7491  caovcanrd  7544  onmindif2  7735  ordunisuc2  7769  dfom2  7793  frxp2  8069  xpord2pred  8070  xpord3pred  8077  ordge1n0  8404  ondif2  8412  oa00  8469  odi  8489  oeoe  8509  eceqoveq  8741  isfinite2  9177  unfilem1  9184  fodomfib  9208  fodomfibOLD  9210  inficl  9304  dffi3  9310  ordiso2  9396  ordtypelem9  9407  cantnfle  9556  cantnf  9578  wemapwe  9582  rankr1a  9721  bnd2  9778  iscard  9860  domtri2  9874  nnsdomel  9875  cardaleph  9972  dfac12lem2  10028  cfss  10148  axcc3  10321  fodomb  10409  iundom2g  10423  inar1  10658  ltpiord  10770  ordpinq  10826  suplem2pr  10936  enreceq  10949  subeq0  11379  negcon1  11405  subexsub  11527  subeqrev  11531  lesub  11588  ltsub13  11590  subge0  11622  mul0or  11749  mulcan1g  11762  div11OLD  11797  divmuleq  11818  mdiv  11949  ltmuldiv2  11988  lemuldiv2  11995  nn1suc  12139  addltmul  12349  elnnnn0  12416  znn0sub  12511  prime  12546  zbtwnre  12836  xadddi2  13188  supxrbnd  13219  fz1n  13434  fzrev3  13482  fzo0n  13573  fzonlt0  13574  ico01fl0  13715  divfl0  13720  modaddid  13806  modsubdir  13839  om2uzlt2i  13850  hashf1lem1  14354  wrdlenge1n0  14449  pfxccat3a  14637  cnpart  15139  sqrt11  15161  sqrtsq2  15167  absdiflt  15217  absdifle  15218  sqreulem  15259  sqreu  15260  eqsqrtor  15266  clim2  15403  climshft2  15481  isercoll  15567  sumrb  15612  supcvg  15755  prodrblem2  15830  sinbnd  16081  cosbnd  16082  sqrt2irr  16150  dvdscmulr  16187  dvdsmulcr  16188  oddm1even  16246  bitsmod  16339  bitsinv1lem  16344  qredeq  16560  cncongr2  16571  isprm3  16586  prmrp  16615  crth  16681  pcdvdsb  16773  pceq0  16775  unbenlem  16812  ramcl  16933  pwselbasb  17384  pwsle  17388  imasleval  17437  xpsfrnel2  17460  acsfn  17557  ismon2  17633  isepi2  17640  epii  17642  fthsect  17826  fthmon  17828  isipodrs  18435  ipodrsfi  18437  gsumval2a  18585  imasmnd2  18674  grpid  18880  grpidrcan  18908  grpidlcan  18909  grplmulf1o  18918  grpraddf1o  18919  imasgrp2  18960  eqg0subg  19101  ghmeqker  19148  gacan  19210  odmulgeq  19462  pgpssslw  19519  efgsfo  19644  efgred  19653  abladdsub4  19716  subgdmdprd  19941  imasrng  20088  imasring  20241  0ring01eqbi  20440  domneq0r  20632  lspsnss2  20931  znf1o  21481  znfld  21490  znunit  21493  znrrg  21495  iporthcom  21565  ip2eq  21583  obsne0  21655  lindfmm  21757  lindsmm  21758  lsslinds  21761  gsumbagdiaglem  21860  psdmul  22074  eltg3  22870  eltop  22882  eltop2  22883  eltop3  22884  lmbrf  23168  cncnpi  23186  dfconn2  23327  1stcfb  23353  elptr  23481  xkoccn  23527  txcn  23534  hausdiag  23553  hmeoimaf1o  23678  isfbas  23737  ufileu  23827  alexsubALTlem4  23958  tsmsf1o  24053  ismet2  24241  imasdsf1olem  24281  imasf1oxmet  24283  imasf1omet  24284  xmseq0  24372  imasf1oxms  24397  metucn  24479  nrmmetd  24482  nmgt0  24538  nlmmul0or  24591  xrsxmet  24718  metdseq0  24763  elpi1i  24966  cphsqrtcl2  25106  tcphcph  25157  lmmbrf  25182  caucfil  25203  lmclim  25223  cmsss  25271  srabn  25280  ovolfioo  25388  ovolficc  25389  elovolmr  25397  ovolctb  25411  ovolicc2lem3  25440  mbfmulc2lem  25568  mbfimaopnlem  25576  itg2mulclem  25667  iblrelem  25712  ellimc2  25798  mdegle0  26002  fta1glem2  26094  dgreq0  26191  plydivlem4  26224  plydivex  26225  fta1  26236  quotcan  26237  logeftb  26512  quad2  26769  cubic2  26778  dquartlem1  26781  atandm4  26809  fsumharmonic  26942  wilthlem1  26998  basellem8  27018  mumullem2  27110  fsumdvdsmul  27125  chpchtsum  27150  logfaclbnd  27153  dchrelbas4  27174  lgsne0  27266  lgsqrlem2  27278  lgsdchrval  27285  lgsquadlem1  27311  lgsquadlem2  27312  2sqlem7  27355  addsqrexnreu  27373  dchrisum0lem1  27447  nogt01o  27628  slenlt  27684  addscan1  27930  subseq0d  28037  mulscan2d  28111  mulscan1d  28112  muls0ord  28117  sltmuldiv2wd  28134  onnolt  28196  onslt  28197  om2noseqlt2  28223  zn0subs  28320  trgcgrg  28486  tgcgr4  28502  tgcolg  28525  lmiinv  28763  iseqlg  28838  elntg2  28956  cusgruvtxb  29393  upgrewlkle2  29578  clwwlkn1  30011  eupth2lem3lem3  30200  eupth2lem3lem6  30203  frgr3vlem2  30244  grpoid  30490  nvmeq0  30628  nvgt0  30644  imsmetlem  30660  nmlnogt0  30767  ip2eqi  30826  hvaddcan2  31041  hvmulcan2  31043  hvaddsub4  31048  hi2eq  31075  pjhtheu  31364  lnopeqi  31978  riesz1  32035  jpi  32240  chcv2  32326  cvp  32345  atnemeq0  32347  brabgaf  32579  fmptcof2  32629  funcnvmpt  32639  nndiffz1  32759  nn0min  32793  sgnneg  32806  xrge0addgt0  32988  lbslsp  33332  ressply1mon1p  33521  fldextrspunlsplem  33676  smatrcl  33799  lmlim  33950  carsggect  34321  eulerpartlems  34363  eulerpartlemgh  34381  ballotlemfc0  34496  ballotlemfcc  34497  signsvfpn  34588  signsvfnn  34589  reprdifc  34630  bnj1280  35022  fineqvnttrclselem3  35111  lfuhgr  35130  satffunlem1lem2  35415  elmrsubrn  35532  msubff1  35568  fz0n  35743  imageval  35943  nn0prpwlem  36335  filnetlem4  36394  onsuct0  36454  onint1  36462  dissneqlem  37353  fvineqsneu  37424  wl-sbalnae  37575  wl-ax11-lem8  37605  wl-ax11-lem10  37607  sin2h  37629  tan2h  37631  matunitlindflem1  37635  matunitlindflem2  37636  matunitlindf  37637  poimirlem18  37657  poimirlem21  37660  poimirlem24  37663  heicant  37674  mblfinlem3  37678  ovoliunnfl  37681  voliunnfl  37683  volsupnfl  37684  mbfresfi  37685  mbfposadd  37686  itg2addnclem  37690  itg2addnclem2  37691  itg2addnc  37693  itg2gt0cn  37694  itgaddnclem2  37698  ftc1anclem5  37716  areacirclem1  37727  areacirclem4  37730  areacirc  37732  isdmn3  38093  eldmres2  38289  cnvref4  38357  relbrcoss  38462  releldmqs  38675  lcvp  39058  lcv2  39060  lsatnem0  39063  atnem0  39336  cvlsupr2  39361  cvr2N  39429  athgt  39474  2llnmat  39542  pmap11  39780  pmapeq0  39784  2lnat  39802  paddclN  39860  pmapjat1  39871  ltrn2ateq  40198  dihcnvord  41292  dihcnv11  41293  dih0bN  41299  dih0sb  41303  dihlspsnat  41351  dihatexv2  41357  dihglblem6  41358  dochvalr  41375  dochn0nv  41393  djhcvat42  41433  dochsatshp  41469  dochshpsat  41472  dochkrsat2  41474  lcfl5a  41515  lcfl8a  41521  lclkrlem2a  41525  mapdcnvordN  41676  hdmap14lem4a  41889  hgmapeq0  41922  hdmaplkr  41931  hdmapellkr  41932  cxp111d  42354  sn-remul0ord  42420  sn-ltmulgt11d  42486  frlmfielbas  42512  eu6w  42688  rmxycomplete  42929  gicabl  43111  minregex2  43547  ntrneiel  44093  ntrneik4w  44112  ntrneik4  44113  extoimad  44176  radcnvrat  44326  pm14.123b  44438  iotavalb  44442  infxrunb3  45441  climreeq  45632  clim2f  45653  clim2f2  45687  dfodd4  47669  oddprmne2  47725  nnsgrpnmnd  48188  ovmpordxf  48349  eenglngeehlnmlem2  48749  iscnrm3  48962  uptrlem1  49221