Theorem bitr3d 284

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3bitrrd  309  3bitr3d  312  3bitr3rd  313  biass  388  sbcom2  2205  19.21t  2240  19.23t  2244  sbco2  2541  sbco3  2543  sbal1  2558  sbal2  2559  clelab  2905  ceqsralt  3487  csbiebt  3881  prsspwg  4788  ssprss  4789  reusv2lem5  5373  copsex2t  5475  ordtri2  6396  onmindif  6455  fnssresb  6657  fcnvres  6755  foelcdmi  6942  funcnvmpt  6991  funimass5  7050  fmptco  7125  cbvfo  7287  isocnv  7328  isoini  7336  isoselem  7339  riota2df  7390  ovmpodxf  7560  caovcanrd  7613  onmindif2  7805  ordunisuc2  7839  dfom2  7863  frxp2  8139  xpord2pred  8140  xpord3pred  8147  ordge1n0  8478  ondif2  8486  oa00  8543  odi  8563  oeoe  8584  eceqoveq  8819  isfinite2  9257  unfilem1  9264  fodomfib  9287  inficl  9384  dffi3  9390  ordiso2  9476  ordtypelem9  9487  cantnfle  9639  cantnf  9661  wemapwe  9665  rankr1a  9807  bnd2  9878  iscard  9960  domtri2  9974  nnsdomel  9975  cardaleph  10072  dfac12lem2  10127  cfss  10248  axcc3  10421  fodomb  10509  iundom2g  10523  inar1  10759  ltpiord  10871  ordpinq  10927  suplem2pr  11037  enreceq  11050  subeq0  11483  negcon1  11509  subexsub  11631  subeqrev  11635  lesub  11692  ltsub13  11694  subge0  11726  mul0or  11853  mulcan1g  11866  divmuleq  11919  mdiv  12050  ltmuldiv2  12088  lemuldiv2  12095  nn1suc  12254  addltmul  12479  elnnnn0  12546  znn0sub  12640  prime  12676  zbtwnre  12969  xadddi2  13322  supxrbnd  13353  fz1n  13569  fzrev3  13617  fzo0n  13709  fzonlt0  13710  ico01fl0  13851  divfl0  13856  modaddid  13942  modsubdir  13975  om2uzlt2i  13986  hashf1lem1  14491  wrdlenge1n0  14586  pfxccat3a  14774  sgnneg  15136  cnpart  15290  sqrt11  15312  sqrtsq2  15318  absdiflt  15368  absdifle  15369  sqreulem  15410  sqreu  15411  eqsqrtor  15417  clim2  15554  climshft2  15632  isercoll  15718  sumrb  15763  supcvg  15909  prodrblem2  15984  sinbnd  16235  cosbnd  16236  sqrt2irr  16304  dvdscmulr  16341  dvdsmulcr  16342  oddm1even  16400  bitsmod  16493  bitsinv1lem  16498  qredeq  16714  cncongr2  16725  isprm3  16740  prmrp  16770  crth  16836  pcdvdsb  16928  pceq0  16930  unbenlem  16967  ramcl  17088  pwselbasb  17540  pwsle  17545  imasleval  17594  xpsfrnel2  17617  acsfn  17714  ismon2  17790  isepi2  17797  epii  17799  fthsect  17983  fthmon  17985  isipodrs  18592  ipodrsfi  18594  gsumval2a  18742  imasmnd2  18831  grpid  19041  grpidrcan  19069  grpidlcan  19070  grplmulf1o  19078  grpraddf1o  19079  imasgrp2  19120  eqg0subg  19266  ghmeqker  19312  gacan  19374  odmulgeq  19626  pgpssslw  19683  efgsfo  19808  efgred  19817  abladdsub4  19880  subgdmdprd  20105  imasrng  20254  imasring  20411  0ring01eqbi  20616  domneq0r  20807  lspsnss2  21105  znf1o  21680  znfld  21689  znunit  21692  znrrg  21694  iporthcom  21764  ip2eq  21782  obsne0  21854  lindfmm  21956  lindsmm  21957  lsslinds  21960  gsumbagdiaglem  22060  psdmul  22308  eltg3  23098  eltop  23110  eltop2  23111  eltop3  23112  lmbrf  23396  cncnpi  23414  dfconn2  23555  1stcfb  23581  elptr  23709  xkoccn  23755  txcn  23762  hausdiag  23781  hmeoimaf1o  23906  isfbas  23965  ufileu  24055  alexsubALTlem4  24186  tsmsf1o  24281  ismet2  24469  imasdsf1olem  24509  imasf1oxmet  24511  imasf1omet  24512  xmseq0  24600  imasf1oxms  24625  metucn  24707  nrmmetd  24710  nmgt0  24766  nlmmul0or  24819  xrsxmet  24946  metdseq0  24991  elpi1i  25184  cphsqrtcl2  25324  tcphcph  25375  lmmbrf  25400  caucfil  25421  lmclim  25441  cmsss  25489  srabn  25498  ovolfioo  25605  ovolficc  25606  elovolmr  25614  ovolctb  25628  ovolicc2lem3  25657  mbfmulc2lem  25785  mbfimaopnlem  25793  itg2mulclem  25884  iblrelem  25929  ellimc2  26015  mdegle0  26213  fta1glem2  26305  dgreq0  26401  plydivlem4  26436  plydivex  26437  fta1  26448  quotcan  26449  logeftb  26724  quad2  26980  cubic2  26989  dquartlem1  26992  atandm4  27020  fsumharmonic  27152  wilthlem1  27208  basellem8  27228  mumullem2  27320  fsumdvdsmul  27335  chpchtsum  27359  logfaclbnd  27362  dchrelbas4  27383  lgsne0  27475  lgsqrlem2  27487  lgsdchrval  27494  lgsquadlem1  27520  lgsquadlem2  27521  2sqlem7  27564  addsqrexnreu  27582  dchrisum0lem1  27656  nogt01o  27836  lenlts  27892  addscan1  28163  subseq0d  28274  mulscan2d  28348  mulscan1d  28349  muls0ord  28354  ltmuldivs2wd  28371  onnolt  28435  onlts  28436  om2noseqlt2  28469  zn0subs  28572  bdaypw2n0bndlem  28632  bdayfinbndlem1  28636  trgcgrg  28760  tgcgr4  28776  tgcolg  28799  plngrotlem2  29044  lmiinv  29075  iseqlg  29157  elntg2  29301  cusgruvtxb  29738  upgrewlkle2  29922  clwwlkn1  30358  eupth2lem3lem3  30547  eupth2lem3lem6  30550  frgr3vlem2  30591  grpoid  30838  nvmeq0  30976  nvgt0  30992  imsmetlem  31008  nmlnogt0  31115  ip2eqi  31174  hvaddcan2  31389  hvmulcan2  31391  hvaddsub4  31396  hi2eq  31423  pjhtheu  31712  lnopeqi  32326  riesz1  32383  jpi  32588  chcv2  32674  cvp  32693  atnemeq0  32695  brabgaf  32917  fmptcof2  32968  nndiffz1  33097  nn0min  33131  xrge0addgt0  33303  rlocisunit  33562  lbslsp  33656  ressply1mon1p  33824  fldextrspunlsplem  34029  smatrcl  34152  lmlim  34303  carsggect  34674  eulerpartlems  34716  eulerpartlemgh  34734  ballotlemfc0  34849  ballotlemfcc  34850  signsvfpn  34938  signsvfnn  34939  reprdifc  34980  bnj1280  35374  fineqvnttrclselem3  35490  lfuhgr  35564  satffunlem1lem2  35849  elmrsubrn  35966  msubff1  36002  fz0n  36177  imageval  36374  nn0prpwlem  36777  filnetlem4  36836  onsuct0  36896  onint1  36904  dissneqlem  37930  fvineqsneu  38001  wl-sbalnae  38161  sin2h  38205  tan2h  38207  matunitlindflem1  38211  matunitlindflem2  38212  matunitlindf  38213  poimirlem18  38233  poimirlem21  38236  poimirlem24  38239  heicant  38250  mblfinlem3  38254  ovoliunnfl  38257  voliunnfl  38259  volsupnfl  38260  mbfresfi  38261  mbfposadd  38262  itg2addnclem  38266  itg2addnclem2  38267  itg2addnc  38269  itg2gt0cn  38270  itgaddnclem2  38274  ftc1anclem5  38292  areacirclem1  38303  areacirclem4  38306  areacirc  38308  isdmn3  38669  eldmres2  38877  cnvref4  38945  relbrcoss  39131  releldmqs  39338  lcvp  39760  lcv2  39762  lsatnem0  39765  atnem0  40038  cvlsupr2  40063  cvr2N  40131  athgt  40176  2llnmat  40244  pmap11  40482  pmapeq0  40486  2lnat  40504  paddclN  40562  pmapjat1  40573  ltrn2ateq  40900  dihcnvord  41994  dihcnv11  41995  dih0bN  42001  dih0sb  42005  dihlspsnat  42053  dihatexv2  42059  dihglblem6  42060  dochvalr  42077  dochn0nv  42095  djhcvat42  42135  dochsatshp  42171  dochshpsat  42174  dochkrsat2  42176  lcfl5a  42217  lcfl8a  42223  lclkrlem2a  42227  mapdcnvordN  42378  hdmap14lem4a  42591  hgmapeq0  42624  hdmaplkr  42633  hdmapellkr  42634  cxp111d  43049  sn-remul0ord  43115  sn-ltmulgt11d  43194  frlmfielbas  43220  eu6w  43356  rmxycomplete  43592  gicabl  43774  minregex2  44209  ntrneiel  44755  ntrneik4w  44774  ntrneik4  44775  extoimad  44838  radcnvrat  44972  pm14.123b  45084  iotavalb  45088  infxrunb3  46086  climreeq  46277  clim2f  46298  clim2f2  46332  dfodd4  48369  oddprmne2  48425  nnsgrpnmnd  48888  isidom3  49055  ovmpordxf  49064  eenglngeehlnmlem2  49463  iscnrm3  49675  uptrlem1  49933