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  2163  19.21t  2202  19.23t  2206  sbco2  2515  sbco3  2517  sbal1  2533  sbal2  2534  csbiebt  3858  prsspwg  4753  ssprss  4754  reusv2lem5  5320  copsex2t  5400  copsex2gOLD  5402  ordtri2  6286  onmindif  6340  fnssresb  6538  fcnvres  6635  foelrni  6813  funimass5  6914  fmptco  6983  cbvfo  7141  isocnv  7181  isoini  7189  isoselem  7192  riota2df  7236  ovmpodxf  7401  caovcanrd  7453  onmindif2  7634  ordunisuc2  7666  dfom2  7689  ordge1n0  8290  ondif2  8294  oa00  8352  odi  8372  oeoe  8392  eceqoveq  8569  isfinite2  9002  unfilem1  9008  fodomfib  9023  inficl  9114  dffi3  9120  ordiso2  9204  ordtypelem9  9215  cantnfle  9359  cantnf  9381  wemapwe  9385  rankr1a  9525  bnd2  9582  iscard  9664  domtri2  9678  nnsdomel  9679  cardaleph  9776  dfac12lem2  9831  cfss  9952  axcc3  10125  fodomb  10213  iundom2g  10227  inar1  10462  ltpiord  10574  ordpinq  10630  suplem2pr  10740  enreceq  10753  subeq0  11177  negcon1  11203  subexsub  11323  subeqrev  11327  lesub  11384  ltsub13  11386  subge0  11418  mul0or  11545  mulcan1g  11558  div11  11591  divmuleq  11610  mdiv  11741  ltmuldiv2  11779  lemuldiv2  11786  nn1suc  11925  addltmul  12139  elnnnn0  12206  znn0sub  12297  prime  12331  zbtwnre  12615  xadddi2  12960  supxrbnd  12991  fz1n  13203  fzrev3  13251  fzo0n  13337  fzonlt0  13338  ico01fl0  13467  divfl0  13472  modsubdir  13588  om2uzlt2i  13599  hashf1lem1  14096  hashf1lem1OLD  14097  wrdlenge1n0  14181  pfxccat3a  14379  cnpart  14879  sqrt11  14902  sqrtsq2  14908  absdiflt  14957  absdifle  14958  sqreulem  14999  sqreu  15000  eqsqrtor  15006  clim2  15141  climshft2  15219  isercoll  15307  sumrb  15353  supcvg  15496  prodrblem2  15569  sinbnd  15817  cosbnd  15818  sqrt2irr  15886  dvdscmulr  15922  dvdsmulcr  15923  oddm1even  15980  bitsmod  16071  bitsinv1lem  16076  qredeq  16290  cncongr2  16301  isprm3  16316  prmrp  16345  crth  16407  pcdvdsb  16498  pceq0  16500  unbenlem  16537  ramcl  16658  pwselbasb  17116  pwsle  17120  imasleval  17169  xpsfrnel2  17192  acsfn  17285  ismon2  17363  isepi2  17370  epii  17372  fthsect  17557  fthmon  17559  isipodrs  18170  ipodrsfi  18172  gsumval2a  18284  imasmnd2  18337  grpid  18530  grpidrcan  18555  grpidlcan  18556  grplmulf1o  18564  imasgrp2  18605  ghmeqker  18776  ghmf1  18778  gacan  18826  odmulgeq  19079  pgpssslw  19134  efgsfo  19260  efgred  19269  abladdsub4  19330  subgdmdprd  19552  imasring  19773  lspsnss2  20182  0ring01eqbi  20457  znf1o  20671  znfld  20680  znunit  20683  znrrg  20685  iporthcom  20752  ip2eq  20770  obsne0  20842  lindfmm  20944  lindsmm  20945  lsslinds  20948  gsumbagdiaglemOLD  21051  gsumbagdiaglem  21054  eltg3  22020  eltop  22032  eltop2  22033  eltop3  22034  lmbrf  22319  cncnpi  22337  dfconn2  22478  1stcfb  22504  elptr  22632  xkoccn  22678  txcn  22685  hausdiag  22704  hmeoimaf1o  22829  isfbas  22888  ufileu  22978  alexsubALTlem4  23109  tsmsf1o  23204  ismet2  23394  imasdsf1olem  23434  imasf1oxmet  23436  imasf1omet  23437  xmseq0  23525  imasf1oxms  23551  metucn  23633  nrmmetd  23636  nmgt0  23692  nlmmul0or  23753  xrsxmet  23878  metdseq0  23923  elpi1i  24115  cphsqrtcl2  24255  tcphcph  24306  lmmbrf  24331  caucfil  24352  lmclim  24372  cmsss  24420  srabn  24429  ovolfioo  24536  ovolficc  24537  elovolmr  24545  ovolctb  24559  ovolicc2lem3  24588  mbfmulc2lem  24716  mbfimaopnlem  24724  itg2mulclem  24816  iblrelem  24860  ellimc2  24946  mdegle0  25147  fta1glem2  25236  dgreq0  25331  plydivlem4  25361  plydivex  25362  fta1  25373  quotcan  25374  logeftb  25644  quad2  25894  cubic2  25903  dquartlem1  25906  atandm4  25934  fsumharmonic  26066  wilthlem1  26122  basellem8  26142  mumullem2  26234  chpchtsum  26272  logfaclbnd  26275  dchrelbas4  26296  lgsne0  26388  lgsqrlem2  26400  lgsdchrval  26407  lgsquadlem1  26433  lgsquadlem2  26434  2sqlem7  26477  addsqrexnreu  26495  dchrisum0lem1  26569  trgcgrg  26780  tgcgr4  26796  tgcolg  26819  lmiinv  27057  iseqlg  27132  elntg2  27256  cusgruvtxb  27692  upgrewlkle2  27876  clwwlkn1  28306  eupth2lem3lem3  28495  eupth2lem3lem6  28498  frgr3vlem2  28539  grpoid  28783  nvmeq0  28921  nvgt0  28937  imsmetlem  28953  nmlnogt0  29060  ip2eqi  29119  hvaddcan2  29334  hvmulcan2  29336  hvaddsub4  29341  hi2eq  29368  pjhtheu  29657  lnopeqi  30271  riesz1  30328  jpi  30533  chcv2  30619  cvp  30638  atnemeq0  30640  brabgaf  30849  fmptcof2  30896  funcnvmpt  30906  nndiffz1  31009  nn0min  31036  xrge0addgt0  31202  lbslsp  31474  smatrcl  31648  lmlim  31799  carsggect  32185  eulerpartlems  32227  eulerpartlemgh  32245  ballotlemfc0  32359  ballotlemfcc  32360  sgnneg  32407  signsvfpn  32464  signsvfnn  32465  reprdifc  32507  bnj1280  32900  lfuhgr  32979  satffunlem1lem2  33265  elmrsubrn  33382  msubff1  33418  fz0n  33602  frxp2  33718  xpord2pred  33719  nogt01o  33826  slenlt  33882  imageval  34159  nn0prpwlem  34438  filnetlem4  34497  onsuct0  34557  onint1  34565  dissneqlem  35438  fvineqsneu  35509  wl-sbalnae  35644  wl-ax11-lem8  35670  wl-ax11-lem10  35672  sin2h  35694  tan2h  35696  matunitlindflem1  35700  matunitlindflem2  35701  matunitlindf  35702  poimirlem18  35722  poimirlem21  35725  poimirlem24  35728  heicant  35739  mblfinlem3  35743  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  mbfresfi  35750  mbfposadd  35751  itg2addnclem  35755  itg2addnclem2  35756  itg2addnc  35758  itg2gt0cn  35759  itgaddnclem2  35763  ftc1anclem5  35781  areacirclem1  35792  areacirclem4  35795  areacirc  35797  isdmn3  36159  eldmres2  36337  relbrcoss  36491  releldmqs  36697  lcvp  36981  lcv2  36983  lsatnem0  36986  atnem0  37259  cvlsupr2  37284  cvr2N  37352  athgt  37397  2llnmat  37465  pmap11  37703  pmapeq0  37707  2lnat  37725  paddclN  37783  pmapjat1  37794  ltrn2ateq  38121  dihcnvord  39215  dihcnv11  39216  dih0bN  39222  dih0sb  39226  dihlspsnat  39274  dihatexv2  39280  dihglblem6  39281  dochvalr  39298  dochn0nv  39316  djhcvat42  39356  dochsatshp  39392  dochshpsat  39395  dochkrsat2  39397  lcfl5a  39438  lcfl8a  39444  lclkrlem2a  39448  mapdcnvordN  39599  hdmap14lem4a  39812  hgmapeq0  39845  hdmaplkr  39854  hdmapellkr  39855  metakunt15  40067  frlmfielbas  40157  rmxycomplete  40655  gicabl  40840  ntrneiel  41580  ntrneik4w  41599  ntrneik4  41600  extoimad  41664  radcnvrat  41821  pm14.123b  41933  iotavalb  41937  infxrunb3  42854  climreeq  43044  clim2f  43067  clim2f2  43101  dfodd4  44999  oddprmne2  45055  nnsgrpnmnd  45260  ovmpordxf  45562  eenglngeehlnmlem2  45972  iscnrm3  46134