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  2174  19.21t  2207  19.23t  2211  sbco2  2509  sbco3  2511  sbal1  2526  sbal2  2527  clelab  2873  ceqsralt  3471  csbiebt  3880  prsspwg  4774  ssprss  4775  reusv2lem5  5341  copsex2t  5435  ordtri2  6342  onmindif  6401  fnssresb  6604  fcnvres  6701  foelcdmi  6884  funimass5  6989  fmptco  7063  cbvfo  7226  isocnv  7267  isoini  7275  isoselem  7278  riota2df  7329  ovmpodxf  7499  caovcanrd  7552  onmindif2  7743  ordunisuc2  7777  dfom2  7801  frxp2  8077  xpord2pred  8078  xpord3pred  8085  ordge1n0  8412  ondif2  8420  oa00  8477  odi  8497  oeoe  8517  eceqoveq  8749  isfinite2  9187  unfilem1  9194  fodomfib  9219  fodomfibOLD  9221  inficl  9315  dffi3  9321  ordiso2  9407  ordtypelem9  9418  cantnfle  9567  cantnf  9589  wemapwe  9593  rankr1a  9732  bnd2  9789  iscard  9871  domtri2  9885  nnsdomel  9886  cardaleph  9983  dfac12lem2  10039  cfss  10159  axcc3  10332  fodomb  10420  iundom2g  10434  inar1  10669  ltpiord  10781  ordpinq  10837  suplem2pr  10947  enreceq  10960  subeq0  11390  negcon1  11416  subexsub  11538  subeqrev  11542  lesub  11599  ltsub13  11601  subge0  11633  mul0or  11760  mulcan1g  11773  div11OLD  11808  divmuleq  11829  mdiv  11960  ltmuldiv2  11999  lemuldiv2  12006  nn1suc  12150  addltmul  12360  elnnnn0  12427  znn0sub  12522  prime  12557  zbtwnre  12847  xadddi2  13199  supxrbnd  13230  fz1n  13445  fzrev3  13493  fzo0n  13584  fzonlt0  13585  ico01fl0  13723  divfl0  13728  modaddid  13814  modsubdir  13847  om2uzlt2i  13858  hashf1lem1  14362  wrdlenge1n0  14457  pfxccat3a  14644  cnpart  15147  sqrt11  15169  sqrtsq2  15175  absdiflt  15225  absdifle  15226  sqreulem  15267  sqreu  15268  eqsqrtor  15274  clim2  15411  climshft2  15489  isercoll  15575  sumrb  15620  supcvg  15763  prodrblem2  15838  sinbnd  16089  cosbnd  16090  sqrt2irr  16158  dvdscmulr  16195  dvdsmulcr  16196  oddm1even  16254  bitsmod  16347  bitsinv1lem  16352  qredeq  16568  cncongr2  16579  isprm3  16594  prmrp  16623  crth  16689  pcdvdsb  16781  pceq0  16783  unbenlem  16820  ramcl  16941  pwselbasb  17392  pwsle  17396  imasleval  17445  xpsfrnel2  17468  acsfn  17565  ismon2  17641  isepi2  17648  epii  17650  fthsect  17834  fthmon  17836  isipodrs  18443  ipodrsfi  18445  gsumval2a  18559  imasmnd2  18648  grpid  18854  grpidrcan  18882  grpidlcan  18883  grplmulf1o  18892  grpraddf1o  18893  imasgrp2  18934  eqg0subg  19075  ghmeqker  19122  gacan  19184  odmulgeq  19436  pgpssslw  19493  efgsfo  19618  efgred  19627  abladdsub4  19690  subgdmdprd  19915  imasrng  20062  imasring  20215  0ring01eqbi  20417  domneq0r  20609  lspsnss2  20908  znf1o  21458  znfld  21467  znunit  21470  znrrg  21472  iporthcom  21542  ip2eq  21560  obsne0  21632  lindfmm  21734  lindsmm  21735  lsslinds  21738  gsumbagdiaglem  21837  psdmul  22051  eltg3  22847  eltop  22859  eltop2  22860  eltop3  22861  lmbrf  23145  cncnpi  23163  dfconn2  23304  1stcfb  23330  elptr  23458  xkoccn  23504  txcn  23511  hausdiag  23530  hmeoimaf1o  23655  isfbas  23714  ufileu  23804  alexsubALTlem4  23935  tsmsf1o  24030  ismet2  24219  imasdsf1olem  24259  imasf1oxmet  24261  imasf1omet  24262  xmseq0  24350  imasf1oxms  24375  metucn  24457  nrmmetd  24460  nmgt0  24516  nlmmul0or  24569  xrsxmet  24696  metdseq0  24741  elpi1i  24944  cphsqrtcl2  25084  tcphcph  25135  lmmbrf  25160  caucfil  25181  lmclim  25201  cmsss  25249  srabn  25258  ovolfioo  25366  ovolficc  25367  elovolmr  25375  ovolctb  25389  ovolicc2lem3  25418  mbfmulc2lem  25546  mbfimaopnlem  25554  itg2mulclem  25645  iblrelem  25690  ellimc2  25776  mdegle0  25980  fta1glem2  26072  dgreq0  26169  plydivlem4  26202  plydivex  26203  fta1  26214  quotcan  26215  logeftb  26490  quad2  26747  cubic2  26756  dquartlem1  26759  atandm4  26787  fsumharmonic  26920  wilthlem1  26976  basellem8  26996  mumullem2  27088  fsumdvdsmul  27103  chpchtsum  27128  logfaclbnd  27131  dchrelbas4  27152  lgsne0  27244  lgsqrlem2  27256  lgsdchrval  27263  lgsquadlem1  27289  lgsquadlem2  27290  2sqlem7  27333  addsqrexnreu  27351  dchrisum0lem1  27425  nogt01o  27606  slenlt  27662  addscan1  27906  subseq0d  28013  mulscan2d  28087  mulscan1d  28088  muls0ord  28093  sltmuldiv2wd  28110  onnolt  28172  onslt  28173  om2noseqlt2  28199  zn0subs  28296  trgcgrg  28460  tgcgr4  28476  tgcolg  28499  lmiinv  28737  iseqlg  28812  elntg2  28930  cusgruvtxb  29367  upgrewlkle2  29552  clwwlkn1  29985  eupth2lem3lem3  30174  eupth2lem3lem6  30177  frgr3vlem2  30218  grpoid  30464  nvmeq0  30602  nvgt0  30618  imsmetlem  30634  nmlnogt0  30741  ip2eqi  30800  hvaddcan2  31015  hvmulcan2  31017  hvaddsub4  31022  hi2eq  31049  pjhtheu  31338  lnopeqi  31952  riesz1  32009  jpi  32214  chcv2  32300  cvp  32319  atnemeq0  32321  brabgaf  32553  fmptcof2  32601  funcnvmpt  32611  nndiffz1  32730  nn0min  32766  sgnneg  32779  xrge0addgt0  32972  lbslsp  33315  ressply1mon1p  33504  fldextrspunlsplem  33646  smatrcl  33769  lmlim  33920  carsggect  34292  eulerpartlems  34334  eulerpartlemgh  34352  ballotlemfc0  34467  ballotlemfcc  34468  signsvfpn  34559  signsvfnn  34560  reprdifc  34601  bnj1280  34993  fineqvnttrclselem3  35082  lfuhgr  35101  satffunlem1lem2  35386  elmrsubrn  35503  msubff1  35539  fz0n  35714  imageval  35914  nn0prpwlem  36306  filnetlem4  36365  onsuct0  36425  onint1  36433  dissneqlem  37324  fvineqsneu  37395  wl-sbalnae  37546  wl-ax11-lem8  37576  wl-ax11-lem10  37578  sin2h  37600  tan2h  37602  matunitlindflem1  37606  matunitlindflem2  37607  matunitlindf  37608  poimirlem18  37628  poimirlem21  37631  poimirlem24  37634  heicant  37645  mblfinlem3  37649  ovoliunnfl  37652  voliunnfl  37654  volsupnfl  37655  mbfresfi  37656  mbfposadd  37657  itg2addnclem  37661  itg2addnclem2  37662  itg2addnc  37664  itg2gt0cn  37665  itgaddnclem2  37669  ftc1anclem5  37687  areacirclem1  37698  areacirclem4  37701  areacirc  37703  isdmn3  38064  eldmres2  38260  cnvref4  38328  relbrcoss  38433  releldmqs  38646  lcvp  39029  lcv2  39031  lsatnem0  39034  atnem0  39307  cvlsupr2  39332  cvr2N  39400  athgt  39445  2llnmat  39513  pmap11  39751  pmapeq0  39755  2lnat  39773  paddclN  39831  pmapjat1  39842  ltrn2ateq  40169  dihcnvord  41263  dihcnv11  41264  dih0bN  41270  dih0sb  41274  dihlspsnat  41322  dihatexv2  41328  dihglblem6  41329  dochvalr  41346  dochn0nv  41364  djhcvat42  41404  dochsatshp  41440  dochshpsat  41443  dochkrsat2  41445  lcfl5a  41486  lcfl8a  41492  lclkrlem2a  41496  mapdcnvordN  41647  hdmap14lem4a  41860  hgmapeq0  41893  hdmaplkr  41902  hdmapellkr  41903  cxp111d  42325  sn-remul0ord  42391  sn-ltmulgt11d  42457  frlmfielbas  42483  eu6w  42659  rmxycomplete  42900  gicabl  43082  minregex2  43518  ntrneiel  44064  ntrneik4w  44083  ntrneik4  44084  extoimad  44147  radcnvrat  44297  pm14.123b  44409  iotavalb  44413  infxrunb3  45413  climreeq  45604  clim2f  45627  clim2f2  45661  dfodd4  47653  oddprmne2  47709  nnsgrpnmnd  48172  ovmpordxf  48333  eenglngeehlnmlem2  48733  iscnrm3  48946  uptrlem1  49205