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  2510  sbco3  2512  sbal1  2527  sbal2  2528  clelab  2874  ceqsralt  3485  csbiebt  3894  prsspwg  4790  ssprss  4791  reusv2lem5  5360  copsex2t  5455  ordtri2  6370  onmindif  6429  fnssresb  6643  fcnvres  6740  foelcdmi  6925  funimass5  7030  fmptco  7104  cbvfo  7267  isocnv  7308  isoini  7316  isoselem  7319  riota2df  7370  ovmpodxf  7542  caovcanrd  7595  onmindif2  7786  ordunisuc2  7823  dfom2  7847  frxp2  8126  xpord2pred  8127  xpord3pred  8134  ordge1n0  8461  ondif2  8469  oa00  8526  odi  8546  oeoe  8566  eceqoveq  8798  isfinite2  9252  unfilem1  9261  fodomfib  9287  fodomfibOLD  9289  inficl  9383  dffi3  9389  ordiso2  9475  ordtypelem9  9486  cantnfle  9631  cantnf  9653  wemapwe  9657  rankr1a  9796  bnd2  9853  iscard  9935  domtri2  9949  nnsdomel  9950  cardaleph  10049  dfac12lem2  10105  cfss  10225  axcc3  10398  fodomb  10486  iundom2g  10500  inar1  10735  ltpiord  10847  ordpinq  10903  suplem2pr  11013  enreceq  11026  subeq0  11455  negcon1  11481  subexsub  11603  subeqrev  11607  lesub  11664  ltsub13  11666  subge0  11698  mul0or  11825  mulcan1g  11838  div11OLD  11873  divmuleq  11894  mdiv  12025  ltmuldiv2  12064  lemuldiv2  12071  nn1suc  12215  addltmul  12425  elnnnn0  12492  znn0sub  12587  prime  12622  zbtwnre  12912  xadddi2  13264  supxrbnd  13295  fz1n  13510  fzrev3  13558  fzo0n  13649  fzonlt0  13650  ico01fl0  13788  divfl0  13793  modaddid  13879  modsubdir  13912  om2uzlt2i  13923  hashf1lem1  14427  wrdlenge1n0  14522  pfxccat3a  14710  cnpart  15213  sqrt11  15235  sqrtsq2  15241  absdiflt  15291  absdifle  15292  sqreulem  15333  sqreu  15334  eqsqrtor  15340  clim2  15477  climshft2  15555  isercoll  15641  sumrb  15686  supcvg  15829  prodrblem2  15904  sinbnd  16155  cosbnd  16156  sqrt2irr  16224  dvdscmulr  16261  dvdsmulcr  16262  oddm1even  16320  bitsmod  16413  bitsinv1lem  16418  qredeq  16634  cncongr2  16645  isprm3  16660  prmrp  16689  crth  16755  pcdvdsb  16847  pceq0  16849  unbenlem  16886  ramcl  17007  pwselbasb  17458  pwsle  17462  imasleval  17511  xpsfrnel2  17534  acsfn  17627  ismon2  17703  isepi2  17710  epii  17712  fthsect  17896  fthmon  17898  isipodrs  18503  ipodrsfi  18505  gsumval2a  18619  imasmnd2  18708  grpid  18914  grpidrcan  18942  grpidlcan  18943  grplmulf1o  18952  grpraddf1o  18953  imasgrp2  18994  eqg0subg  19135  ghmeqker  19182  gacan  19244  odmulgeq  19494  pgpssslw  19551  efgsfo  19676  efgred  19685  abladdsub4  19748  subgdmdprd  19973  imasrng  20093  imasring  20246  0ring01eqbi  20448  domneq0r  20640  lspsnss2  20918  znf1o  21468  znfld  21477  znunit  21480  znrrg  21482  iporthcom  21551  ip2eq  21569  obsne0  21641  lindfmm  21743  lindsmm  21744  lsslinds  21747  gsumbagdiaglem  21846  psdmul  22060  eltg3  22856  eltop  22868  eltop2  22869  eltop3  22870  lmbrf  23154  cncnpi  23172  dfconn2  23313  1stcfb  23339  elptr  23467  xkoccn  23513  txcn  23520  hausdiag  23539  hmeoimaf1o  23664  isfbas  23723  ufileu  23813  alexsubALTlem4  23944  tsmsf1o  24039  ismet2  24228  imasdsf1olem  24268  imasf1oxmet  24270  imasf1omet  24271  xmseq0  24359  imasf1oxms  24384  metucn  24466  nrmmetd  24469  nmgt0  24525  nlmmul0or  24578  xrsxmet  24705  metdseq0  24750  elpi1i  24953  cphsqrtcl2  25093  tcphcph  25144  lmmbrf  25169  caucfil  25190  lmclim  25210  cmsss  25258  srabn  25267  ovolfioo  25375  ovolficc  25376  elovolmr  25384  ovolctb  25398  ovolicc2lem3  25427  mbfmulc2lem  25555  mbfimaopnlem  25563  itg2mulclem  25654  iblrelem  25699  ellimc2  25785  mdegle0  25989  fta1glem2  26081  dgreq0  26178  plydivlem4  26211  plydivex  26212  fta1  26223  quotcan  26224  logeftb  26499  quad2  26756  cubic2  26765  dquartlem1  26768  atandm4  26796  fsumharmonic  26929  wilthlem1  26985  basellem8  27005  mumullem2  27097  fsumdvdsmul  27112  chpchtsum  27137  logfaclbnd  27140  dchrelbas4  27161  lgsne0  27253  lgsqrlem2  27265  lgsdchrval  27272  lgsquadlem1  27298  lgsquadlem2  27299  2sqlem7  27342  addsqrexnreu  27360  dchrisum0lem1  27434  nogt01o  27615  slenlt  27671  addscan1  27908  subseq0d  28015  mulscan2d  28089  mulscan1d  28090  muls0ord  28095  sltmuldiv2wd  28112  onnolt  28174  onslt  28175  om2noseqlt2  28201  zn0subs  28298  trgcgrg  28449  tgcgr4  28465  tgcolg  28488  lmiinv  28726  iseqlg  28801  elntg2  28919  cusgruvtxb  29356  upgrewlkle2  29541  clwwlkn1  29977  eupth2lem3lem3  30166  eupth2lem3lem6  30169  frgr3vlem2  30210  grpoid  30456  nvmeq0  30594  nvgt0  30610  imsmetlem  30626  nmlnogt0  30733  ip2eqi  30792  hvaddcan2  31007  hvmulcan2  31009  hvaddsub4  31014  hi2eq  31041  pjhtheu  31330  lnopeqi  31944  riesz1  32001  jpi  32206  chcv2  32292  cvp  32311  atnemeq0  32313  brabgaf  32543  fmptcof2  32588  funcnvmpt  32598  nndiffz1  32716  nn0min  32752  sgnneg  32765  xrge0addgt0  32965  lbslsp  33355  ressply1mon1p  33544  fldextrspunlsplem  33675  smatrcl  33793  lmlim  33944  carsggect  34316  eulerpartlems  34358  eulerpartlemgh  34376  ballotlemfc0  34491  ballotlemfcc  34492  signsvfpn  34583  signsvfnn  34584  reprdifc  34625  bnj1280  35017  lfuhgr  35112  satffunlem1lem2  35397  elmrsubrn  35514  msubff1  35550  fz0n  35725  imageval  35925  nn0prpwlem  36317  filnetlem4  36376  onsuct0  36436  onint1  36444  dissneqlem  37335  fvineqsneu  37406  wl-sbalnae  37557  wl-ax11-lem8  37587  wl-ax11-lem10  37589  sin2h  37611  tan2h  37613  matunitlindflem1  37617  matunitlindflem2  37618  matunitlindf  37619  poimirlem18  37639  poimirlem21  37642  poimirlem24  37645  heicant  37656  mblfinlem3  37660  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  mbfresfi  37667  mbfposadd  37668  itg2addnclem  37672  itg2addnclem2  37673  itg2addnc  37675  itg2gt0cn  37676  itgaddnclem2  37680  ftc1anclem5  37698  areacirclem1  37709  areacirclem4  37712  areacirc  37714  isdmn3  38075  eldmres2  38271  cnvref4  38339  relbrcoss  38444  releldmqs  38657  lcvp  39040  lcv2  39042  lsatnem0  39045  atnem0  39318  cvlsupr2  39343  cvr2N  39412  athgt  39457  2llnmat  39525  pmap11  39763  pmapeq0  39767  2lnat  39785  paddclN  39843  pmapjat1  39854  ltrn2ateq  40181  dihcnvord  41275  dihcnv11  41276  dih0bN  41282  dih0sb  41286  dihlspsnat  41334  dihatexv2  41340  dihglblem6  41341  dochvalr  41358  dochn0nv  41376  djhcvat42  41416  dochsatshp  41452  dochshpsat  41455  dochkrsat2  41457  lcfl5a  41498  lcfl8a  41504  lclkrlem2a  41508  mapdcnvordN  41659  hdmap14lem4a  41872  hgmapeq0  41905  hdmaplkr  41914  hdmapellkr  41915  cxp111d  42337  sn-remul0ord  42403  sn-ltmulgt11d  42469  frlmfielbas  42495  eu6w  42671  rmxycomplete  42913  gicabl  43095  minregex2  43531  ntrneiel  44077  ntrneik4w  44096  ntrneik4  44097  extoimad  44160  radcnvrat  44310  pm14.123b  44422  iotavalb  44426  infxrunb3  45427  climreeq  45618  clim2f  45641  clim2f2  45675  dfodd4  47664  oddprmne2  47720  nnsgrpnmnd  48170  ovmpordxf  48331  eenglngeehlnmlem2  48731  iscnrm3  48944  uptrlem1  49203