Theorem bitr3d 273

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  3bitrrd  298  3bitr3d  301  3bitr3rd  302  biass  377  19.21t  2135  19.23t  2139  sbcom2  2410  sbcom2OLD  2411  sbco2  2477  sbco3  2479  sbal1  2495  sbal2  2496  sbal2OLD  2497  sbal2OLDOLD  2498  sbalOLD  2500  sbco2ALT  2542  csbiebt  3802  prsspwg  4624  ssprss  4625  reusv2lem5  5150  copsex2t  5233  copsex2g  5234  ordtri2  6058  onmindif  6112  fnssresb  6296  fcnvres  6379  foelrni  6551  funimass5  6644  fmptco  6708  cbvfo  6864  isocnv  6900  isoini  6908  isoselem  6911  riota2df  6951  ovmpodxf  7110  caovcanrd  7161  onmindif2  7337  ordunisuc2  7369  dfom2  7392  ordge1n0  7919  ondif2  7923  oa00  7980  odi  8000  oeoe  8020  eceqoveq  8196  isfinite2  8565  unfilem1  8571  fodomfib  8587  inficl  8678  dffi3  8684  ordiso2  8768  ordtypelem9  8779  cantnfle  8922  cantnf  8944  wemapwe  8948  rankr1a  9053  bnd2  9110  iscard  9192  domtri2  9206  nnsdomel  9207  cardaleph  9303  dfac12lem2  9358  cfss  9479  axcc3  9652  fodomb  9740  iundom2g  9754  inar1  9989  ltpiord  10101  ordpinq  10157  suplem2pr  10267  enreceq  10280  subeq0  10707  negcon1  10733  subexsub  10853  subeqrev  10857  lesub  10914  ltsub13  10916  subge0  10948  mul0or  11075  mulcan1g  11088  div11  11121  divmuleq  11140  mdiv  11271  ltmuldiv2  11309  lemuldiv2  11316  nn1suc  11456  addltmul  11677  elnnnn0  11746  znn0sub  11836  prime  11870  zbtwnre  12154  xadddi2  12500  supxrbnd  12531  fz1n  12735  fzrev3  12783  fzo0n  12868  fzonlt0  12869  ico01fl0  12998  divfl0  13003  modsubdir  13117  om2uzlt2i  13128  hashf1lem1  13620  wrdlenge1n0  13707  ccat0  13733  pfxccat3a  13936  cnpart  14454  sqrt11  14477  sqrtsq2  14483  absdiflt  14532  absdifle  14533  sqreulem  14574  sqreu  14575  eqsqrtor  14581  clim2  14716  climshft2  14794  isercoll  14879  sumrb  14924  supcvg  15065  prodrblem2  15139  sinbnd  15387  cosbnd  15388  sqrt2irr  15456  dvdscmulr  15492  dvdsmulcr  15493  oddm1even  15546  bitsmod  15639  bitsinv1lem  15644  qredeq  15851  cncongr2  15862  isprm3  15877  prmrp  15906  crth  15965  pcdvdsb  16055  pceq0  16057  unbenlem  16094  ramcl  16215  pwselbasb  16611  pwsle  16615  imasleval  16664  xpsfrnel2  16688  acsfn  16782  ismon2  16856  isepi2  16863  epii  16865  fthsect  17047  fthmon  17049  isipodrs  17623  ipodrsfi  17625  gsumval2a  17741  imasmnd2  17789  grpid  17920  grpidrcan  17945  grpidlcan  17946  grplmulf1o  17954  imasgrp2  17995  ghmeqker  18150  ghmf1  18152  gacan  18200  odmulgeq  18439  pgpssslw  18494  efgsfo  18618  efgred  18628  abladdsub4  18686  subgdmdprd  18900  imasring  19086  lspsnss2  19493  0ring01eqbi  19761  gsumbagdiaglem  19863  znf1o  20394  znfld  20403  znunit  20406  znrrg  20408  iporthcom  20475  ip2eq  20493  obsne0  20565  lindfmm  20667  lindsmm  20668  lsslinds  20671  eltg3  21268  eltop  21280  eltop2  21281  eltop3  21282  lmbrf  21566  cncnpi  21584  dfconn2  21725  1stcfb  21751  elptr  21879  xkoccn  21925  txcn  21932  hausdiag  21951  hmeoimaf1o  22076  isfbas  22135  ufileu  22225  alexsubALTlem4  22356  tsmsf1o  22450  ismet2  22640  imasdsf1olem  22680  imasf1oxmet  22682  imasf1omet  22683  xmseq0  22771  imasf1oxms  22796  metucn  22878  nrmmetd  22881  nmgt0  22936  nlmmul0or  22989  xrsxmet  23114  metdseq0  23159  elpi1i  23347  cphsqrtcl2  23487  tcphcph  23537  lmmbrf  23562  caucfil  23583  lmclim  23603  cmsss  23651  srabn  23660  ovolfioo  23765  ovolficc  23766  elovolmr  23774  ovolctb  23788  ovolicc2lem3  23817  mbfmulc2lem  23945  mbfimaopnlem  23953  itg2mulclem  24044  iblrelem  24088  ellimc2  24172  mdegle0  24368  fta1glem2  24457  dgreq0  24552  plydivlem4  24582  plydivex  24583  fta1  24594  quotcan  24595  logeftb  24862  quad2  25112  cubic2  25121  dquartlem1  25124  atandm4  25152  fsumharmonic  25285  wilthlem1  25341  basellem8  25361  mumullem2  25453  chpchtsum  25491  logfaclbnd  25494  dchrelbas4  25515  lgsne0  25607  lgsqrlem2  25619  lgsdchrval  25626  lgsquadlem1  25652  lgsquadlem2  25653  2sqlem7  25696  addsqrexnreu  25714  dchrisum0lem1  25788  trgcgrg  25997  tgcgr4  26013  tgcolg  26036  lmiinv  26274  iseqlg  26350  elntg2  26468  cusgruvtxb  26901  upgrewlkle2  27085  clwwlkn1  27551  eupth2lem3lem3  27754  eupth2lem3lem6  27757  frgr3vlem2  27802  grpoid  28068  nvmeq0  28206  nvgt0  28222  imsmetlem  28238  nmlnogt0  28345  ip2eqi  28405  hvaddcan2  28621  hvmulcan2  28623  hvaddsub4  28628  hi2eq  28655  pjhtheu  28946  lnopeqi  29560  riesz1  29617  jpi  29822  chcv2  29908  cvp  29927  atnemeq0  29929  brabgaf  30117  fmptcof2  30158  funcnvmpt  30168  nndiffz1  30262  nn0min  30284  xrge0addgt0  30410  lbslsp  30609  smatrcl  30703  lmlim  30834  carsggect  31221  eulerpartlems  31263  eulerpartlemgh  31281  ballotlemfc0  31396  ballotlemfcc  31397  sgnneg  31444  signsvfpn  31503  signsvfnn  31504  reprdifc  31546  bnj1280  31937  elmrsubrn  32287  msubff1  32323  fz0n  32482  slenlt  32752  imageval  32912  nn0prpwlem  33191  filnetlem4  33250  onsuct0  33309  onint1  33317  dissneqlem  34063  fvineqsneu  34133  wl-sbalnae  34239  wl-ax11-lem8  34265  wl-ax11-lem10  34267  sin2h  34323  tan2h  34325  matunitlindflem1  34329  matunitlindflem2  34330  matunitlindf  34331  poimirlem18  34351  poimirlem21  34354  poimirlem24  34357  heicant  34368  mblfinlem3  34372  ovoliunnfl  34375  voliunnfl  34377  volsupnfl  34378  mbfresfi  34379  mbfposadd  34380  itg2addnclem  34384  itg2addnclem2  34385  itg2addnc  34387  itg2gt0cn  34388  itgaddnclem2  34392  ftc1anclem5  34412  areacirclem1  34423  areacirclem4  34426  areacirc  34428  isdmn3  34794  eldmres2  34976  relbrcoss  35131  releldmqs  35337  lcvp  35621  lcv2  35623  lsatnem0  35626  atnem0  35899  cvlsupr2  35924  cvr2N  35992  athgt  36037  2llnmat  36105  pmap11  36343  pmapeq0  36347  2lnat  36365  paddclN  36423  pmapjat1  36434  ltrn2ateq  36761  dihcnvord  37855  dihcnv11  37856  dih0bN  37862  dih0sb  37866  dihlspsnat  37914  dihatexv2  37920  dihglblem6  37921  dochvalr  37938  dochn0nv  37956  djhcvat42  37996  dochsatshp  38032  dochshpsat  38035  dochkrsat2  38037  lcfl5a  38078  lcfl8a  38084  lclkrlem2a  38088  mapdcnvordN  38239  hdmap14lem4a  38452  hgmapeq0  38485  hdmaplkr  38494  hdmapellkr  38495  frlmfielbas  38576  rmxycomplete  38910  gicabl  39095  ntrneiel  39794  ntrneik4w  39813  ntrneik4  39814  extoimad  39879  radcnvrat  40062  pm14.123b  40175  iotavalb  40179  infxrunb3  41129  climreeq  41325  clim2f  41348  clim2f2  41382  dfodd4  43192  oddprmne2  43248  nnsgrpnmnd  43453  ovmpordxf  43751  eenglngeehlnmlem2  44093