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  2196  19.21t  2231  19.23t  2235  sbco2  2532  sbco3  2534  sbal1  2549  sbal2  2550  clelab  2896  ceqsralt  3478  csbiebt  3872  prsspwg  4771  ssprss  4772  reusv2lem5  5349  copsex2t  5451  ordtri2  6366  onmindif  6425  fnssresb  6628  fcnvres  6726  foelcdmi  6913  funcnvmpt  6962  funimass5  7021  fmptco  7096  cbvfo  7258  isocnv  7299  isoini  7307  isoselem  7310  riota2df  7361  ovmpodxf  7531  caovcanrd  7584  onmindif2  7775  ordunisuc2  7809  dfom2  7833  frxp2  8108  xpord2pred  8109  xpord3pred  8116  ordge1n0  8447  ondif2  8455  oa00  8512  odi  8532  oeoe  8553  eceqoveq  8788  isfinite2  9227  unfilem1  9234  fodomfib  9258  fodomfibOLD  9260  inficl  9357  dffi3  9363  ordiso2  9449  ordtypelem9  9460  cantnfle  9612  cantnf  9634  wemapwe  9638  rankr1a  9780  bnd2  9837  iscard  9919  domtri2  9933  nnsdomel  9934  cardaleph  10031  dfac12lem2  10087  cfss  10208  axcc3  10381  fodomb  10469  iundom2g  10483  inar1  10719  ltpiord  10831  ordpinq  10887  suplem2pr  10997  enreceq  11010  subeq0  11443  negcon1  11469  subexsub  11591  subeqrev  11595  lesub  11652  ltsub13  11654  subge0  11686  mul0or  11813  mulcan1g  11826  div11OLD  11860  divmuleq  11882  mdiv  12013  ltmuldiv2  12052  lemuldiv2  12059  nn1suc  12218  addltmul  12443  elnnnn0  12510  znn0sub  12604  prime  12640  zbtwnre  12933  xadddi2  13286  supxrbnd  13317  fz1n  13533  fzrev3  13581  fzo0n  13673  fzonlt0  13674  ico01fl0  13815  divfl0  13820  modaddid  13906  modsubdir  13939  om2uzlt2i  13950  hashf1lem1  14454  wrdlenge1n0  14549  pfxccat3a  14737  cnpart  15239  sqrt11  15261  sqrtsq2  15267  absdiflt  15317  absdifle  15318  sqreulem  15359  sqreu  15360  eqsqrtor  15366  clim2  15503  climshft2  15581  isercoll  15667  sumrb  15712  supcvg  15858  prodrblem2  15933  sinbnd  16184  cosbnd  16185  sqrt2irr  16253  dvdscmulr  16290  dvdsmulcr  16291  oddm1even  16349  bitsmod  16442  bitsinv1lem  16447  qredeq  16663  cncongr2  16674  isprm3  16689  prmrp  16719  crth  16785  pcdvdsb  16877  pceq0  16879  unbenlem  16916  ramcl  17037  pwselbasb  17489  pwsle  17494  imasleval  17543  xpsfrnel2  17566  acsfn  17663  ismon2  17739  isepi2  17746  epii  17748  fthsect  17932  fthmon  17934  isipodrs  18541  ipodrsfi  18543  gsumval2a  18691  imasmnd2  18780  grpid  18989  grpidrcan  19017  grpidlcan  19018  grplmulf1o  19027  grpraddf1o  19028  imasgrp2  19069  eqg0subg  19209  ghmeqker  19255  gacan  19317  odmulgeq  19569  pgpssslw  19626  efgsfo  19751  efgred  19760  abladdsub4  19823  subgdmdprd  20048  imasrng  20195  imasring  20347  0ring01eqbi  20550  domneq0r  20742  lspsnss2  21041  znf1o  21572  znfld  21581  znunit  21584  znrrg  21586  iporthcom  21656  ip2eq  21674  obsne0  21746  lindfmm  21848  lindsmm  21849  lsslinds  21852  gsumbagdiaglem  21952  psdmul  22200  eltg3  22991  eltop  23003  eltop2  23004  eltop3  23005  lmbrf  23289  cncnpi  23307  dfconn2  23448  1stcfb  23474  elptr  23602  xkoccn  23648  txcn  23655  hausdiag  23674  hmeoimaf1o  23799  isfbas  23858  ufileu  23948  alexsubALTlem4  24079  tsmsf1o  24174  ismet2  24362  imasdsf1olem  24402  imasf1oxmet  24404  imasf1omet  24405  xmseq0  24493  imasf1oxms  24518  metucn  24600  nrmmetd  24603  nmgt0  24659  nlmmul0or  24712  xrsxmet  24839  metdseq0  24884  elpi1i  25077  cphsqrtcl2  25217  tcphcph  25268  lmmbrf  25293  caucfil  25314  lmclim  25334  cmsss  25382  srabn  25391  ovolfioo  25498  ovolficc  25499  elovolmr  25507  ovolctb  25521  ovolicc2lem3  25550  mbfmulc2lem  25678  mbfimaopnlem  25686  itg2mulclem  25777  iblrelem  25822  ellimc2  25908  mdegle0  26106  fta1glem2  26198  dgreq0  26294  plydivlem4  26326  plydivex  26327  fta1  26338  quotcan  26339  logeftb  26614  quad2  26870  cubic2  26879  dquartlem1  26882  atandm4  26910  fsumharmonic  27042  wilthlem1  27098  basellem8  27118  mumullem2  27210  fsumdvdsmul  27225  chpchtsum  27249  logfaclbnd  27252  dchrelbas4  27273  lgsne0  27365  lgsqrlem2  27377  lgsdchrval  27384  lgsquadlem1  27410  lgsquadlem2  27411  2sqlem7  27454  addsqrexnreu  27472  dchrisum0lem1  27546  nogt01o  27726  lenlts  27782  addscan1  28053  subseq0d  28164  mulscan2d  28238  mulscan1d  28239  muls0ord  28244  ltmuldivs2wd  28261  onnolt  28325  onlts  28326  om2noseqlt2  28359  zn0subs  28462  bdaypw2n0bndlem  28522  bdayfinbndlem1  28526  trgcgrg  28650  tgcgr4  28666  tgcolg  28689  lmiinv  28927  iseqlg  29002  elntg2  29121  cusgruvtxb  29558  upgrewlkle2  29742  clwwlkn1  30178  eupth2lem3lem3  30367  eupth2lem3lem6  30370  frgr3vlem2  30411  grpoid  30658  nvmeq0  30796  nvgt0  30812  imsmetlem  30828  nmlnogt0  30935  ip2eqi  30994  hvaddcan2  31209  hvmulcan2  31211  hvaddsub4  31216  hi2eq  31243  pjhtheu  31532  lnopeqi  32146  riesz1  32203  jpi  32408  chcv2  32494  cvp  32513  atnemeq0  32515  brabgaf  32747  fmptcof2  32798  nndiffz1  32927  nn0min  32962  sgnneg  32974  xrge0addgt0  33145  lbslsp  33509  ressply1mon1p  33708  fldextrspunlsplem  33914  smatrcl  34037  lmlim  34188  carsggect  34559  eulerpartlems  34601  eulerpartlemgh  34619  ballotlemfc0  34734  ballotlemfcc  34735  signsvfpn  34826  signsvfnn  34827  reprdifc  34868  bnj1280  35262  fineqvnttrclselem3  35364  lfuhgr  35406  satffunlem1lem2  35691  elmrsubrn  35808  msubff1  35844  fz0n  36019  imageval  36216  nn0prpwlem  36620  filnetlem4  36679  onsuct0  36739  onint1  36747  dissneqlem  37772  fvineqsneu  37843  wl-sbalnae  38003  sin2h  38047  tan2h  38049  matunitlindflem1  38053  matunitlindflem2  38054  matunitlindf  38055  poimirlem18  38075  poimirlem21  38078  poimirlem24  38081  heicant  38092  mblfinlem3  38096  ovoliunnfl  38099  voliunnfl  38101  volsupnfl  38102  mbfresfi  38103  mbfposadd  38104  itg2addnclem  38108  itg2addnclem2  38109  itg2addnc  38111  itg2gt0cn  38112  itgaddnclem2  38116  ftc1anclem5  38134  areacirclem1  38145  areacirclem4  38148  areacirc  38150  isdmn3  38511  eldmres2  38719  cnvref4  38787  relbrcoss  38973  releldmqs  39180  lcvp  39602  lcv2  39604  lsatnem0  39607  atnem0  39880  cvlsupr2  39905  cvr2N  39973  athgt  40018  2llnmat  40086  pmap11  40324  pmapeq0  40328  2lnat  40346  paddclN  40404  pmapjat1  40415  ltrn2ateq  40742  dihcnvord  41836  dihcnv11  41837  dih0bN  41843  dih0sb  41847  dihlspsnat  41895  dihatexv2  41901  dihglblem6  41902  dochvalr  41919  dochn0nv  41937  djhcvat42  41977  dochsatshp  42013  dochshpsat  42016  dochkrsat2  42018  lcfl5a  42059  lcfl8a  42065  lclkrlem2a  42069  mapdcnvordN  42220  hdmap14lem4a  42433  hgmapeq0  42466  hdmaplkr  42475  hdmapellkr  42476  cxp111d  42889  sn-remul0ord  42955  sn-ltmulgt11d  43034  frlmfielbas  43060  eu6w  43196  rmxycomplete  43432  gicabl  43614  minregex2  44049  ntrneiel  44595  ntrneik4w  44614  ntrneik4  44615  extoimad  44678  radcnvrat  44828  pm14.123b  44940  iotavalb  44944  infxrunb3  45936  climreeq  46127  clim2f  46148  clim2f2  46182  dfodd4  48219  oddprmne2  48275  nnsgrpnmnd  48738  ovmpordxf  48899  eenglngeehlnmlem2  49298  iscnrm3  49511  uptrlem1  49769