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  3482  csbiebt  3891  prsspwg  4787  ssprss  4788  reusv2lem5  5357  copsex2t  5452  ordtri2  6367  onmindif  6426  fnssresb  6640  fcnvres  6737  foelcdmi  6922  funimass5  7027  fmptco  7101  cbvfo  7264  isocnv  7305  isoini  7313  isoselem  7316  riota2df  7367  ovmpodxf  7539  caovcanrd  7592  onmindif2  7783  ordunisuc2  7820  dfom2  7844  frxp2  8123  xpord2pred  8124  xpord3pred  8131  ordge1n0  8458  ondif2  8466  oa00  8523  odi  8543  oeoe  8563  eceqoveq  8795  isfinite2  9245  unfilem1  9254  fodomfib  9280  fodomfibOLD  9282  inficl  9376  dffi3  9382  ordiso2  9468  ordtypelem9  9479  cantnfle  9624  cantnf  9646  wemapwe  9650  rankr1a  9789  bnd2  9846  iscard  9928  domtri2  9942  nnsdomel  9943  cardaleph  10042  dfac12lem2  10098  cfss  10218  axcc3  10391  fodomb  10479  iundom2g  10493  inar1  10728  ltpiord  10840  ordpinq  10896  suplem2pr  11006  enreceq  11019  subeq0  11448  negcon1  11474  subexsub  11596  subeqrev  11600  lesub  11657  ltsub13  11659  subge0  11691  mul0or  11818  mulcan1g  11831  div11OLD  11866  divmuleq  11887  mdiv  12018  ltmuldiv2  12057  lemuldiv2  12064  nn1suc  12208  addltmul  12418  elnnnn0  12485  znn0sub  12580  prime  12615  zbtwnre  12905  xadddi2  13257  supxrbnd  13288  fz1n  13503  fzrev3  13551  fzo0n  13642  fzonlt0  13643  ico01fl0  13781  divfl0  13786  modaddid  13872  modsubdir  13905  om2uzlt2i  13916  hashf1lem1  14420  wrdlenge1n0  14515  pfxccat3a  14703  cnpart  15206  sqrt11  15228  sqrtsq2  15234  absdiflt  15284  absdifle  15285  sqreulem  15326  sqreu  15327  eqsqrtor  15333  clim2  15470  climshft2  15548  isercoll  15634  sumrb  15679  supcvg  15822  prodrblem2  15897  sinbnd  16148  cosbnd  16149  sqrt2irr  16217  dvdscmulr  16254  dvdsmulcr  16255  oddm1even  16313  bitsmod  16406  bitsinv1lem  16411  qredeq  16627  cncongr2  16638  isprm3  16653  prmrp  16682  crth  16748  pcdvdsb  16840  pceq0  16842  unbenlem  16879  ramcl  17000  pwselbasb  17451  pwsle  17455  imasleval  17504  xpsfrnel2  17527  acsfn  17620  ismon2  17696  isepi2  17703  epii  17705  fthsect  17889  fthmon  17891  isipodrs  18496  ipodrsfi  18498  gsumval2a  18612  imasmnd2  18701  grpid  18907  grpidrcan  18935  grpidlcan  18936  grplmulf1o  18945  grpraddf1o  18946  imasgrp2  18987  eqg0subg  19128  ghmeqker  19175  gacan  19237  odmulgeq  19487  pgpssslw  19544  efgsfo  19669  efgred  19678  abladdsub4  19741  subgdmdprd  19966  imasrng  20086  imasring  20239  0ring01eqbi  20441  domneq0r  20633  lspsnss2  20911  znf1o  21461  znfld  21470  znunit  21473  znrrg  21475  iporthcom  21544  ip2eq  21562  obsne0  21634  lindfmm  21736  lindsmm  21737  lsslinds  21740  gsumbagdiaglem  21839  psdmul  22053  eltg3  22849  eltop  22861  eltop2  22862  eltop3  22863  lmbrf  23147  cncnpi  23165  dfconn2  23306  1stcfb  23332  elptr  23460  xkoccn  23506  txcn  23513  hausdiag  23532  hmeoimaf1o  23657  isfbas  23716  ufileu  23806  alexsubALTlem4  23937  tsmsf1o  24032  ismet2  24221  imasdsf1olem  24261  imasf1oxmet  24263  imasf1omet  24264  xmseq0  24352  imasf1oxms  24377  metucn  24459  nrmmetd  24462  nmgt0  24518  nlmmul0or  24571  xrsxmet  24698  metdseq0  24743  elpi1i  24946  cphsqrtcl2  25086  tcphcph  25137  lmmbrf  25162  caucfil  25183  lmclim  25203  cmsss  25251  srabn  25260  ovolfioo  25368  ovolficc  25369  elovolmr  25377  ovolctb  25391  ovolicc2lem3  25420  mbfmulc2lem  25548  mbfimaopnlem  25556  itg2mulclem  25647  iblrelem  25692  ellimc2  25778  mdegle0  25982  fta1glem2  26074  dgreq0  26171  plydivlem4  26204  plydivex  26205  fta1  26216  quotcan  26217  logeftb  26492  quad2  26749  cubic2  26758  dquartlem1  26761  atandm4  26789  fsumharmonic  26922  wilthlem1  26978  basellem8  26998  mumullem2  27090  fsumdvdsmul  27105  chpchtsum  27130  logfaclbnd  27133  dchrelbas4  27154  lgsne0  27246  lgsqrlem2  27258  lgsdchrval  27265  lgsquadlem1  27291  lgsquadlem2  27292  2sqlem7  27335  addsqrexnreu  27353  dchrisum0lem1  27427  nogt01o  27608  slenlt  27664  addscan1  27901  subseq0d  28008  mulscan2d  28082  mulscan1d  28083  muls0ord  28088  sltmuldiv2wd  28105  onnolt  28167  onslt  28168  om2noseqlt2  28194  zn0subs  28291  trgcgrg  28442  tgcgr4  28458  tgcolg  28481  lmiinv  28719  iseqlg  28794  elntg2  28912  cusgruvtxb  29349  upgrewlkle2  29534  clwwlkn1  29970  eupth2lem3lem3  30159  eupth2lem3lem6  30162  frgr3vlem2  30203  grpoid  30449  nvmeq0  30587  nvgt0  30603  imsmetlem  30619  nmlnogt0  30726  ip2eqi  30785  hvaddcan2  31000  hvmulcan2  31002  hvaddsub4  31007  hi2eq  31034  pjhtheu  31323  lnopeqi  31937  riesz1  31994  jpi  32199  chcv2  32285  cvp  32304  atnemeq0  32306  brabgaf  32536  fmptcof2  32581  funcnvmpt  32591  nndiffz1  32709  nn0min  32745  sgnneg  32758  xrge0addgt0  32958  lbslsp  33348  ressply1mon1p  33537  fldextrspunlsplem  33668  smatrcl  33786  lmlim  33937  carsggect  34309  eulerpartlems  34351  eulerpartlemgh  34369  ballotlemfc0  34484  ballotlemfcc  34485  signsvfpn  34576  signsvfnn  34577  reprdifc  34618  bnj1280  35010  lfuhgr  35105  satffunlem1lem2  35390  elmrsubrn  35507  msubff1  35543  fz0n  35718  imageval  35918  nn0prpwlem  36310  filnetlem4  36369  onsuct0  36429  onint1  36437  dissneqlem  37328  fvineqsneu  37399  wl-sbalnae  37550  wl-ax11-lem8  37580  wl-ax11-lem10  37582  sin2h  37604  tan2h  37606  matunitlindflem1  37610  matunitlindflem2  37611  matunitlindf  37612  poimirlem18  37632  poimirlem21  37635  poimirlem24  37638  heicant  37649  mblfinlem3  37653  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  mbfresfi  37660  mbfposadd  37661  itg2addnclem  37665  itg2addnclem2  37666  itg2addnc  37668  itg2gt0cn  37669  itgaddnclem2  37673  ftc1anclem5  37691  areacirclem1  37702  areacirclem4  37705  areacirc  37707  isdmn3  38068  eldmres2  38264  cnvref4  38332  relbrcoss  38437  releldmqs  38650  lcvp  39033  lcv2  39035  lsatnem0  39038  atnem0  39311  cvlsupr2  39336  cvr2N  39405  athgt  39450  2llnmat  39518  pmap11  39756  pmapeq0  39760  2lnat  39778  paddclN  39836  pmapjat1  39847  ltrn2ateq  40174  dihcnvord  41268  dihcnv11  41269  dih0bN  41275  dih0sb  41279  dihlspsnat  41327  dihatexv2  41333  dihglblem6  41334  dochvalr  41351  dochn0nv  41369  djhcvat42  41409  dochsatshp  41445  dochshpsat  41448  dochkrsat2  41450  lcfl5a  41491  lcfl8a  41497  lclkrlem2a  41501  mapdcnvordN  41652  hdmap14lem4a  41865  hgmapeq0  41898  hdmaplkr  41907  hdmapellkr  41908  cxp111d  42330  sn-remul0ord  42396  sn-ltmulgt11d  42462  frlmfielbas  42488  eu6w  42664  rmxycomplete  42906  gicabl  43088  minregex2  43524  ntrneiel  44070  ntrneik4w  44089  ntrneik4  44090  extoimad  44153  radcnvrat  44303  pm14.123b  44415  iotavalb  44419  infxrunb3  45420  climreeq  45611  clim2f  45634  clim2f2  45668  dfodd4  47660  oddprmne2  47716  nnsgrpnmnd  48166  ovmpordxf  48327  eenglngeehlnmlem2  48727  iscnrm3  48940  uptrlem1  49199