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  2174  19.21t  2207  19.23t  2211  sbco2  2509  sbco3  2511  sbal1  2526  sbal2  2527  clelab  2873  ceqsralt  3473  csbiebt  3882  prsspwg  4777  ssprss  4778  reusv2lem5  5344  copsex2t  5439  ordtri2  6346  onmindif  6405  fnssresb  6608  fcnvres  6705  foelcdmi  6888  funimass5  6993  fmptco  7067  cbvfo  7230  isocnv  7271  isoini  7279  isoselem  7282  riota2df  7333  ovmpodxf  7503  caovcanrd  7556  onmindif2  7747  ordunisuc2  7784  dfom2  7808  frxp2  8084  xpord2pred  8085  xpord3pred  8092  ordge1n0  8419  ondif2  8427  oa00  8484  odi  8504  oeoe  8524  eceqoveq  8756  isfinite2  9203  unfilem1  9212  fodomfib  9238  fodomfibOLD  9240  inficl  9334  dffi3  9340  ordiso2  9426  ordtypelem9  9437  cantnfle  9586  cantnf  9608  wemapwe  9612  rankr1a  9751  bnd2  9808  iscard  9890  domtri2  9904  nnsdomel  9905  cardaleph  10002  dfac12lem2  10058  cfss  10178  axcc3  10351  fodomb  10439  iundom2g  10453  inar1  10688  ltpiord  10800  ordpinq  10856  suplem2pr  10966  enreceq  10979  subeq0  11408  negcon1  11434  subexsub  11556  subeqrev  11560  lesub  11617  ltsub13  11619  subge0  11651  mul0or  11778  mulcan1g  11791  div11OLD  11826  divmuleq  11847  mdiv  11978  ltmuldiv2  12017  lemuldiv2  12024  nn1suc  12168  addltmul  12378  elnnnn0  12445  znn0sub  12540  prime  12575  zbtwnre  12865  xadddi2  13217  supxrbnd  13248  fz1n  13463  fzrev3  13511  fzo0n  13602  fzonlt0  13603  ico01fl0  13741  divfl0  13746  modaddid  13832  modsubdir  13865  om2uzlt2i  13876  hashf1lem1  14380  wrdlenge1n0  14475  pfxccat3a  14662  cnpart  15165  sqrt11  15187  sqrtsq2  15193  absdiflt  15243  absdifle  15244  sqreulem  15285  sqreu  15286  eqsqrtor  15292  clim2  15429  climshft2  15507  isercoll  15593  sumrb  15638  supcvg  15781  prodrblem2  15856  sinbnd  16107  cosbnd  16108  sqrt2irr  16176  dvdscmulr  16213  dvdsmulcr  16214  oddm1even  16272  bitsmod  16365  bitsinv1lem  16370  qredeq  16586  cncongr2  16597  isprm3  16612  prmrp  16641  crth  16707  pcdvdsb  16799  pceq0  16801  unbenlem  16838  ramcl  16959  pwselbasb  17410  pwsle  17414  imasleval  17463  xpsfrnel2  17486  acsfn  17583  ismon2  17659  isepi2  17666  epii  17668  fthsect  17852  fthmon  17854  isipodrs  18461  ipodrsfi  18463  gsumval2a  18577  imasmnd2  18666  grpid  18872  grpidrcan  18900  grpidlcan  18901  grplmulf1o  18910  grpraddf1o  18911  imasgrp2  18952  eqg0subg  19093  ghmeqker  19140  gacan  19202  odmulgeq  19454  pgpssslw  19511  efgsfo  19636  efgred  19645  abladdsub4  19708  subgdmdprd  19933  imasrng  20080  imasring  20233  0ring01eqbi  20435  domneq0r  20627  lspsnss2  20926  znf1o  21476  znfld  21485  znunit  21488  znrrg  21490  iporthcom  21560  ip2eq  21578  obsne0  21650  lindfmm  21752  lindsmm  21753  lsslinds  21756  gsumbagdiaglem  21855  psdmul  22069  eltg3  22865  eltop  22877  eltop2  22878  eltop3  22879  lmbrf  23163  cncnpi  23181  dfconn2  23322  1stcfb  23348  elptr  23476  xkoccn  23522  txcn  23529  hausdiag  23548  hmeoimaf1o  23673  isfbas  23732  ufileu  23822  alexsubALTlem4  23953  tsmsf1o  24048  ismet2  24237  imasdsf1olem  24277  imasf1oxmet  24279  imasf1omet  24280  xmseq0  24368  imasf1oxms  24393  metucn  24475  nrmmetd  24478  nmgt0  24534  nlmmul0or  24587  xrsxmet  24714  metdseq0  24759  elpi1i  24962  cphsqrtcl2  25102  tcphcph  25153  lmmbrf  25178  caucfil  25199  lmclim  25219  cmsss  25267  srabn  25276  ovolfioo  25384  ovolficc  25385  elovolmr  25393  ovolctb  25407  ovolicc2lem3  25436  mbfmulc2lem  25564  mbfimaopnlem  25572  itg2mulclem  25663  iblrelem  25708  ellimc2  25794  mdegle0  25998  fta1glem2  26090  dgreq0  26187  plydivlem4  26220  plydivex  26221  fta1  26232  quotcan  26233  logeftb  26508  quad2  26765  cubic2  26774  dquartlem1  26777  atandm4  26805  fsumharmonic  26938  wilthlem1  26994  basellem8  27014  mumullem2  27106  fsumdvdsmul  27121  chpchtsum  27146  logfaclbnd  27149  dchrelbas4  27170  lgsne0  27262  lgsqrlem2  27274  lgsdchrval  27281  lgsquadlem1  27307  lgsquadlem2  27308  2sqlem7  27351  addsqrexnreu  27369  dchrisum0lem1  27443  nogt01o  27624  slenlt  27680  addscan1  27924  subseq0d  28031  mulscan2d  28105  mulscan1d  28106  muls0ord  28111  sltmuldiv2wd  28128  onnolt  28190  onslt  28191  om2noseqlt2  28217  zn0subs  28314  trgcgrg  28478  tgcgr4  28494  tgcolg  28517  lmiinv  28755  iseqlg  28830  elntg2  28948  cusgruvtxb  29385  upgrewlkle2  29570  clwwlkn1  30003  eupth2lem3lem3  30192  eupth2lem3lem6  30195  frgr3vlem2  30236  grpoid  30482  nvmeq0  30620  nvgt0  30636  imsmetlem  30652  nmlnogt0  30759  ip2eqi  30818  hvaddcan2  31033  hvmulcan2  31035  hvaddsub4  31040  hi2eq  31067  pjhtheu  31356  lnopeqi  31970  riesz1  32027  jpi  32232  chcv2  32318  cvp  32337  atnemeq0  32339  brabgaf  32569  fmptcof2  32614  funcnvmpt  32624  nndiffz1  32742  nn0min  32778  sgnneg  32791  xrge0addgt0  32984  lbslsp  33324  ressply1mon1p  33513  fldextrspunlsplem  33644  smatrcl  33762  lmlim  33913  carsggect  34285  eulerpartlems  34327  eulerpartlemgh  34345  ballotlemfc0  34460  ballotlemfcc  34461  signsvfpn  34552  signsvfnn  34553  reprdifc  34594  bnj1280  34986  lfuhgr  35090  satffunlem1lem2  35375  elmrsubrn  35492  msubff1  35528  fz0n  35703  imageval  35903  nn0prpwlem  36295  filnetlem4  36354  onsuct0  36414  onint1  36422  dissneqlem  37313  fvineqsneu  37384  wl-sbalnae  37535  wl-ax11-lem8  37565  wl-ax11-lem10  37567  sin2h  37589  tan2h  37591  matunitlindflem1  37595  matunitlindflem2  37596  matunitlindf  37597  poimirlem18  37617  poimirlem21  37620  poimirlem24  37623  heicant  37634  mblfinlem3  37638  ovoliunnfl  37641  voliunnfl  37643  volsupnfl  37644  mbfresfi  37645  mbfposadd  37646  itg2addnclem  37650  itg2addnclem2  37651  itg2addnc  37653  itg2gt0cn  37654  itgaddnclem2  37658  ftc1anclem5  37676  areacirclem1  37687  areacirclem4  37690  areacirc  37692  isdmn3  38053  eldmres2  38249  cnvref4  38317  relbrcoss  38422  releldmqs  38635  lcvp  39018  lcv2  39020  lsatnem0  39023  atnem0  39296  cvlsupr2  39321  cvr2N  39390  athgt  39435  2llnmat  39503  pmap11  39741  pmapeq0  39745  2lnat  39763  paddclN  39821  pmapjat1  39832  ltrn2ateq  40159  dihcnvord  41253  dihcnv11  41254  dih0bN  41260  dih0sb  41264  dihlspsnat  41312  dihatexv2  41318  dihglblem6  41319  dochvalr  41336  dochn0nv  41354  djhcvat42  41394  dochsatshp  41430  dochshpsat  41433  dochkrsat2  41435  lcfl5a  41476  lcfl8a  41482  lclkrlem2a  41486  mapdcnvordN  41637  hdmap14lem4a  41850  hgmapeq0  41883  hdmaplkr  41892  hdmapellkr  41893  cxp111d  42315  sn-remul0ord  42381  sn-ltmulgt11d  42447  frlmfielbas  42473  eu6w  42649  rmxycomplete  42890  gicabl  43072  minregex2  43508  ntrneiel  44054  ntrneik4w  44073  ntrneik4  44074  extoimad  44137  radcnvrat  44287  pm14.123b  44399  iotavalb  44403  infxrunb3  45404  climreeq  45595  clim2f  45618  clim2f2  45652  dfodd4  47644  oddprmne2  47700  nnsgrpnmnd  48150  ovmpordxf  48311  eenglngeehlnmlem2  48711  iscnrm3  48924  uptrlem1  49183