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  2209  19.21t  2244  19.23t  2248  sbco2  2542  sbco3  2544  sbal1  2559  sbal2  2560  clelab  2906  ceqsralt  3487  csbiebt  3879  prsspwg  4787  ssprss  4788  reusv2lem5  5371  copsex2t  5473  ordtri2  6397  onmindif  6456  fnssresb  6658  fcnvres  6756  foelcdmi  6943  funcnvmpt  6992  funimass5  7051  fmptco  7126  cbvfo  7293  isocnv  7334  isoini  7342  isoselem  7345  riota2df  7396  ovmpodxf  7566  caovcanrd  7620  onmindif2  7809  ordunisuc2  7843  dfom2  7867  frxp2  8145  xpord2pred  8146  xpord3pred  8153  ordge1n0  8484  ondif2  8492  oa00  8549  odi  8569  oeoe  8590  eceqoveq  8825  isfinite2  9271  unfilem1  9278  fodomfib  9301  inficl  9398  dffi3  9404  ordiso2  9490  ordtypelem9  9501  cantnfle  9653  cantnf  9675  wemapwe  9679  rankr1a  9821  bnd2  9898  iscard  9983  domtri2  9997  nnsdomel  9998  cardaleph  10095  dfac12lem2  10150  cfss  10270  axcc3  10443  fodomb  10532  iundom2g  10551  inar1  10787  ltpiord  10899  ordpinq  10955  suplem2pr  11065  enreceq  11078  subeq0  11511  negcon1  11537  subexsub  11659  subeqrev  11663  lesub  11720  ltsub13  11722  subge0  11754  mul0or  11881  mulcan1g  11894  divmuleq  11947  mdiv  12078  ltmuldiv2  12116  lemuldiv2  12123  nn1suc  12282  addltmul  12507  elnnnn0  12574  znn0sub  12668  prime  12705  zbtwnre  12998  xadddi2  13351  supxrbnd  13382  fz1n  13598  fzrev3  13647  fzo0n  13739  fzonlt0  13740  ico01fl0  13882  divfl0  13887  modaddid  13973  modsubdir  14006  om2uzlt2i  14017  hashf1lem1  14522  wrdlenge1n0  14617  pfxccat3a  14809  sgnneg  15175  cnpart  15329  sqrt11  15351  sqrtsq2  15357  absdiflt  15407  absdifle  15408  sqreulem  15449  sqreu  15450  eqsqrtor  15456  clim2  15593  climshft2  15671  isercoll  15757  sumrb  15801  supcvg  15947  prodrblem2  16022  sinbnd  16272  cosbnd  16273  sqrt2irr  16341  dvdscmulr  16378  dvdsmulcr  16379  oddm1even  16437  bitsmod  16530  bitsinv1lem  16535  qredeq  16751  cncongr2  16762  isprm3  16777  prmrp  16807  crth  16873  pcdvdsb  16965  pceq0  16967  unbenlem  17004  ramcl  17125  pwselbasb  17577  pwsle  17582  imasleval  17631  xpsfrnel2  17654  acsfn  17751  ismon2  17827  isepi2  17834  epii  17836  fthsect  18020  fthmon  18022  isipodrs  18629  ipodrsfi  18631  gsumval2a  18789  imasmnd2  18883  grpid  19100  grpidrcan  19128  grpidlcan  19129  grplmulf1o  19137  grpraddf1o  19138  imasgrp2  19179  eqg0subg  19325  ghmeqker  19371  gacan  19433  odmulgeq  19685  pgpssslw  19742  efgsfo  19867  efgred  19876  abladdsub4  19939  subgdmdprd  20164  imasrng  20313  imasring  20472  0ring01eqbi  20695  domneq0r  20886  lspsnss2  21190  znf1o  21765  znfld  21774  znunit  21777  znrrg  21779  iporthcom  21849  ip2eq  21867  obsne0  21939  lindfmm  22041  lindsmm  22042  lsslinds  22045  gsumbagdiaglem  22147  psdmul  22395  matunitlindflem1  22902  matunitlindflem2  22903  matunitlindf  22904  eltg3  23188  eltop  23200  eltop2  23201  eltop3  23202  lmbrf  23486  cncnpi  23504  dfconn2  23645  1stcfb  23671  elptr  23800  xkoccn  23846  txcn  23853  hausdiag  23872  hmeoimaf1o  23997  isfbas  24056  ufileu  24146  alexsubALTlem4  24277  tsmsf1o  24372  ismet2  24560  imasdsf1olem  24600  imasf1oxmet  24602  imasf1omet  24603  xmseq0  24691  imasf1oxms  24716  metucn  24798  nrmmetd  24801  nmgt0  24857  nlmmul0or  24910  xrsxmet  25037  metdseq0  25082  elpi1i  25275  cphsqrtcl2  25415  tcphcph  25466  lmmbrf  25491  caucfil  25512  lmclim  25532  cmsss  25580  srabn  25589  ovolfioo  25696  ovolficc  25697  elovolmr  25705  ovolctb  25719  ovolicc2lem3  25748  mbfmulc2lem  25876  mbfimaopnlem  25884  itg2mulclem  25975  iblrelem  26020  ellimc2  26106  mdegle0  26304  fta1glem2  26396  dgreq0  26492  plydivlem4  26527  plydivex  26528  fta1  26539  quotcan  26540  logeftb  26818  quad2  27074  cubic2  27083  dquartlem1  27086  atandm4  27114  fsumharmonic  27246  wilthlem1  27302  basellem8  27322  mumullem2  27414  fsumdvdsmul  27429  chpchtsum  27453  logfaclbnd  27456  dchrelbas4  27477  lgsne0  27569  lgsqrlem2  27581  lgsdchrval  27588  lgsquadlem1  27614  lgsquadlem2  27615  2sqlem7  27658  addsqrexnreu  27676  dchrisum0lem1  27750  nogt01o  27930  lenlts  27986  addscan1  28257  subseq0d  28368  mulscan2d  28442  mulscan1d  28443  muls0ord  28448  ltmuldivs2wd  28465  onnolt  28529  onlts  28530  om2noseqlt2  28563  zn0subs  28666  bdaypw2n0bndlem  28726  bdayfinbndlem1  28730  trgcgrg  28855  tgcgr4  28871  tgcolg  28894  plngrotlem2  29143  lmiinv  29174  iseqlg  29277  elntg2  29428  lfuhgr  29591  cusgruvtxb  29868  upgrewlkle2  30052  clwwlkn1  30497  eupth2lem3lem3  30696  eupth2lem3lem6  30699  frgr3vlem2  30740  grpoid  30987  nvmeq0  31125  nvgt0  31141  imsmetlem  31157  nmlnogt0  31264  ip2eqi  31323  hvaddcan2  31538  hvmulcan2  31540  hvaddsub4  31545  hi2eq  31572  pjhtheu  31861  lnopeqi  32475  riesz1  32532  jpi  32737  chcv2  32823  cvp  32842  atnemeq0  32844  brabgaf  33066  fmptcof2  33117  nndiffz1  33244  nn0min  33278  xrge0addgt0  33444  rlocisunit  33703  lbslsp  33797  ressply1mon1p  33965  fldextrspunlsplem  34170  smatrcl  34293  lmlim  34444  carsggect  34816  eulerpartlems  34858  eulerpartlemgh  34876  ballotlemfc0  34991  ballotlemfcc  34992  signsvfpn  35080  signsvfnn  35081  reprdifc  35122  bnj1280  35516  fineqvnttrclselem3  35636  satffunlem1lem2  35969  elmrsubrn  36086  msubff1  36122  fz0n  36297  imageval  36494  nn0prpwlem  36928  filnetlem4  36987  onsuct0  37047  onint1  37055  dissneqlem  38081  fvineqsneu  38152  wl-sbalnae  38312  sin2h  38351  tan2h  38353  poimirlem18  38374  poimirlem21  38377  poimirlem24  38380  heicant  38391  mblfinlem3  38395  ovoliunnfl  38398  voliunnfl  38400  volsupnfl  38401  mbfresfi  38402  mbfposadd  38403  itg2addnclem  38407  itg2addnclem2  38408  itg2addnc  38410  itg2gt0cn  38411  itgaddnclem2  38415  ftc1anclem5  38433  areacirclem1  38444  areacirclem4  38447  areacirc  38449  isdmn3  38811  eldmres2  39017  cnvref4  39085  relbrcoss  39271  releldmqs  39478  lcvp  39900  lcv2  39902  lsatnem0  39905  atnem0  40178  cvlsupr2  40203  cvr2N  40271  athgt  40316  2llnmat  40384  pmap11  40622  pmapeq0  40626  2lnat  40644  paddclN  40702  pmapjat1  40713  ltrn2ateq  41040  dihcnvord  42134  dihcnv11  42135  dih0bN  42141  dih0sb  42145  dihlspsnat  42193  dihatexv2  42199  dihglblem6  42200  dochvalr  42217  dochn0nv  42235  djhcvat42  42275  dochsatshp  42311  dochshpsat  42314  dochkrsat2  42316  lcfl5a  42357  lcfl8a  42363  lclkrlem2a  42367  mapdcnvordN  42518  hdmap14lem4a  42731  hgmapeq0  42764  hdmaplkr  42773  hdmapellkr  42774  cxp111d  43204  sn-remul0ord  43270  sn-ltmulgt11d  43349  frlmfielbas  43375  eu6w  43509  rmxycomplete  43745  gicabl  43927  minregex2  44362  ntrneiel  44908  ntrneik4w  44927  ntrneik4  44928  extoimad  44991  radcnvrat  45125  pm14.123b  45237  iotavalb  45241  infxrunb3  46239  climreeq  46430  clim2f  46451  clim2f2  46485  dfodd4  48562  oddprmne2  48618  nnsgrpnmnd  49080  isidom3  49247  ovmpordxf  49256  eenglngeehlnmlem2  49655  iscnrm3  49865  uptrlem1  50123