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  389  sbcom2  2165  19.21t  2204  19.23t  2208  sbco2  2514  sbco3  2516  sbal1  2532  sbal2  2533  csbiebt  3841  prsspwg  4736  ssprss  4737  reusv2lem5  5295  copsex2t  5375  copsex2gOLD  5377  ordtri2  6248  onmindif  6302  fnssresb  6499  fcnvres  6596  foelrni  6774  funimass5  6875  fmptco  6944  cbvfo  7099  isocnv  7139  isoini  7147  isoselem  7150  riota2df  7194  ovmpodxf  7359  caovcanrd  7411  onmindif2  7591  ordunisuc2  7623  dfom2  7646  ordge1n0  8225  ondif2  8229  oa00  8287  odi  8307  oeoe  8327  eceqoveq  8504  isfinite2  8929  unfilem1  8935  fodomfib  8950  inficl  9041  dffi3  9047  ordiso2  9131  ordtypelem9  9142  cantnfle  9286  cantnf  9308  wemapwe  9312  rankr1a  9452  bnd2  9509  iscard  9591  domtri2  9605  nnsdomel  9606  cardaleph  9703  dfac12lem2  9758  cfss  9879  axcc3  10052  fodomb  10140  iundom2g  10154  inar1  10389  ltpiord  10501  ordpinq  10557  suplem2pr  10667  enreceq  10680  subeq0  11104  negcon1  11130  subexsub  11250  subeqrev  11254  lesub  11311  ltsub13  11313  subge0  11345  mul0or  11472  mulcan1g  11485  div11  11518  divmuleq  11537  mdiv  11668  ltmuldiv2  11706  lemuldiv2  11713  nn1suc  11852  addltmul  12066  elnnnn0  12133  znn0sub  12224  prime  12258  zbtwnre  12542  xadddi2  12887  supxrbnd  12918  fz1n  13130  fzrev3  13178  fzo0n  13264  fzonlt0  13265  ico01fl0  13394  divfl0  13399  modsubdir  13513  om2uzlt2i  13524  hashf1lem1  14020  hashf1lem1OLD  14021  wrdlenge1n0  14105  pfxccat3a  14303  cnpart  14803  sqrt11  14826  sqrtsq2  14832  absdiflt  14881  absdifle  14882  sqreulem  14923  sqreu  14924  eqsqrtor  14930  clim2  15065  climshft2  15143  isercoll  15231  sumrb  15277  supcvg  15420  prodrblem2  15493  sinbnd  15741  cosbnd  15742  sqrt2irr  15810  dvdscmulr  15846  dvdsmulcr  15847  oddm1even  15904  bitsmod  15995  bitsinv1lem  16000  qredeq  16214  cncongr2  16225  isprm3  16240  prmrp  16269  crth  16331  pcdvdsb  16422  pceq0  16424  unbenlem  16461  ramcl  16582  pwselbasb  16993  pwsle  16997  imasleval  17046  xpsfrnel2  17069  acsfn  17162  ismon2  17239  isepi2  17246  epii  17248  fthsect  17432  fthmon  17434  isipodrs  18043  ipodrsfi  18045  gsumval2a  18157  imasmnd2  18210  grpid  18403  grpidrcan  18428  grpidlcan  18429  grplmulf1o  18437  imasgrp2  18478  ghmeqker  18649  ghmf1  18651  gacan  18699  odmulgeq  18948  pgpssslw  19003  efgsfo  19129  efgred  19138  abladdsub4  19199  subgdmdprd  19421  imasring  19637  lspsnss2  20042  0ring01eqbi  20311  znf1o  20516  znfld  20525  znunit  20528  znrrg  20530  iporthcom  20597  ip2eq  20615  obsne0  20687  lindfmm  20789  lindsmm  20790  lsslinds  20793  gsumbagdiaglemOLD  20897  gsumbagdiaglem  20900  eltg3  21859  eltop  21871  eltop2  21872  eltop3  21873  lmbrf  22157  cncnpi  22175  dfconn2  22316  1stcfb  22342  elptr  22470  xkoccn  22516  txcn  22523  hausdiag  22542  hmeoimaf1o  22667  isfbas  22726  ufileu  22816  alexsubALTlem4  22947  tsmsf1o  23042  ismet2  23231  imasdsf1olem  23271  imasf1oxmet  23273  imasf1omet  23274  xmseq0  23362  imasf1oxms  23387  metucn  23469  nrmmetd  23472  nmgt0  23528  nlmmul0or  23581  xrsxmet  23706  metdseq0  23751  elpi1i  23943  cphsqrtcl2  24083  tcphcph  24134  lmmbrf  24159  caucfil  24180  lmclim  24200  cmsss  24248  srabn  24257  ovolfioo  24364  ovolficc  24365  elovolmr  24373  ovolctb  24387  ovolicc2lem3  24416  mbfmulc2lem  24544  mbfimaopnlem  24552  itg2mulclem  24644  iblrelem  24688  ellimc2  24774  mdegle0  24975  fta1glem2  25064  dgreq0  25159  plydivlem4  25189  plydivex  25190  fta1  25201  quotcan  25202  logeftb  25472  quad2  25722  cubic2  25731  dquartlem1  25734  atandm4  25762  fsumharmonic  25894  wilthlem1  25950  basellem8  25970  mumullem2  26062  chpchtsum  26100  logfaclbnd  26103  dchrelbas4  26124  lgsne0  26216  lgsqrlem2  26228  lgsdchrval  26235  lgsquadlem1  26261  lgsquadlem2  26262  2sqlem7  26305  addsqrexnreu  26323  dchrisum0lem1  26397  trgcgrg  26606  tgcgr4  26622  tgcolg  26645  lmiinv  26883  iseqlg  26958  elntg2  27076  cusgruvtxb  27510  upgrewlkle2  27694  clwwlkn1  28124  eupth2lem3lem3  28313  eupth2lem3lem6  28316  frgr3vlem2  28357  grpoid  28601  nvmeq0  28739  nvgt0  28755  imsmetlem  28771  nmlnogt0  28878  ip2eqi  28937  hvaddcan2  29152  hvmulcan2  29154  hvaddsub4  29159  hi2eq  29186  pjhtheu  29475  lnopeqi  30089  riesz1  30146  jpi  30351  chcv2  30437  cvp  30456  atnemeq0  30458  brabgaf  30667  fmptcof2  30714  funcnvmpt  30724  nndiffz1  30827  nn0min  30854  xrge0addgt0  31019  lbslsp  31286  smatrcl  31460  lmlim  31611  carsggect  31997  eulerpartlems  32039  eulerpartlemgh  32057  ballotlemfc0  32171  ballotlemfcc  32172  sgnneg  32219  signsvfpn  32276  signsvfnn  32277  reprdifc  32319  bnj1280  32713  lfuhgr  32792  satffunlem1lem2  33078  elmrsubrn  33195  msubff1  33231  fz0n  33414  frxp2  33528  xpord2pred  33529  nogt01o  33636  slenlt  33692  imageval  33969  nn0prpwlem  34248  filnetlem4  34307  onsuct0  34367  onint1  34375  dissneqlem  35248  fvineqsneu  35319  wl-sbalnae  35454  wl-ax11-lem8  35480  wl-ax11-lem10  35482  sin2h  35504  tan2h  35506  matunitlindflem1  35510  matunitlindflem2  35511  matunitlindf  35512  poimirlem18  35532  poimirlem21  35535  poimirlem24  35538  heicant  35549  mblfinlem3  35553  ovoliunnfl  35556  voliunnfl  35558  volsupnfl  35559  mbfresfi  35560  mbfposadd  35561  itg2addnclem  35565  itg2addnclem2  35566  itg2addnc  35568  itg2gt0cn  35569  itgaddnclem2  35573  ftc1anclem5  35591  areacirclem1  35602  areacirclem4  35605  areacirc  35607  isdmn3  35969  eldmres2  36147  relbrcoss  36301  releldmqs  36507  lcvp  36791  lcv2  36793  lsatnem0  36796  atnem0  37069  cvlsupr2  37094  cvr2N  37162  athgt  37207  2llnmat  37275  pmap11  37513  pmapeq0  37517  2lnat  37535  paddclN  37593  pmapjat1  37604  ltrn2ateq  37931  dihcnvord  39025  dihcnv11  39026  dih0bN  39032  dih0sb  39036  dihlspsnat  39084  dihatexv2  39090  dihglblem6  39091  dochvalr  39108  dochn0nv  39126  djhcvat42  39166  dochsatshp  39202  dochshpsat  39205  dochkrsat2  39207  lcfl5a  39248  lcfl8a  39254  lclkrlem2a  39258  mapdcnvordN  39409  hdmap14lem4a  39622  hgmapeq0  39655  hdmaplkr  39664  hdmapellkr  39665  metakunt15  39861  frlmfielbas  39944  rmxycomplete  40442  gicabl  40627  ntrneiel  41368  ntrneik4w  41387  ntrneik4  41388  extoimad  41452  radcnvrat  41605  pm14.123b  41717  iotavalb  41721  infxrunb3  42637  climreeq  42829  clim2f  42852  clim2f2  42886  dfodd4  44784  oddprmne2  44840  nnsgrpnmnd  45045  ovmpordxf  45347  eenglngeehlnmlem2  45757  iscnrm3  45919