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  2173  19.21t  2206  19.23t  2210  sbco2  2515  sbco3  2517  sbal1  2532  sbal2  2533  clelab  2880  ceqsralt  3495  csbiebt  3903  prsspwg  4799  ssprss  4800  reusv2lem5  5372  copsex2t  5467  ordtri2  6387  onmindif  6445  fnssresb  6659  fcnvres  6754  foelcdmi  6939  funimass5  7044  fmptco  7118  cbvfo  7281  isocnv  7322  isoini  7330  isoselem  7333  riota2df  7383  ovmpodxf  7555  caovcanrd  7608  onmindif2  7799  ordunisuc2  7837  dfom2  7861  frxp2  8141  xpord2pred  8142  xpord3pred  8149  ordge1n0  8504  ondif2  8512  oa00  8569  odi  8589  oeoe  8609  eceqoveq  8834  isfinite2  9304  unfilem1  9313  fodomfib  9339  fodomfibOLD  9341  inficl  9435  dffi3  9441  ordiso2  9527  ordtypelem9  9538  cantnfle  9683  cantnf  9705  wemapwe  9709  rankr1a  9848  bnd2  9905  iscard  9987  domtri2  10001  nnsdomel  10002  cardaleph  10101  dfac12lem2  10157  cfss  10277  axcc3  10450  fodomb  10538  iundom2g  10552  inar1  10787  ltpiord  10899  ordpinq  10955  suplem2pr  11065  enreceq  11078  subeq0  11507  negcon1  11533  subexsub  11653  subeqrev  11657  lesub  11714  ltsub13  11716  subge0  11748  mul0or  11875  mulcan1g  11888  div11OLD  11923  divmuleq  11944  mdiv  12075  ltmuldiv2  12114  lemuldiv2  12121  nn1suc  12260  addltmul  12475  elnnnn0  12542  znn0sub  12637  prime  12672  zbtwnre  12960  xadddi2  13311  supxrbnd  13342  fz1n  13557  fzrev3  13605  fzo0n  13696  fzonlt0  13697  ico01fl0  13834  divfl0  13839  modsubdir  13956  om2uzlt2i  13967  hashf1lem1  14471  wrdlenge1n0  14566  pfxccat3a  14754  cnpart  15257  sqrt11  15279  sqrtsq2  15285  absdiflt  15334  absdifle  15335  sqreulem  15376  sqreu  15377  eqsqrtor  15383  clim2  15518  climshft2  15596  isercoll  15682  sumrb  15727  supcvg  15870  prodrblem2  15945  sinbnd  16196  cosbnd  16197  sqrt2irr  16265  dvdscmulr  16302  dvdsmulcr  16303  oddm1even  16360  bitsmod  16453  bitsinv1lem  16458  qredeq  16674  cncongr2  16685  isprm3  16700  prmrp  16729  crth  16795  pcdvdsb  16887  pceq0  16889  unbenlem  16926  ramcl  17047  pwselbasb  17500  pwsle  17504  imasleval  17553  xpsfrnel2  17576  acsfn  17669  ismon2  17745  isepi2  17752  epii  17754  fthsect  17938  fthmon  17940  isipodrs  18545  ipodrsfi  18547  gsumval2a  18661  imasmnd2  18750  grpid  18956  grpidrcan  18984  grpidlcan  18985  grplmulf1o  18994  grpraddf1o  18995  imasgrp2  19036  eqg0subg  19177  ghmeqker  19224  gacan  19286  odmulgeq  19536  pgpssslw  19593  efgsfo  19718  efgred  19727  abladdsub4  19790  subgdmdprd  20015  imasrng  20135  imasring  20288  0ring01eqbi  20490  domneq0r  20682  lspsnss2  20960  znf1o  21510  znfld  21519  znunit  21522  znrrg  21524  iporthcom  21593  ip2eq  21611  obsne0  21683  lindfmm  21785  lindsmm  21786  lsslinds  21789  gsumbagdiaglem  21888  psdmul  22102  eltg3  22898  eltop  22910  eltop2  22911  eltop3  22912  lmbrf  23196  cncnpi  23214  dfconn2  23355  1stcfb  23381  elptr  23509  xkoccn  23555  txcn  23562  hausdiag  23581  hmeoimaf1o  23706  isfbas  23765  ufileu  23855  alexsubALTlem4  23986  tsmsf1o  24081  ismet2  24270  imasdsf1olem  24310  imasf1oxmet  24312  imasf1omet  24313  xmseq0  24401  imasf1oxms  24426  metucn  24508  nrmmetd  24511  nmgt0  24567  nlmmul0or  24620  xrsxmet  24747  metdseq0  24792  elpi1i  24995  cphsqrtcl2  25136  tcphcph  25187  lmmbrf  25212  caucfil  25233  lmclim  25253  cmsss  25301  srabn  25310  ovolfioo  25418  ovolficc  25419  elovolmr  25427  ovolctb  25441  ovolicc2lem3  25470  mbfmulc2lem  25598  mbfimaopnlem  25606  itg2mulclem  25697  iblrelem  25742  ellimc2  25828  mdegle0  26032  fta1glem2  26124  dgreq0  26221  plydivlem4  26254  plydivex  26255  fta1  26266  quotcan  26267  logeftb  26542  quad2  26799  cubic2  26808  dquartlem1  26811  atandm4  26839  fsumharmonic  26972  wilthlem1  27028  basellem8  27048  mumullem2  27140  fsumdvdsmul  27155  chpchtsum  27180  logfaclbnd  27183  dchrelbas4  27204  lgsne0  27296  lgsqrlem2  27308  lgsdchrval  27315  lgsquadlem1  27341  lgsquadlem2  27342  2sqlem7  27385  addsqrexnreu  27403  dchrisum0lem1  27477  nogt01o  27658  slenlt  27714  addscan1  27944  mulscan2d  28122  mulscan1d  28123  muls0ord  28128  sltmuldiv2wd  28144  om2noseqlt2  28223  zn0subs  28306  trgcgrg  28440  tgcgr4  28456  tgcolg  28479  lmiinv  28717  iseqlg  28792  elntg2  28910  cusgruvtxb  29347  upgrewlkle2  29532  clwwlkn1  29968  eupth2lem3lem3  30157  eupth2lem3lem6  30160  frgr3vlem2  30201  grpoid  30447  nvmeq0  30585  nvgt0  30601  imsmetlem  30617  nmlnogt0  30724  ip2eqi  30783  hvaddcan2  30998  hvmulcan2  31000  hvaddsub4  31005  hi2eq  31032  pjhtheu  31321  lnopeqi  31935  riesz1  31992  jpi  32197  chcv2  32283  cvp  32302  atnemeq0  32304  brabgaf  32534  fmptcof2  32581  funcnvmpt  32591  nndiffz1  32709  nn0min  32745  sgnneg  32758  xrge0addgt0  32958  lbslsp  33338  ressply1mon1p  33527  fldextrspunlsplem  33660  smatrcl  33773  lmlim  33924  carsggect  34296  eulerpartlems  34338  eulerpartlemgh  34356  ballotlemfc0  34471  ballotlemfcc  34472  signsvfpn  34563  signsvfnn  34564  reprdifc  34605  bnj1280  34997  lfuhgr  35086  satffunlem1lem2  35371  elmrsubrn  35488  msubff1  35524  fz0n  35694  imageval  35894  nn0prpwlem  36286  filnetlem4  36345  onsuct0  36405  onint1  36413  dissneqlem  37304  fvineqsneu  37375  wl-sbalnae  37526  wl-ax11-lem8  37556  wl-ax11-lem10  37558  sin2h  37580  tan2h  37582  matunitlindflem1  37586  matunitlindflem2  37587  matunitlindf  37588  poimirlem18  37608  poimirlem21  37611  poimirlem24  37614  heicant  37625  mblfinlem3  37629  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  mbfresfi  37636  mbfposadd  37637  itg2addnclem  37641  itg2addnclem2  37642  itg2addnc  37644  itg2gt0cn  37645  itgaddnclem2  37649  ftc1anclem5  37667  areacirclem1  37678  areacirclem4  37681  areacirc  37683  isdmn3  38044  eldmres2  38239  cnvref4  38314  relbrcoss  38410  releldmqs  38622  lcvp  39004  lcv2  39006  lsatnem0  39009  atnem0  39282  cvlsupr2  39307  cvr2N  39376  athgt  39421  2llnmat  39489  pmap11  39727  pmapeq0  39731  2lnat  39749  paddclN  39807  pmapjat1  39818  ltrn2ateq  40145  dihcnvord  41239  dihcnv11  41240  dih0bN  41246  dih0sb  41250  dihlspsnat  41298  dihatexv2  41304  dihglblem6  41305  dochvalr  41322  dochn0nv  41340  djhcvat42  41380  dochsatshp  41416  dochshpsat  41419  dochkrsat2  41421  lcfl5a  41462  lcfl8a  41468  lclkrlem2a  41472  mapdcnvordN  41623  hdmap14lem4a  41836  hgmapeq0  41869  hdmaplkr  41878  hdmapellkr  41879  metakunt15  42178  cxp111d  42338  sn-ltmulgt11d  42452  frlmfielbas  42470  eu6w  42646  rmxycomplete  42888  gicabl  43070  minregex2  43506  ntrneiel  44052  ntrneik4w  44071  ntrneik4  44072  extoimad  44135  radcnvrat  44286  pm14.123b  44398  iotavalb  44402  infxrunb3  45399  climreeq  45590  clim2f  45613  clim2f2  45647  dfodd4  47621  oddprmne2  47677  nnsgrpnmnd  48101  ovmpordxf  48262  eenglngeehlnmlem2  48666  iscnrm3  48874