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  2179  19.21t  2214  19.23t  2218  sbco2  2516  sbco3  2518  sbal1  2533  sbal2  2534  clelab  2881  ceqsralt  3476  csbiebt  3879  prsspwg  4780  ssprss  4781  reusv2lem5  5348  copsex2t  5441  ordtri2  6353  onmindif  6412  fnssresb  6615  fcnvres  6712  foelcdmi  6896  funcnvmpt  6944  funimass5  7002  fmptco  7076  cbvfo  7237  isocnv  7278  isoini  7286  isoselem  7289  riota2df  7340  ovmpodxf  7510  caovcanrd  7563  onmindif2  7754  ordunisuc2  7788  dfom2  7812  frxp2  8088  xpord2pred  8089  xpord3pred  8096  ordge1n0  8423  ondif2  8431  oa00  8488  odi  8508  oeoe  8529  eceqoveq  8763  isfinite2  9202  unfilem1  9209  fodomfib  9233  fodomfibOLD  9235  inficl  9332  dffi3  9338  ordiso2  9424  ordtypelem9  9435  cantnfle  9584  cantnf  9606  wemapwe  9610  rankr1a  9752  bnd2  9809  iscard  9891  domtri2  9905  nnsdomel  9906  cardaleph  10003  dfac12lem2  10059  cfss  10179  axcc3  10352  fodomb  10440  iundom2g  10454  inar1  10690  ltpiord  10802  ordpinq  10858  suplem2pr  10968  enreceq  10981  subeq0  11411  negcon1  11437  subexsub  11559  subeqrev  11563  lesub  11620  ltsub13  11622  subge0  11654  mul0or  11781  mulcan1g  11794  div11OLD  11829  divmuleq  11850  mdiv  11981  ltmuldiv2  12020  lemuldiv2  12027  nn1suc  12171  addltmul  12381  elnnnn0  12448  znn0sub  12542  prime  12577  zbtwnre  12863  xadddi2  13216  supxrbnd  13247  fz1n  13462  fzrev3  13510  fzo0n  13601  fzonlt0  13602  ico01fl0  13743  divfl0  13748  modaddid  13834  modsubdir  13867  om2uzlt2i  13878  hashf1lem1  14382  wrdlenge1n0  14477  pfxccat3a  14665  cnpart  15167  sqrt11  15189  sqrtsq2  15195  absdiflt  15245  absdifle  15246  sqreulem  15287  sqreu  15288  eqsqrtor  15294  clim2  15431  climshft2  15509  isercoll  15595  sumrb  15640  supcvg  15783  prodrblem2  15858  sinbnd  16109  cosbnd  16110  sqrt2irr  16178  dvdscmulr  16215  dvdsmulcr  16216  oddm1even  16274  bitsmod  16367  bitsinv1lem  16372  qredeq  16588  cncongr2  16599  isprm3  16614  prmrp  16643  crth  16709  pcdvdsb  16801  pceq0  16803  unbenlem  16840  ramcl  16961  pwselbasb  17412  pwsle  17417  imasleval  17466  xpsfrnel2  17489  acsfn  17586  ismon2  17662  isepi2  17669  epii  17671  fthsect  17855  fthmon  17857  isipodrs  18464  ipodrsfi  18466  gsumval2a  18614  imasmnd2  18703  grpid  18909  grpidrcan  18937  grpidlcan  18938  grplmulf1o  18947  grpraddf1o  18948  imasgrp2  18989  eqg0subg  19129  ghmeqker  19176  gacan  19238  odmulgeq  19490  pgpssslw  19547  efgsfo  19672  efgred  19681  abladdsub4  19744  subgdmdprd  19969  imasrng  20116  imasring  20270  0ring01eqbi  20469  domneq0r  20661  lspsnss2  20960  znf1o  21510  znfld  21519  znunit  21522  znrrg  21524  iporthcom  21594  ip2eq  21612  obsne0  21684  lindfmm  21786  lindsmm  21787  lsslinds  21790  gsumbagdiaglem  21890  psdmul  22113  eltg3  22910  eltop  22922  eltop2  22923  eltop3  22924  lmbrf  23208  cncnpi  23226  dfconn2  23367  1stcfb  23393  elptr  23521  xkoccn  23567  txcn  23574  hausdiag  23593  hmeoimaf1o  23718  isfbas  23777  ufileu  23867  alexsubALTlem4  23998  tsmsf1o  24093  ismet2  24281  imasdsf1olem  24321  imasf1oxmet  24323  imasf1omet  24324  xmseq0  24412  imasf1oxms  24437  metucn  24519  nrmmetd  24522  nmgt0  24578  nlmmul0or  24631  xrsxmet  24758  metdseq0  24803  elpi1i  25006  cphsqrtcl2  25146  tcphcph  25197  lmmbrf  25222  caucfil  25243  lmclim  25263  cmsss  25311  srabn  25320  ovolfioo  25428  ovolficc  25429  elovolmr  25437  ovolctb  25451  ovolicc2lem3  25480  mbfmulc2lem  25608  mbfimaopnlem  25616  itg2mulclem  25707  iblrelem  25752  ellimc2  25838  mdegle0  26042  fta1glem2  26134  dgreq0  26231  plydivlem4  26264  plydivex  26265  fta1  26276  quotcan  26277  logeftb  26552  quad2  26809  cubic2  26818  dquartlem1  26821  atandm4  26849  fsumharmonic  26982  wilthlem1  27038  basellem8  27058  mumullem2  27150  fsumdvdsmul  27165  chpchtsum  27190  logfaclbnd  27193  dchrelbas4  27214  lgsne0  27306  lgsqrlem2  27318  lgsdchrval  27325  lgsquadlem1  27351  lgsquadlem2  27352  2sqlem7  27395  addsqrexnreu  27413  dchrisum0lem1  27487  nogt01o  27668  slenlt  27724  addscan1  27976  subseq0d  28087  mulscan2d  28161  mulscan1d  28162  muls0ord  28167  sltmuldiv2wd  28184  onnolt  28247  onslt  28248  om2noseqlt2  28281  zn0subs  28382  bdaypw2n0sbndlem  28442  trgcgrg  28570  tgcgr4  28586  tgcolg  28609  lmiinv  28847  iseqlg  28922  elntg2  29041  cusgruvtxb  29478  upgrewlkle2  29663  clwwlkn1  30099  eupth2lem3lem3  30288  eupth2lem3lem6  30291  frgr3vlem2  30332  grpoid  30578  nvmeq0  30716  nvgt0  30732  imsmetlem  30748  nmlnogt0  30855  ip2eqi  30914  hvaddcan2  31129  hvmulcan2  31131  hvaddsub4  31136  hi2eq  31163  pjhtheu  31452  lnopeqi  32066  riesz1  32123  jpi  32328  chcv2  32414  cvp  32433  atnemeq0  32435  brabgaf  32666  fmptcof2  32717  nndiffz1  32847  nn0min  32882  sgnneg  32895  xrge0addgt0  33080  lbslsp  33439  ressply1mon1p  33630  fldextrspunlsplem  33811  smatrcl  33934  lmlim  34085  carsggect  34456  eulerpartlems  34498  eulerpartlemgh  34516  ballotlemfc0  34631  ballotlemfcc  34632  signsvfpn  34723  signsvfnn  34724  reprdifc  34765  bnj1280  35157  fineqvnttrclselem3  35260  lfuhgr  35293  satffunlem1lem2  35578  elmrsubrn  35695  msubff1  35731  fz0n  35906  imageval  36103  nn0prpwlem  36497  filnetlem4  36556  onsuct0  36616  onint1  36624  dissneqlem  37516  fvineqsneu  37587  wl-sbalnae  37738  sin2h  37782  tan2h  37784  matunitlindflem1  37788  matunitlindflem2  37789  matunitlindf  37790  poimirlem18  37810  poimirlem21  37813  poimirlem24  37816  heicant  37827  mblfinlem3  37831  ovoliunnfl  37834  voliunnfl  37836  volsupnfl  37837  mbfresfi  37838  mbfposadd  37839  itg2addnclem  37843  itg2addnclem2  37844  itg2addnc  37846  itg2gt0cn  37847  itgaddnclem2  37851  ftc1anclem5  37869  areacirclem1  37880  areacirclem4  37883  areacirc  37885  isdmn3  38246  eldmres2  38454  cnvref4  38522  relbrcoss  38708  releldmqs  38915  lcvp  39337  lcv2  39339  lsatnem0  39342  atnem0  39615  cvlsupr2  39640  cvr2N  39708  athgt  39753  2llnmat  39821  pmap11  40059  pmapeq0  40063  2lnat  40081  paddclN  40139  pmapjat1  40150  ltrn2ateq  40477  dihcnvord  41571  dihcnv11  41572  dih0bN  41578  dih0sb  41582  dihlspsnat  41630  dihatexv2  41636  dihglblem6  41637  dochvalr  41654  dochn0nv  41672  djhcvat42  41712  dochsatshp  41748  dochshpsat  41751  dochkrsat2  41753  lcfl5a  41794  lcfl8a  41800  lclkrlem2a  41804  mapdcnvordN  41955  hdmap14lem4a  42168  hgmapeq0  42201  hdmaplkr  42210  hdmapellkr  42211  cxp111d  42633  sn-remul0ord  42699  sn-ltmulgt11d  42765  frlmfielbas  42791  eu6w  42955  rmxycomplete  43195  gicabl  43377  minregex2  43812  ntrneiel  44358  ntrneik4w  44377  ntrneik4  44378  extoimad  44441  radcnvrat  44591  pm14.123b  44703  iotavalb  44707  infxrunb3  45704  climreeq  45895  clim2f  45916  clim2f2  45950  dfodd4  47941  oddprmne2  47997  nnsgrpnmnd  48460  ovmpordxf  48621  eenglngeehlnmlem2  49020  iscnrm3  49233  uptrlem1  49491