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  388  sbcom2  2168  19.21t  2206  19.23t  2210  sbco2  2553  sbco3  2555  sbal1  2572  sbal2  2573  sbal2OLD  2574  sbalOLD  2575  sbco2ALT  2615  csbiebt  3912  prsspwg  4756  ssprss  4757  reusv2lem5  5303  copsex2t  5383  copsex2g  5384  ordtri2  6226  onmindif  6280  fnssresb  6469  fcnvres  6556  foelrni  6727  funimass5  6825  fmptco  6891  cbvfo  7045  isocnv  7083  isoini  7091  isoselem  7094  riota2df  7137  ovmpodxf  7300  caovcanrd  7351  onmindif2  7527  ordunisuc2  7559  dfom2  7582  ordge1n0  8123  ondif2  8127  oa00  8185  odi  8205  oeoe  8225  eceqoveq  8402  isfinite2  8776  unfilem1  8782  fodomfib  8798  inficl  8889  dffi3  8895  ordiso2  8979  ordtypelem9  8990  cantnfle  9134  cantnf  9156  wemapwe  9160  rankr1a  9265  bnd2  9322  iscard  9404  domtri2  9418  nnsdomel  9419  cardaleph  9515  dfac12lem2  9570  cfss  9687  axcc3  9860  fodomb  9948  iundom2g  9962  inar1  10197  ltpiord  10309  ordpinq  10365  suplem2pr  10475  enreceq  10488  subeq0  10912  negcon1  10938  subexsub  11058  subeqrev  11062  lesub  11119  ltsub13  11121  subge0  11153  mul0or  11280  mulcan1g  11293  div11  11326  divmuleq  11345  mdiv  11476  ltmuldiv2  11514  lemuldiv2  11521  nn1suc  11660  addltmul  11874  elnnnn0  11941  znn0sub  12030  prime  12064  zbtwnre  12347  xadddi2  12691  supxrbnd  12722  fz1n  12926  fzrev3  12974  fzo0n  13060  fzonlt0  13061  ico01fl0  13190  divfl0  13195  modsubdir  13309  om2uzlt2i  13320  hashf1lem1  13814  wrdlenge1n0  13902  pfxccat3a  14100  cnpart  14599  sqrt11  14622  sqrtsq2  14628  absdiflt  14677  absdifle  14678  sqreulem  14719  sqreu  14720  eqsqrtor  14726  clim2  14861  climshft2  14939  isercoll  15024  sumrb  15070  supcvg  15211  prodrblem2  15285  sinbnd  15533  cosbnd  15534  sqrt2irr  15602  dvdscmulr  15638  dvdsmulcr  15639  oddm1even  15692  bitsmod  15785  bitsinv1lem  15790  qredeq  16001  cncongr2  16012  isprm3  16027  prmrp  16056  crth  16115  pcdvdsb  16205  pceq0  16207  unbenlem  16244  ramcl  16365  pwselbasb  16761  pwsle  16765  imasleval  16814  xpsfrnel2  16837  acsfn  16930  ismon2  17004  isepi2  17011  epii  17013  fthsect  17195  fthmon  17197  isipodrs  17771  ipodrsfi  17773  gsumval2a  17895  imasmnd2  17948  grpid  18139  grpidrcan  18164  grpidlcan  18165  grplmulf1o  18173  imasgrp2  18214  ghmeqker  18385  ghmf1  18387  gacan  18435  odmulgeq  18684  pgpssslw  18739  efgsfo  18865  efgred  18874  abladdsub4  18934  subgdmdprd  19156  imasring  19369  lspsnss2  19777  0ring01eqbi  20046  gsumbagdiaglem  20155  znf1o  20698  znfld  20707  znunit  20710  znrrg  20712  iporthcom  20779  ip2eq  20797  obsne0  20869  lindfmm  20971  lindsmm  20972  lsslinds  20975  eltg3  21570  eltop  21582  eltop2  21583  eltop3  21584  lmbrf  21868  cncnpi  21886  dfconn2  22027  1stcfb  22053  elptr  22181  xkoccn  22227  txcn  22234  hausdiag  22253  hmeoimaf1o  22378  isfbas  22437  ufileu  22527  alexsubALTlem4  22658  tsmsf1o  22753  ismet2  22943  imasdsf1olem  22983  imasf1oxmet  22985  imasf1omet  22986  xmseq0  23074  imasf1oxms  23099  metucn  23181  nrmmetd  23184  nmgt0  23239  nlmmul0or  23292  xrsxmet  23417  metdseq0  23462  elpi1i  23650  cphsqrtcl2  23790  tcphcph  23840  lmmbrf  23865  caucfil  23886  lmclim  23906  cmsss  23954  srabn  23963  ovolfioo  24068  ovolficc  24069  elovolmr  24077  ovolctb  24091  ovolicc2lem3  24120  mbfmulc2lem  24248  mbfimaopnlem  24256  itg2mulclem  24347  iblrelem  24391  ellimc2  24475  mdegle0  24671  fta1glem2  24760  dgreq0  24855  plydivlem4  24885  plydivex  24886  fta1  24897  quotcan  24898  logeftb  25167  quad2  25417  cubic2  25426  dquartlem1  25429  atandm4  25457  fsumharmonic  25589  wilthlem1  25645  basellem8  25665  mumullem2  25757  chpchtsum  25795  logfaclbnd  25798  dchrelbas4  25819  lgsne0  25911  lgsqrlem2  25923  lgsdchrval  25930  lgsquadlem1  25956  lgsquadlem2  25957  2sqlem7  26000  addsqrexnreu  26018  dchrisum0lem1  26092  trgcgrg  26301  tgcgr4  26317  tgcolg  26340  lmiinv  26578  iseqlg  26653  elntg2  26771  cusgruvtxb  27204  upgrewlkle2  27388  clwwlkn1  27819  eupth2lem3lem3  28009  eupth2lem3lem6  28012  frgr3vlem2  28053  grpoid  28297  nvmeq0  28435  nvgt0  28451  imsmetlem  28467  nmlnogt0  28574  ip2eqi  28633  hvaddcan2  28848  hvmulcan2  28850  hvaddsub4  28855  hi2eq  28882  pjhtheu  29171  lnopeqi  29785  riesz1  29842  jpi  30047  chcv2  30133  cvp  30152  atnemeq0  30154  brabgaf  30359  fmptcof2  30402  funcnvmpt  30412  nndiffz1  30509  nn0min  30536  xrge0addgt0  30678  lbslsp  30938  smatrcl  31061  lmlim  31190  carsggect  31576  eulerpartlems  31618  eulerpartlemgh  31636  ballotlemfc0  31750  ballotlemfcc  31751  sgnneg  31798  signsvfpn  31855  signsvfnn  31856  reprdifc  31898  bnj1280  32292  lfuhgr  32364  satffunlem1lem2  32650  elmrsubrn  32767  msubff1  32803  fz0n  32962  slenlt  33231  imageval  33391  nn0prpwlem  33670  filnetlem4  33729  onsuct0  33789  onint1  33797  dissneqlem  34624  fvineqsneu  34695  wl-sbalnae  34813  wl-ax11-lem8  34839  wl-ax11-lem10  34841  sin2h  34897  tan2h  34899  matunitlindflem1  34903  matunitlindflem2  34904  matunitlindf  34905  poimirlem18  34925  poimirlem21  34928  poimirlem24  34931  heicant  34942  mblfinlem3  34946  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  mbfresfi  34953  mbfposadd  34954  itg2addnclem  34958  itg2addnclem2  34959  itg2addnc  34961  itg2gt0cn  34962  itgaddnclem2  34966  ftc1anclem5  34986  areacirclem1  34997  areacirclem4  35000  areacirc  35002  isdmn3  35367  eldmres2  35547  relbrcoss  35701  releldmqs  35907  lcvp  36191  lcv2  36193  lsatnem0  36196  atnem0  36469  cvlsupr2  36494  cvr2N  36562  athgt  36607  2llnmat  36675  pmap11  36913  pmapeq0  36917  2lnat  36935  paddclN  36993  pmapjat1  37004  ltrn2ateq  37331  dihcnvord  38425  dihcnv11  38426  dih0bN  38432  dih0sb  38436  dihlspsnat  38484  dihatexv2  38490  dihglblem6  38491  dochvalr  38508  dochn0nv  38526  djhcvat42  38566  dochsatshp  38602  dochshpsat  38605  dochkrsat2  38607  lcfl5a  38648  lcfl8a  38654  lclkrlem2a  38658  mapdcnvordN  38809  hdmap14lem4a  39022  hgmapeq0  39055  hdmaplkr  39064  hdmapellkr  39065  frlmfielbas  39188  rmxycomplete  39563  gicabl  39748  ntrneiel  40480  ntrneik4w  40499  ntrneik4  40500  extoimad  40564  radcnvrat  40695  pm14.123b  40807  iotavalb  40811  infxrunb3  41747  climreeq  41943  clim2f  41966  clim2f2  42000  dfodd4  43873  oddprmne2  43929  nnsgrpnmnd  44134  ovmpordxf  44436  eenglngeehlnmlem2  44774