Theorem bitr3d 283

Description: Deduction form of bitr3i 279. (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 225	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
3		bitr3d.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 281	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3bitrrd  308  3bitr3d  311  3bitr3rd  312  biass  387  sbcom2  2207  19.21t  2242  19.23t  2246  sbco2  2543  sbco3  2545  sbal1  2560  sbal2  2561  clelab  2907  ceqsralt  3489  csbiebt  3882  prsspwg  4782  ssprss  4783  reusv2lem5  5360  copsex2t  5462  ordtri2  6381  onmindif  6440  fnssresb  6643  fcnvres  6741  foelcdmi  6928  funcnvmpt  6977  funimass5  7036  fmptco  7111  cbvfo  7273  isocnv  7314  isoini  7322  isoselem  7325  riota2df  7376  ovmpodxf  7546  caovcanrd  7599  onmindif2  7790  ordunisuc2  7824  dfom2  7848  frxp2  8124  xpord2pred  8125  xpord3pred  8132  ordge1n0  8463  ondif2  8471  oa00  8528  odi  8548  oeoe  8569  eceqoveq  8804  isfinite2  9242  unfilem1  9249  fodomfib  9272  inficl  9369  dffi3  9375  ordiso2  9461  ordtypelem9  9472  cantnfle  9624  cantnf  9646  wemapwe  9650  rankr1a  9792  bnd2  9863  iscard  9945  domtri2  9959  nnsdomel  9960  cardaleph  10057  dfac12lem2  10112  cfss  10233  axcc3  10406  fodomb  10494  iundom2g  10508  inar1  10744  ltpiord  10856  ordpinq  10912  suplem2pr  11022  enreceq  11035  subeq0  11468  negcon1  11494  subexsub  11616  subeqrev  11620  lesub  11677  ltsub13  11679  subge0  11711  mul0or  11838  mulcan1g  11851  div11OLD  11885  divmuleq  11907  mdiv  12038  ltmuldiv2  12076  lemuldiv2  12083  nn1suc  12242  addltmul  12467  elnnnn0  12534  znn0sub  12628  prime  12664  zbtwnre  12957  xadddi2  13310  supxrbnd  13341  fz1n  13557  fzrev3  13605  fzo0n  13697  fzonlt0  13698  ico01fl0  13839  divfl0  13844  modaddid  13930  modsubdir  13963  om2uzlt2i  13974  hashf1lem1  14478  wrdlenge1n0  14573  pfxccat3a  14761  sgnneg  15123  cnpart  15277  sqrt11  15299  sqrtsq2  15305  absdiflt  15355  absdifle  15356  sqreulem  15397  sqreu  15398  eqsqrtor  15404  clim2  15541  climshft2  15619  isercoll  15705  sumrb  15750  supcvg  15896  prodrblem2  15971  sinbnd  16222  cosbnd  16223  sqrt2irr  16291  dvdscmulr  16328  dvdsmulcr  16329  oddm1even  16387  bitsmod  16480  bitsinv1lem  16485  qredeq  16701  cncongr2  16712  isprm3  16727  prmrp  16757  crth  16823  pcdvdsb  16915  pceq0  16917  unbenlem  16954  ramcl  17075  pwselbasb  17527  pwsle  17532  imasleval  17581  xpsfrnel2  17604  acsfn  17701  ismon2  17777  isepi2  17784  epii  17786  fthsect  17970  fthmon  17972  isipodrs  18579  ipodrsfi  18581  gsumval2a  18729  imasmnd2  18818  grpid  19027  grpidrcan  19055  grpidlcan  19056  grplmulf1o  19065  grpraddf1o  19066  imasgrp2  19107  eqg0subg  19247  ghmeqker  19293  gacan  19355  odmulgeq  19607  pgpssslw  19664  efgsfo  19789  efgred  19798  abladdsub4  19861  subgdmdprd  20086  imasrng  20233  imasring  20389  0ring01eqbi  20592  domneq0r  20783  lspsnss2  21079  znf1o  21610  znfld  21619  znunit  21622  znrrg  21624  iporthcom  21694  ip2eq  21712  obsne0  21784  lindfmm  21886  lindsmm  21887  lsslinds  21890  gsumbagdiaglem  21990  psdmul  22238  eltg3  23029  eltop  23041  eltop2  23042  eltop3  23043  lmbrf  23327  cncnpi  23345  dfconn2  23486  1stcfb  23512  elptr  23640  xkoccn  23686  txcn  23693  hausdiag  23712  hmeoimaf1o  23837  isfbas  23896  ufileu  23986  alexsubALTlem4  24117  tsmsf1o  24212  ismet2  24400  imasdsf1olem  24440  imasf1oxmet  24442  imasf1omet  24443  xmseq0  24531  imasf1oxms  24556  metucn  24638  nrmmetd  24641  nmgt0  24697  nlmmul0or  24750  xrsxmet  24877  metdseq0  24922  elpi1i  25115  cphsqrtcl2  25255  tcphcph  25306  lmmbrf  25331  caucfil  25352  lmclim  25372  cmsss  25420  srabn  25429  ovolfioo  25536  ovolficc  25537  elovolmr  25545  ovolctb  25559  ovolicc2lem3  25588  mbfmulc2lem  25716  mbfimaopnlem  25724  itg2mulclem  25815  iblrelem  25860  ellimc2  25946  mdegle0  26144  fta1glem2  26236  dgreq0  26332  plydivlem4  26367  plydivex  26368  fta1  26379  quotcan  26380  logeftb  26655  quad2  26911  cubic2  26920  dquartlem1  26923  atandm4  26951  fsumharmonic  27083  wilthlem1  27139  basellem8  27159  mumullem2  27251  fsumdvdsmul  27266  chpchtsum  27290  logfaclbnd  27293  dchrelbas4  27314  lgsne0  27406  lgsqrlem2  27418  lgsdchrval  27425  lgsquadlem1  27451  lgsquadlem2  27452  2sqlem7  27495  addsqrexnreu  27513  dchrisum0lem1  27587  nogt01o  27767  lenlts  27823  addscan1  28094  subseq0d  28205  mulscan2d  28279  mulscan1d  28280  muls0ord  28285  ltmuldivs2wd  28302  onnolt  28366  onlts  28367  om2noseqlt2  28400  zn0subs  28503  bdaypw2n0bndlem  28563  bdayfinbndlem1  28567  trgcgrg  28691  tgcgr4  28707  tgcolg  28730  lmiinv  28972  plngrotlem2  29002  iseqlg  29068  elntg2  29193  cusgruvtxb  29630  upgrewlkle2  29814  clwwlkn1  30250  eupth2lem3lem3  30439  eupth2lem3lem6  30442  frgr3vlem2  30483  grpoid  30730  nvmeq0  30868  nvgt0  30884  imsmetlem  30900  nmlnogt0  31007  ip2eqi  31066  hvaddcan2  31281  hvmulcan2  31283  hvaddsub4  31288  hi2eq  31315  pjhtheu  31604  lnopeqi  32218  riesz1  32275  jpi  32480  chcv2  32566  cvp  32585  atnemeq0  32587  brabgaf  32814  fmptcof2  32865  nndiffz1  32994  nn0min  33029  xrge0addgt0  33201  rlocisunit  33463  lbslsp  33566  ressply1mon1p  33767  fldextrspunlsplem  33972  smatrcl  34095  lmlim  34246  carsggect  34617  eulerpartlems  34659  eulerpartlemgh  34677  ballotlemfc0  34792  ballotlemfcc  34793  signsvfpn  34881  signsvfnn  34882  reprdifc  34923  bnj1280  35317  fineqvnttrclselem3  35423  lfuhgr  35473  satffunlem1lem2  35758  elmrsubrn  35875  msubff1  35911  fz0n  36086  imageval  36283  nn0prpwlem  36687  filnetlem4  36746  onsuct0  36806  onint1  36814  dissneqlem  37839  fvineqsneu  37910  wl-sbalnae  38070  sin2h  38114  tan2h  38116  matunitlindflem1  38120  matunitlindflem2  38121  matunitlindf  38122  poimirlem18  38142  poimirlem21  38145  poimirlem24  38148  heicant  38159  mblfinlem3  38163  ovoliunnfl  38166  voliunnfl  38168  volsupnfl  38169  mbfresfi  38170  mbfposadd  38171  itg2addnclem  38175  itg2addnclem2  38176  itg2addnc  38178  itg2gt0cn  38179  itgaddnclem2  38183  ftc1anclem5  38201  areacirclem1  38212  areacirclem4  38215  areacirc  38217  isdmn3  38578  eldmres2  38786  cnvref4  38854  relbrcoss  39040  releldmqs  39247  lcvp  39669  lcv2  39671  lsatnem0  39674  atnem0  39947  cvlsupr2  39972  cvr2N  40040  athgt  40085  2llnmat  40153  pmap11  40391  pmapeq0  40395  2lnat  40413  paddclN  40471  pmapjat1  40482  ltrn2ateq  40809  dihcnvord  41903  dihcnv11  41904  dih0bN  41910  dih0sb  41914  dihlspsnat  41962  dihatexv2  41968  dihglblem6  41969  dochvalr  41986  dochn0nv  42004  djhcvat42  42044  dochsatshp  42080  dochshpsat  42083  dochkrsat2  42085  lcfl5a  42126  lcfl8a  42132  lclkrlem2a  42136  mapdcnvordN  42287  hdmap14lem4a  42500  hgmapeq0  42533  hdmaplkr  42542  hdmapellkr  42543  cxp111d  42956  sn-remul0ord  43022  sn-ltmulgt11d  43101  frlmfielbas  43127  eu6w  43263  rmxycomplete  43499  gicabl  43681  minregex2  44116  ntrneiel  44662  ntrneik4w  44681  ntrneik4  44682  extoimad  44745  radcnvrat  44881  pm14.123b  44993  iotavalb  44997  infxrunb3  45989  climreeq  46180  clim2f  46201  clim2f2  46235  dfodd4  48272  oddprmne2  48328  nnsgrpnmnd  48791  ovmpordxf  48952  eenglngeehlnmlem2  49351  iscnrm3  49564  uptrlem1  49822