Theorem bitr3d 280

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3bitrrd  305  3bitr3d  308  3bitr3rd  309  biass  385  sbcom2  2160  19.21t  2198  19.23t  2202  sbco2  2513  sbco3  2515  sbal1  2531  sbal2  2532  csbiebt  3873  prsspwg  4771  ssprss  4772  reusv2lem5  5346  copsex2t  5437  copsex2gOLD  5439  ordtri2  6338  onmindif  6394  fnssresb  6607  fcnvres  6703  foelcdmi  6888  funimass5  6989  fmptco  7058  cbvfo  7218  isocnv  7258  isoini  7266  isoselem  7269  riota2df  7318  ovmpodxf  7486  caovcanrd  7538  onmindif2  7721  ordunisuc2  7759  dfom2  7783  ordge1n0  8396  ondif2  8404  oa00  8462  odi  8482  oeoe  8502  eceqoveq  8683  isfinite2  9167  unfilem1  9176  fodomfib  9192  inficl  9283  dffi3  9289  ordiso2  9373  ordtypelem9  9384  cantnfle  9529  cantnf  9551  wemapwe  9555  rankr1a  9694  bnd2  9751  iscard  9833  domtri2  9847  nnsdomel  9848  cardaleph  9947  dfac12lem2  10002  cfss  10123  axcc3  10296  fodomb  10384  iundom2g  10398  inar1  10633  ltpiord  10745  ordpinq  10801  suplem2pr  10911  enreceq  10924  subeq0  11349  negcon1  11375  subexsub  11495  subeqrev  11499  lesub  11556  ltsub13  11558  subge0  11590  mul0or  11717  mulcan1g  11730  div11  11763  divmuleq  11782  mdiv  11913  ltmuldiv2  11951  lemuldiv2  11958  nn1suc  12097  addltmul  12311  elnnnn0  12378  znn0sub  12469  prime  12503  zbtwnre  12788  xadddi2  13133  supxrbnd  13164  fz1n  13376  fzrev3  13424  fzo0n  13511  fzonlt0  13512  ico01fl0  13641  divfl0  13646  modsubdir  13762  om2uzlt2i  13773  hashf1lem1  14269  hashf1lem1OLD  14270  wrdlenge1n0  14354  pfxccat3a  14550  cnpart  15051  sqrt11  15074  sqrtsq2  15080  absdiflt  15129  absdifle  15130  sqreulem  15171  sqreu  15172  eqsqrtor  15178  clim2  15313  climshft2  15391  isercoll  15479  sumrb  15525  supcvg  15668  prodrblem2  15741  sinbnd  15989  cosbnd  15990  sqrt2irr  16058  dvdscmulr  16094  dvdsmulcr  16095  oddm1even  16152  bitsmod  16243  bitsinv1lem  16248  qredeq  16460  cncongr2  16471  isprm3  16486  prmrp  16515  crth  16577  pcdvdsb  16668  pceq0  16670  unbenlem  16707  ramcl  16828  pwselbasb  17297  pwsle  17301  imasleval  17350  xpsfrnel2  17373  acsfn  17466  ismon2  17544  isepi2  17551  epii  17553  fthsect  17739  fthmon  17741  isipodrs  18353  ipodrsfi  18355  gsumval2a  18467  imasmnd2  18520  grpid  18712  grpidrcan  18737  grpidlcan  18738  grplmulf1o  18746  imasgrp2  18787  ghmeqker  18958  ghmf1  18960  gacan  19008  odmulgeq  19261  pgpssslw  19316  efgsfo  19441  efgred  19450  abladdsub4  19511  subgdmdprd  19733  imasring  19954  lspsnss2  20374  0ring01eqbi  20651  znf1o  20866  znfld  20875  znunit  20878  znrrg  20880  iporthcom  20947  ip2eq  20965  obsne0  21039  lindfmm  21141  lindsmm  21142  lsslinds  21145  gsumbagdiaglemOLD  21248  gsumbagdiaglem  21251  eltg3  22219  eltop  22231  eltop2  22232  eltop3  22233  lmbrf  22518  cncnpi  22536  dfconn2  22677  1stcfb  22703  elptr  22831  xkoccn  22877  txcn  22884  hausdiag  22903  hmeoimaf1o  23028  isfbas  23087  ufileu  23177  alexsubALTlem4  23308  tsmsf1o  23403  ismet2  23593  imasdsf1olem  23633  imasf1oxmet  23635  imasf1omet  23636  xmseq0  23724  imasf1oxms  23752  metucn  23834  nrmmetd  23837  nmgt0  23893  nlmmul0or  23954  xrsxmet  24079  metdseq0  24124  elpi1i  24316  cphsqrtcl2  24457  tcphcph  24508  lmmbrf  24533  caucfil  24554  lmclim  24574  cmsss  24622  srabn  24631  ovolfioo  24738  ovolficc  24739  elovolmr  24747  ovolctb  24761  ovolicc2lem3  24790  mbfmulc2lem  24918  mbfimaopnlem  24926  itg2mulclem  25018  iblrelem  25062  ellimc2  25148  mdegle0  25349  fta1glem2  25438  dgreq0  25533  plydivlem4  25563  plydivex  25564  fta1  25575  quotcan  25576  logeftb  25846  quad2  26096  cubic2  26105  dquartlem1  26108  atandm4  26136  fsumharmonic  26268  wilthlem1  26324  basellem8  26344  mumullem2  26436  chpchtsum  26474  logfaclbnd  26477  dchrelbas4  26498  lgsne0  26590  lgsqrlem2  26602  lgsdchrval  26609  lgsquadlem1  26635  lgsquadlem2  26636  2sqlem7  26679  addsqrexnreu  26697  dchrisum0lem1  26771  nogt01o  26951  slenlt  27007  trgcgrg  27166  tgcgr4  27182  tgcolg  27205  lmiinv  27443  iseqlg  27518  elntg2  27643  cusgruvtxb  28079  upgrewlkle2  28263  clwwlkn1  28694  eupth2lem3lem3  28883  eupth2lem3lem6  28886  frgr3vlem2  28927  grpoid  29171  nvmeq0  29309  nvgt0  29325  imsmetlem  29341  nmlnogt0  29448  ip2eqi  29507  hvaddcan2  29722  hvmulcan2  29724  hvaddsub4  29729  hi2eq  29756  pjhtheu  30045  lnopeqi  30659  riesz1  30716  jpi  30921  chcv2  31007  cvp  31026  atnemeq0  31028  brabgaf  31235  fmptcof2  31281  funcnvmpt  31291  nndiffz1  31394  nn0min  31421  xrge0addgt0  31587  lbslsp  31869  smatrcl  32044  lmlim  32195  carsggect  32585  eulerpartlems  32627  eulerpartlemgh  32645  ballotlemfc0  32759  ballotlemfcc  32760  sgnneg  32807  signsvfpn  32864  signsvfnn  32865  reprdifc  32907  bnj1280  33299  lfuhgr  33378  satffunlem1lem2  33664  elmrsubrn  33781  msubff1  33817  fz0n  33988  frxp2  34075  xpord2pred  34076  addscan1  34257  imageval  34371  nn0prpwlem  34650  filnetlem4  34709  onsuct0  34769  onint1  34777  dissneqlem  35667  fvineqsneu  35738  wl-sbalnae  35873  wl-ax11-lem8  35899  wl-ax11-lem10  35901  sin2h  35923  tan2h  35925  matunitlindflem1  35929  matunitlindflem2  35930  matunitlindf  35931  poimirlem18  35951  poimirlem21  35954  poimirlem24  35957  heicant  35968  mblfinlem3  35972  ovoliunnfl  35975  voliunnfl  35977  volsupnfl  35978  mbfresfi  35979  mbfposadd  35980  itg2addnclem  35984  itg2addnclem2  35985  itg2addnc  35987  itg2gt0cn  35988  itgaddnclem2  35992  ftc1anclem5  36010  areacirclem1  36021  areacirclem4  36024  areacirc  36026  isdmn3  36388  eldmres2  36591  cnvref4  36667  relbrcoss  36764  releldmqs  36976  lcvp  37358  lcv2  37360  lsatnem0  37363  atnem0  37636  cvlsupr2  37661  cvr2N  37730  athgt  37775  2llnmat  37843  pmap11  38081  pmapeq0  38085  2lnat  38103  paddclN  38161  pmapjat1  38172  ltrn2ateq  38499  dihcnvord  39593  dihcnv11  39594  dih0bN  39600  dih0sb  39604  dihlspsnat  39652  dihatexv2  39658  dihglblem6  39659  dochvalr  39676  dochn0nv  39694  djhcvat42  39734  dochsatshp  39770  dochshpsat  39773  dochkrsat2  39775  lcfl5a  39816  lcfl8a  39822  lclkrlem2a  39826  mapdcnvordN  39977  hdmap14lem4a  40190  hgmapeq0  40223  hdmaplkr  40232  hdmapellkr  40233  metakunt15  40447  frlmfielbas  40536  rmxycomplete  41053  gicabl  41238  minregex2  41516  ntrneiel  42064  ntrneik4w  42083  ntrneik4  42084  extoimad  42148  radcnvrat  42305  pm14.123b  42417  iotavalb  42421  infxrunb3  43351  climreeq  43542  clim2f  43565  clim2f2  43599  dfodd4  45529  oddprmne2  45585  nnsgrpnmnd  45790  ovmpordxf  46092  eenglngeehlnmlem2  46502  iscnrm3  46664