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  2179  19.21t  2214  19.23t  2218  sbco2  2516  sbco3  2518  sbal1  2533  sbal2  2534  clelab  2881  ceqsralt  3476  csbiebt  3879  prsspwg  4780  ssprss  4781  reusv2lem5  5348  copsex2t  5441  ordtri2  6353  onmindif  6412  fnssresb  6615  fcnvres  6712  foelcdmi  6896  funcnvmpt  6944  funimass5  7002  fmptco  7077  cbvfo  7238  isocnv  7279  isoini  7287  isoselem  7290  riota2df  7341  ovmpodxf  7511  caovcanrd  7564  onmindif2  7755  ordunisuc2  7789  dfom2  7813  frxp2  8089  xpord2pred  8090  xpord3pred  8097  ordge1n0  8424  ondif2  8432  oa00  8489  odi  8509  oeoe  8530  eceqoveq  8764  isfinite2  9203  unfilem1  9210  fodomfib  9234  fodomfibOLD  9236  inficl  9333  dffi3  9339  ordiso2  9425  ordtypelem9  9436  cantnfle  9585  cantnf  9607  wemapwe  9611  rankr1a  9753  bnd2  9810  iscard  9892  domtri2  9906  nnsdomel  9907  cardaleph  10004  dfac12lem2  10060  cfss  10180  axcc3  10353  fodomb  10441  iundom2g  10455  inar1  10691  ltpiord  10803  ordpinq  10859  suplem2pr  10969  enreceq  10982  subeq0  11412  negcon1  11438  subexsub  11560  subeqrev  11564  lesub  11621  ltsub13  11623  subge0  11655  mul0or  11782  mulcan1g  11795  div11OLD  11830  divmuleq  11851  mdiv  11982  ltmuldiv2  12021  lemuldiv2  12028  nn1suc  12172  addltmul  12382  elnnnn0  12449  znn0sub  12543  prime  12578  zbtwnre  12864  xadddi2  13217  supxrbnd  13248  fz1n  13463  fzrev3  13511  fzo0n  13602  fzonlt0  13603  ico01fl0  13744  divfl0  13749  modaddid  13835  modsubdir  13868  om2uzlt2i  13879  hashf1lem1  14383  wrdlenge1n0  14478  pfxccat3a  14666  cnpart  15168  sqrt11  15190  sqrtsq2  15196  absdiflt  15246  absdifle  15247  sqreulem  15288  sqreu  15289  eqsqrtor  15295  clim2  15432  climshft2  15510  isercoll  15596  sumrb  15641  supcvg  15784  prodrblem2  15859  sinbnd  16110  cosbnd  16111  sqrt2irr  16179  dvdscmulr  16216  dvdsmulcr  16217  oddm1even  16275  bitsmod  16368  bitsinv1lem  16373  qredeq  16589  cncongr2  16600  isprm3  16615  prmrp  16644  crth  16710  pcdvdsb  16802  pceq0  16804  unbenlem  16841  ramcl  16962  pwselbasb  17413  pwsle  17418  imasleval  17467  xpsfrnel2  17490  acsfn  17587  ismon2  17663  isepi2  17670  epii  17672  fthsect  17856  fthmon  17858  isipodrs  18465  ipodrsfi  18467  gsumval2a  18615  imasmnd2  18704  grpid  18910  grpidrcan  18938  grpidlcan  18939  grplmulf1o  18948  grpraddf1o  18949  imasgrp2  18990  eqg0subg  19130  ghmeqker  19177  gacan  19239  odmulgeq  19491  pgpssslw  19548  efgsfo  19673  efgred  19682  abladdsub4  19745  subgdmdprd  19970  imasrng  20117  imasring  20271  0ring01eqbi  20470  domneq0r  20662  lspsnss2  20961  znf1o  21511  znfld  21520  znunit  21523  znrrg  21525  iporthcom  21595  ip2eq  21613  obsne0  21685  lindfmm  21787  lindsmm  21788  lsslinds  21791  gsumbagdiaglem  21891  psdmul  22114  eltg3  22911  eltop  22923  eltop2  22924  eltop3  22925  lmbrf  23209  cncnpi  23227  dfconn2  23368  1stcfb  23394  elptr  23522  xkoccn  23568  txcn  23575  hausdiag  23594  hmeoimaf1o  23719  isfbas  23778  ufileu  23868  alexsubALTlem4  23999  tsmsf1o  24094  ismet2  24282  imasdsf1olem  24322  imasf1oxmet  24324  imasf1omet  24325  xmseq0  24413  imasf1oxms  24438  metucn  24520  nrmmetd  24523  nmgt0  24579  nlmmul0or  24632  xrsxmet  24759  metdseq0  24804  elpi1i  25007  cphsqrtcl2  25147  tcphcph  25198  lmmbrf  25223  caucfil  25244  lmclim  25264  cmsss  25312  srabn  25321  ovolfioo  25429  ovolficc  25430  elovolmr  25438  ovolctb  25452  ovolicc2lem3  25481  mbfmulc2lem  25609  mbfimaopnlem  25617  itg2mulclem  25708  iblrelem  25753  ellimc2  25839  mdegle0  26043  fta1glem2  26135  dgreq0  26232  plydivlem4  26265  plydivex  26266  fta1  26277  quotcan  26278  logeftb  26553  quad2  26810  cubic2  26819  dquartlem1  26822  atandm4  26850  fsumharmonic  26983  wilthlem1  27039  basellem8  27059  mumullem2  27151  fsumdvdsmul  27166  chpchtsum  27191  logfaclbnd  27194  dchrelbas4  27215  lgsne0  27307  lgsqrlem2  27319  lgsdchrval  27326  lgsquadlem1  27352  lgsquadlem2  27353  2sqlem7  27396  addsqrexnreu  27414  dchrisum0lem1  27488  nogt01o  27669  lenlts  27725  addscan1  27995  subseq0d  28106  mulscan2d  28180  mulscan1d  28181  muls0ord  28186  ltmuldivs2wd  28203  onnolt  28267  onlts  28268  om2noseqlt2  28301  zn0subs  28404  bdaypw2n0bndlem  28464  bdayfinbndlem1  28468  trgcgrg  28592  tgcgr4  28608  tgcolg  28631  lmiinv  28869  iseqlg  28944  elntg2  29063  cusgruvtxb  29500  upgrewlkle2  29685  clwwlkn1  30121  eupth2lem3lem3  30310  eupth2lem3lem6  30313  frgr3vlem2  30354  grpoid  30600  nvmeq0  30738  nvgt0  30754  imsmetlem  30770  nmlnogt0  30877  ip2eqi  30936  hvaddcan2  31151  hvmulcan2  31153  hvaddsub4  31158  hi2eq  31185  pjhtheu  31474  lnopeqi  32088  riesz1  32145  jpi  32350  chcv2  32436  cvp  32455  atnemeq0  32457  brabgaf  32688  fmptcof2  32739  nndiffz1  32869  nn0min  32904  sgnneg  32917  xrge0addgt0  33102  lbslsp  33462  ressply1mon1p  33653  fldextrspunlsplem  33843  smatrcl  33966  lmlim  34117  carsggect  34488  eulerpartlems  34530  eulerpartlemgh  34548  ballotlemfc0  34663  ballotlemfcc  34664  signsvfpn  34755  signsvfnn  34756  reprdifc  34797  bnj1280  35189  fineqvnttrclselem3  35292  lfuhgr  35325  satffunlem1lem2  35610  elmrsubrn  35727  msubff1  35763  fz0n  35938  imageval  36135  nn0prpwlem  36529  filnetlem4  36588  onsuct0  36648  onint1  36656  dissneqlem  37558  fvineqsneu  37629  wl-sbalnae  37780  sin2h  37824  tan2h  37826  matunitlindflem1  37830  matunitlindflem2  37831  matunitlindf  37832  poimirlem18  37852  poimirlem21  37855  poimirlem24  37858  heicant  37869  mblfinlem3  37873  ovoliunnfl  37876  voliunnfl  37878  volsupnfl  37879  mbfresfi  37880  mbfposadd  37881  itg2addnclem  37885  itg2addnclem2  37886  itg2addnc  37888  itg2gt0cn  37889  itgaddnclem2  37893  ftc1anclem5  37911  areacirclem1  37922  areacirclem4  37925  areacirc  37927  isdmn3  38288  eldmres2  38496  cnvref4  38564  relbrcoss  38750  releldmqs  38957  lcvp  39379  lcv2  39381  lsatnem0  39384  atnem0  39657  cvlsupr2  39682  cvr2N  39750  athgt  39795  2llnmat  39863  pmap11  40101  pmapeq0  40105  2lnat  40123  paddclN  40181  pmapjat1  40192  ltrn2ateq  40519  dihcnvord  41613  dihcnv11  41614  dih0bN  41620  dih0sb  41624  dihlspsnat  41672  dihatexv2  41678  dihglblem6  41679  dochvalr  41696  dochn0nv  41714  djhcvat42  41754  dochsatshp  41790  dochshpsat  41793  dochkrsat2  41795  lcfl5a  41836  lcfl8a  41842  lclkrlem2a  41846  mapdcnvordN  41997  hdmap14lem4a  42210  hgmapeq0  42243  hdmaplkr  42252  hdmapellkr  42253  cxp111d  42675  sn-remul0ord  42741  sn-ltmulgt11d  42807  frlmfielbas  42833  eu6w  42997  rmxycomplete  43237  gicabl  43419  minregex2  43854  ntrneiel  44400  ntrneik4w  44419  ntrneik4  44420  extoimad  44483  radcnvrat  44633  pm14.123b  44745  iotavalb  44749  infxrunb3  45745  climreeq  45936  clim2f  45957  clim2f2  45991  dfodd4  47982  oddprmne2  48038  nnsgrpnmnd  48501  ovmpordxf  48662  eenglngeehlnmlem2  49061  iscnrm3  49274  uptrlem1  49532