Theorem bitr3d 283

Description: Deduction form of bitr3i 279. (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 225	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
3		bitr3d.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 281	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3bitrrd  308  3bitr3d  311  3bitr3rd  312  biass  388  sbcom2  2164  19.21t  2202  19.23t  2206  sbco2  2549  sbco3  2551  sbal1  2568  sbal2  2569  sbal2OLD  2570  sbalOLD  2571  sbco2ALT  2611  csbiebt  3911  prsspwg  4749  ssprss  4750  reusv2lem5  5294  copsex2t  5375  copsex2g  5376  ordtri2  6220  onmindif  6274  fnssresb  6463  fcnvres  6550  foelrni  6721  funimass5  6819  fmptco  6885  cbvfo  7039  isocnv  7077  isoini  7085  isoselem  7088  riota2df  7131  ovmpodxf  7294  caovcanrd  7345  onmindif2  7521  ordunisuc2  7553  dfom2  7576  ordge1n0  8117  ondif2  8121  oa00  8179  odi  8199  oeoe  8219  eceqoveq  8396  isfinite2  8770  unfilem1  8776  fodomfib  8792  inficl  8883  dffi3  8889  ordiso2  8973  ordtypelem9  8984  cantnfle  9128  cantnf  9150  wemapwe  9154  rankr1a  9259  bnd2  9316  iscard  9398  domtri2  9412  nnsdomel  9413  cardaleph  9509  dfac12lem2  9564  cfss  9681  axcc3  9854  fodomb  9942  iundom2g  9956  inar1  10191  ltpiord  10303  ordpinq  10359  suplem2pr  10469  enreceq  10482  subeq0  10906  negcon1  10932  subexsub  11052  subeqrev  11056  lesub  11113  ltsub13  11115  subge0  11147  mul0or  11274  mulcan1g  11287  div11  11320  divmuleq  11339  mdiv  11470  ltmuldiv2  11508  lemuldiv2  11515  nn1suc  11653  addltmul  11867  elnnnn0  11934  znn0sub  12023  prime  12057  zbtwnre  12340  xadddi2  12684  supxrbnd  12715  fz1n  12919  fzrev3  12967  fzo0n  13053  fzonlt0  13054  ico01fl0  13183  divfl0  13188  modsubdir  13302  om2uzlt2i  13313  hashf1lem1  13807  wrdlenge1n0  13896  pfxccat3a  14094  cnpart  14593  sqrt11  14616  sqrtsq2  14622  absdiflt  14671  absdifle  14672  sqreulem  14713  sqreu  14714  eqsqrtor  14720  clim2  14855  climshft2  14933  isercoll  15018  sumrb  15064  supcvg  15205  prodrblem2  15279  sinbnd  15527  cosbnd  15528  sqrt2irr  15596  dvdscmulr  15632  dvdsmulcr  15633  oddm1even  15686  bitsmod  15779  bitsinv1lem  15784  qredeq  15995  cncongr2  16006  isprm3  16021  prmrp  16050  crth  16109  pcdvdsb  16199  pceq0  16201  unbenlem  16238  ramcl  16359  pwselbasb  16755  pwsle  16759  imasleval  16808  xpsfrnel2  16831  acsfn  16924  ismon2  16998  isepi2  17005  epii  17007  fthsect  17189  fthmon  17191  isipodrs  17765  ipodrsfi  17767  gsumval2a  17889  imasmnd2  17942  grpid  18133  grpidrcan  18158  grpidlcan  18159  grplmulf1o  18167  imasgrp2  18208  ghmeqker  18379  ghmf1  18381  gacan  18429  odmulgeq  18678  pgpssslw  18733  efgsfo  18859  efgred  18868  abladdsub4  18928  subgdmdprd  19150  imasring  19363  lspsnss2  19771  0ring01eqbi  20040  gsumbagdiaglem  20149  znf1o  20692  znfld  20701  znunit  20704  znrrg  20706  iporthcom  20773  ip2eq  20791  obsne0  20863  lindfmm  20965  lindsmm  20966  lsslinds  20969  eltg3  21564  eltop  21576  eltop2  21577  eltop3  21578  lmbrf  21862  cncnpi  21880  dfconn2  22021  1stcfb  22047  elptr  22175  xkoccn  22221  txcn  22228  hausdiag  22247  hmeoimaf1o  22372  isfbas  22431  ufileu  22521  alexsubALTlem4  22652  tsmsf1o  22747  ismet2  22937  imasdsf1olem  22977  imasf1oxmet  22979  imasf1omet  22980  xmseq0  23068  imasf1oxms  23093  metucn  23175  nrmmetd  23178  nmgt0  23233  nlmmul0or  23286  xrsxmet  23411  metdseq0  23456  elpi1i  23644  cphsqrtcl2  23784  tcphcph  23834  lmmbrf  23859  caucfil  23880  lmclim  23900  cmsss  23948  srabn  23957  ovolfioo  24062  ovolficc  24063  elovolmr  24071  ovolctb  24085  ovolicc2lem3  24114  mbfmulc2lem  24242  mbfimaopnlem  24250  itg2mulclem  24341  iblrelem  24385  ellimc2  24469  mdegle0  24665  fta1glem2  24754  dgreq0  24849  plydivlem4  24879  plydivex  24880  fta1  24891  quotcan  24892  logeftb  25161  quad2  25411  cubic2  25420  dquartlem1  25423  atandm4  25451  fsumharmonic  25583  wilthlem1  25639  basellem8  25659  mumullem2  25751  chpchtsum  25789  logfaclbnd  25792  dchrelbas4  25813  lgsne0  25905  lgsqrlem2  25917  lgsdchrval  25924  lgsquadlem1  25950  lgsquadlem2  25951  2sqlem7  25994  addsqrexnreu  26012  dchrisum0lem1  26086  trgcgrg  26295  tgcgr4  26311  tgcolg  26334  lmiinv  26572  iseqlg  26647  elntg2  26765  cusgruvtxb  27198  upgrewlkle2  27382  clwwlkn1  27813  eupth2lem3lem3  28003  eupth2lem3lem6  28006  frgr3vlem2  28047  grpoid  28291  nvmeq0  28429  nvgt0  28445  imsmetlem  28461  nmlnogt0  28568  ip2eqi  28627  hvaddcan2  28842  hvmulcan2  28844  hvaddsub4  28849  hi2eq  28876  pjhtheu  29165  lnopeqi  29779  riesz1  29836  jpi  30041  chcv2  30127  cvp  30146  atnemeq0  30148  brabgaf  30353  fmptcof2  30396  funcnvmpt  30406  nndiffz1  30503  nn0min  30531  xrge0addgt0  30673  lbslsp  30933  smatrcl  31056  lmlim  31185  carsggect  31571  eulerpartlems  31613  eulerpartlemgh  31631  ballotlemfc0  31745  ballotlemfcc  31746  sgnneg  31793  signsvfpn  31850  signsvfnn  31851  reprdifc  31893  bnj1280  32287  lfuhgr  32359  satffunlem1lem2  32645  elmrsubrn  32762  msubff1  32798  fz0n  32957  slenlt  33226  imageval  33386  nn0prpwlem  33665  filnetlem4  33724  onsuct0  33784  onint1  33792  dissneqlem  34615  fvineqsneu  34686  wl-sbalnae  34792  wl-ax11-lem8  34818  wl-ax11-lem10  34820  sin2h  34876  tan2h  34878  matunitlindflem1  34882  matunitlindflem2  34883  matunitlindf  34884  poimirlem18  34904  poimirlem21  34907  poimirlem24  34910  heicant  34921  mblfinlem3  34925  ovoliunnfl  34928  voliunnfl  34930  volsupnfl  34931  mbfresfi  34932  mbfposadd  34933  itg2addnclem  34937  itg2addnclem2  34938  itg2addnc  34940  itg2gt0cn  34941  itgaddnclem2  34945  ftc1anclem5  34965  areacirclem1  34976  areacirclem4  34979  areacirc  34981  isdmn3  35346  eldmres2  35526  relbrcoss  35680  releldmqs  35886  lcvp  36170  lcv2  36172  lsatnem0  36175  atnem0  36448  cvlsupr2  36473  cvr2N  36541  athgt  36586  2llnmat  36654  pmap11  36892  pmapeq0  36896  2lnat  36914  paddclN  36972  pmapjat1  36983  ltrn2ateq  37310  dihcnvord  38404  dihcnv11  38405  dih0bN  38411  dih0sb  38415  dihlspsnat  38463  dihatexv2  38469  dihglblem6  38470  dochvalr  38487  dochn0nv  38505  djhcvat42  38545  dochsatshp  38581  dochshpsat  38584  dochkrsat2  38586  lcfl5a  38627  lcfl8a  38633  lclkrlem2a  38637  mapdcnvordN  38788  hdmap14lem4a  39001  hgmapeq0  39034  hdmaplkr  39043  hdmapellkr  39044  frlmfielbas  39132  rmxycomplete  39507  gicabl  39692  ntrneiel  40424  ntrneik4w  40443  ntrneik4  40444  extoimad  40508  radcnvrat  40639  pm14.123b  40751  iotavalb  40755  infxrunb3  41691  climreeq  41887  clim2f  41910  clim2f2  41944  dfodd4  43818  oddprmne2  43874  nnsgrpnmnd  44079  ovmpordxf  44381  eenglngeehlnmlem2  44719