Theorem bitr3d 284

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitrrd  309  3bitr3d  312  3bitr3rd  313  biass  388  sbcom2  2208  19.21t  2242  19.23t  2246  sbco2  2540  sbco3  2542  sbal1  2557  sbal2  2558  clelab  2904  ceqsralt  3484  csbiebt  3875  prsspwg  4783  ssprss  4784  reusv2lem5  5363  copsex2t  5463  ordtri2  6398  onmindif  6457  fnssresb  6661  fcnvres  6759  foelcdmi  6946  funcnvmpt  6995  funimass5  7054  fmptco  7130  cbvfo  7297  isocnv  7338  isoini  7346  isoselem  7349  riota2df  7400  ovmpodxf  7570  caovcanrd  7624  onmindif2  7821  ordunisuc2  7855  dfom2  7879  frxp2  8161  xpord2pred  8162  xpord3pred  8169  ordge1n0  8502  ondif2  8510  oa00  8567  odi  8587  oeoe  8608  eceqoveq  8843  isfinite2  9290  unfilem1  9297  fodomfib  9320  inficl  9417  dffi3  9423  ordiso2  9509  ordtypelem9  9520  cantnfle  9672  cantnf  9694  wemapwe  9698  rankr1a  9848  bnd2  9956  iscard  10056  domtri2  10070  nnsdomel  10071  cardaleph  10168  dfac12lem2  10223  cfss  10343  axcc3  10516  fodomb  10605  iundom2g  10624  inar1  10860  ltpiord  10972  ordpinq  11028  suplem2pr  11138  enreceq  11151  subeq0  11584  negcon1  11610  subexsub  11734  subeqrev  11738  lesub  11795  ltsub13  11797  subge0  11829  mul0or  11956  mulcan1g  11969  divmuleq  12022  mdiv  12153  ltmuldiv2  12191  lemuldiv2  12198  nn1suc  12357  addltmul  12582  elnnnn0  12649  znn0sub  12743  prime  12780  zbtwnre  13073  xadddi2  13427  supxrbnd  13458  fz1n  13675  fzrev3  13724  fzo0n  13816  fzonlt0  13817  ico01fl0  13959  divfl0  13964  modaddid  14050  modsubdir  14083  om2uzlt2i  14094  hashf1lem1  14600  wrdlenge1n0  14695  pfxccat3a  14887  sgnneg  15253  cnpart  15407  sqrt11  15429  sqrtsq2  15435  absdiflt  15485  absdifle  15486  sqreulem  15527  sqreu  15528  eqsqrtor  15534  clim2  15671  climshft2  15749  isercoll  15835  sumrb  15879  supcvg  16025  prodrblem2  16098  sinbnd  16348  cosbnd  16349  sqrt2irr  16417  dvdscmulr  16454  dvdsmulcr  16455  oddm1even  16513  bitsmod  16606  bitsinv1lem  16611  qredeq  16832  cncongr2  16843  isprm3  16858  prmrp  16888  crth  16955  pcdvdsb  17047  pceq0  17049  unbenlem  17086  ramcl  17207  pwselbasb  17659  pwsle  17664  imasleval  17713  xpsfrnel2  17736  acsfn  17833  ismon2  17909  isepi2  17916  epii  17918  fthsect  18102  fthmon  18104  isipodrs  18711  ipodrsfi  18713  imasmgm2  18863  gsumval2a  18874  imasmnd2  18968  grpid  19186  grpidrcan  19214  grpidlcan  19215  grplmulf1o  19223  grpraddf1o  19224  imasgrp2  19265  eqg0subg  19411  ghmeqker  19457  gacan  19519  odmulgeq  19771  pgpssslw  19828  efgsfo  19953  efgred  19962  abladdsub4  20025  subgdmdprd  20250  imasrng  20399  imasring  20560  0ring01eqbi  20784  domneq0r  20975  lspsnss2  21280  znf1o  21857  znfld  21866  znunit  21869  znrrg  21871  iporthcom  21941  ip2eq  21959  obsne0  22031  lindfmm  22133  lindsmm  22134  lsslinds  22137  gsumbagdiaglem  22239  psdmul  22487  matunitlindflem1  22994  matunitlindflem2  22995  matunitlindf  22996  eltg3  23280  eltop  23292  eltop2  23293  eltop3  23294  lmbrf  23578  cncnpi  23596  dfconn2  23737  1stcfb  23763  elptr  23892  xkoccn  23938  txcn  23945  hausdiag  23964  hmeoimaf1o  24089  isfbas  24148  ufileu  24238  alexsubALTlem4  24369  tsmsf1o  24464  ismet2  24652  imasdsf1olem  24692  imasf1oxmet  24694  imasf1omet  24695  xmseq0  24783  imasf1oxms  24808  metucn  24890  nrmmetd  24893  nmgt0  24949  nlmmul0or  25002  xrsxmet  25129  metdseq0  25174  elpi1i  25367  cphsqrtcl2  25507  tcphcph  25558  lmmbrf  25583  caucfil  25604  lmclim  25624  cmsss  25672  srabn  25681  ovolfioo  25788  ovolficc  25789  elovolmr  25797  ovolctb  25811  ovolicc2lem3  25840  mbfmulc2lem  25968  mbfimaopnlem  25976  itg2mulclem  26067  iblrelem  26111  ellimc2  26197  mdegle0  26395  fta1glem2  26487  dgreq0  26584  plydivlem4  26617  plydivex  26618  fta1  26629  quotcan  26632  logeftb  26911  quad2  27167  cubic2  27176  dquartlem1  27179  atandm4  27207  fsumharmonic  27339  wilthlem1  27395  basellem8  27415  mumullem2  27507  fsumdvdsmul  27522  chpchtsum  27546  logfaclbnd  27549  dchrelbas4  27570  lgsne0  27662  lgsqrlem2  27674  lgsdchrval  27681  lgsquadlem1  27707  lgsquadlem2  27708  2sqlem7  27751  addsqrexnreu  27769  dchrisum0lem1  27843  flt4ALT  27992  nogt01o  28053  lenlts  28109  addscan1  28380  subseq0d  28491  mulscan2d  28565  mulscan1d  28566  muls0ord  28571  ltmuldivs2wd  28588  onnolt  28652  onlts  28653  om2noseqlt2  28686  zn0subs  28789  bdaypw2n0bndlem  28849  bdayfinbndlem1  28853  trgcgrg  28978  tgcgr4  28994  tgcolg  29017  plngrotlem2  29266  lmiinv  29297  iseqlg  29412  elntg2  29563  lfuhgr  29726  cusgruvtxb  30003  upgrewlkle2  30187  clwwlkn1  30632  eupth2lem3lem3  30831  eupth2lem3lem6  30834  frgr3vlem2  30875  grpoid  31122  nvmeq0  31260  nvgt0  31276  imsmetlem  31292  nmlnogt0  31399  ip2eqi  31458  hvaddcan2  31673  hvmulcan2  31675  hvaddsub4  31680  hi2eq  31707  pjhtheu  31996  lnopeqi  32610  riesz1  32667  jpi  32872  chcv2  32958  cvp  32977  atnemeq0  32979  brabgaf  33242  fmptcof2  33293  nndiffz1  33420  nn0min  33454  xrge0addgt0  33620  rlocisunit  33879  lbslsp  33974  ressply1mon1p  34142  fldextrspunlsplem  34347  smatrcl  34470  lmlim  34621  carsggect  34992  eulerpartlems  35034  eulerpartlemgh  35052  ballotlemfc0  35167  ballotlemfcc  35168  signsvfpn  35256  signsvfnn  35257  reprdifc  35298  bnj1280  35692  fineqvnttrclselem3  35833  satffunlem1lem2  36210  elmrsubrn  36327  msubff1  36363  fz0n  36538  imageval  36734  nn0prpwlem  37152  filnetlem4  37211  onsuct0  37271  onint1  37279  dissneqlem  38306  fvineqsneu  38377  wl-sbalnae  38537  sin2h  38576  tan2h  38578  poimirlem18  38599  poimirlem21  38602  poimirlem24  38605  heicant  38616  mblfinlem3  38620  ovoliunnfl  38623  voliunnfl  38625  volsupnfl  38626  mbfresfi  38627  mbfposadd  38628  itg2addnclem  38632  itg2addnclem2  38633  itg2addnc  38635  itg2gt0cn  38636  itgaddnclem2  38640  ftc1anclem5  38658  areacirclem1  38669  areacirclem4  38672  areacirc  38674  isdmn3  39051  eldmres2  39257  cnvref4  39325  relbrcoss  39511  releldmqs  39718  lcvp  40140  lcv2  40142  lsatnem0  40145  atnem0  40418  cvlsupr2  40443  cvr2N  40511  athgt  40556  2llnmat  40624  pmap11  40862  pmapeq0  40866  2lnat  40884  paddclN  40942  pmapjat1  40953  ltrn2ateq  41280  dihcnvord  42374  dihcnv11  42375  dih0bN  42381  dih0sb  42385  dihlspsnat  42433  dihatexv2  42439  dihglblem6  42440  dochvalr  42457  dochn0nv  42475  djhcvat42  42515  dochsatshp  42551  dochshpsat  42554  dochkrsat2  42556  lcfl5a  42597  lcfl8a  42603  lclkrlem2a  42607  mapdcnvordN  42758  hdmap14lem4a  42971  hgmapeq0  43004  hdmaplkr  43013  hdmapellkr  43014  cxp111d  43436  sn-remul0ord  43502  sn-ltmulgt11d  43581  frlmfielbas  43610  eu6w  43730  rmxycomplete  43967  gicabl  44144  minregex2  44579  ntrneiel  45124  ntrneik4w  45143  ntrneik4  45144  extoimad  45207  radcnvrat  45341  pm14.123b  45453  iotavalb  45457  infxrunb3  46477  climreeq  46668  clim2f  46689  clim2f2  46723  dfodd4  48800  oddprmne2  48856  nnsgrpnmnd  49318  isidom3  49485  ovmpordxf  49494  eenglngeehlnmlem2  49893  iscnrm3  50103  uptrlem1  50361