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  2212  19.21t  2246  19.23t  2250  sbco2  2543  sbco3  2545  sbal1  2560  sbal2  2561  clelab  2908  ceqsralt  3488  csbiebt  3880  prsspwg  4782  ssprss  4783  reusv2lem5  5368  copsex2t  5468  ordtri2  6416  onmindif  6475  fnssresb  6683  fcnvres  6781  foelcdmi  6969  funcnvmpt  7018  funimass5  7077  fmptco  7154  cbvfo  7320  isocnv  7361  isoini  7369  isoselem  7372  riota2df  7423  ovmpodxf  7594  caovcanrd  7648  onmindif2  7845  ordunisuc2  7879  dfom2  7903  frxp2  8188  xpord2pred  8189  xpord3pred  8196  ordge1n0  8530  ondif2  8538  oa00  8595  odi  8615  oeoe  8636  eceqoveq  8871  isfinite2  9318  unfilem1  9325  fodomfib  9348  inficl  9444  dffi3  9450  ordiso2  9536  ordtypelem9  9547  cantnfle  9699  cantnf  9721  wemapwe  9725  rankr1a  9875  bnd2  9983  iscard  10083  domtri2  10097  nnsdomel  10098  cardaleph  10195  dfac12lem2  10250  cfss  10370  axcc3  10543  fodomb  10632  iundom2g  10651  inar1  10887  ltpiord  10999  ordpinq  11055  suplem2pr  11165  enreceq  11178  subeq0  11611  negcon1  11637  subexsub  11761  subeqrev  11765  lesub  11822  ltsub13  11824  subge0  11856  mul0or  11983  mulcan1g  11996  divmuleq  12049  mdiv  12180  ltmuldiv2  12218  lemuldiv2  12225  nn1suc  12384  addltmul  12609  elnnnn0  12676  znn0sub  12770  prime  12807  zbtwnre  13100  xadddi2  13454  supxrbnd  13485  fz1n  13702  fzrev3  13751  fzo0n  13843  fzonlt0  13844  ico01fl0  13986  divfl0  13991  modaddid  14077  modsubdir  14110  om2uzlt2i  14121  hashf1lem1  14627  wrdlenge1n0  14722  pfxccat3a  14915  sgnneg  15282  cnpart  15436  sqrt11  15458  sqrtsq2  15464  absdiflt  15514  absdifle  15515  sqreulem  15556  sqreu  15557  eqsqrtor  15563  clim2  15700  climshft2  15778  isercoll  15864  sumrb  15908  supcvg  16054  prodrblem2  16127  sinbnd  16377  cosbnd  16378  sqrt2irr  16446  dvdscmulr  16483  dvdsmulcr  16484  oddm1even  16542  bitsmod  16635  bitsinv1lem  16640  qredeq  16861  cncongr2  16872  isprm3  16887  prmrp  16917  crth  16984  pcdvdsb  17076  pceq0  17078  unbenlem  17115  ramcl  17236  pwselbasb  17688  pwsle  17693  imasleval  17742  xpsfrnel2  17765  acsfn  17862  ismon2  17938  isepi2  17945  epii  17947  fthsect  18131  fthmon  18133  isipodrs  18740  ipodrsfi  18742  imasmgm2  18892  gsumval2a  18903  imasmnd2  18997  grpid  19215  grpidrcan  19243  grpidlcan  19244  grplmulf1o  19252  grpraddf1o  19253  imasgrp2  19294  eqg0subg  19440  ghmeqker  19486  gacan  19549  odmulgeq  19801  pgpssslw  19858  efgsfo  19983  efgred  19992  abladdsub4  20055  subgdmdprd  20280  imasrng  20429  imasring  20590  0ring01eqbi  20814  domneq0r  21005  lspsnss2  21310  znf1o  21887  znfld  21896  znunit  21899  znrrg  21901  iporthcom  21971  ip2eq  21989  obsne0  22061  lindfmm  22163  lindsmm  22164  lsslinds  22167  gsumbagdiaglem  22269  psdmul  22517  matunitlindflem1  23024  matunitlindflem2  23025  matunitlindf  23026  eltg3  23310  eltop  23322  eltop2  23323  eltop3  23324  lmbrf  23608  cncnpi  23626  dfconn2  23767  1stcfb  23793  elptr  23922  xkoccn  23968  txcn  23975  hausdiag  23994  hmeoimaf1o  24119  isfbas  24178  ufileu  24268  alexsubALTlem4  24399  tsmsf1o  24494  ismet2  24682  imasdsf1olem  24722  imasf1oxmet  24724  imasf1omet  24725  xmseq0  24813  imasf1oxms  24838  metucn  24920  nrmmetd  24923  nmgt0  24979  nlmmul0or  25032  xrsxmet  25159  metdseq0  25204  elpi1i  25397  cphsqrtcl2  25537  tcphcph  25588  lmmbrf  25613  caucfil  25634  lmclim  25654  cmsss  25702  srabn  25711  ovolfioo  25818  ovolficc  25819  elovolmr  25827  ovolctb  25841  ovolicc2lem3  25870  mbfmulc2lem  25998  mbfimaopnlem  26006  itg2mulclem  26097  iblrelem  26141  ellimc2  26227  mdegle0  26425  fta1glem2  26517  dgreq0  26614  plydivlem4  26647  plydivex  26648  fta1  26659  quotcan  26662  logeftb  26941  quad2  27197  cubic2  27206  dquartlem1  27209  atandm4  27237  fsumharmonic  27369  wilthlem1  27425  basellem8  27445  mumullem2  27537  fsumdvdsmul  27552  chpchtsum  27576  logfaclbnd  27579  dchrelbas4  27600  lgsne0  27692  lgsqrlem2  27704  lgsdchrval  27711  lgsquadlem1  27737  lgsquadlem2  27738  2sqlem7  27781  addsqrexnreu  27799  dchrisum0lem1  27873  flt4ALT  28022  nogt01o  28083  lenlts  28139  addscan1  28410  subseq0d  28521  mulscan2d  28595  mulscan1d  28596  muls0ord  28601  ltmuldivs2wd  28618  onnolt  28682  onlts  28683  om2noseqlt2  28716  zn0subs  28819  bdaypw2n0bndlem  28879  bdayfinbndlem1  28883  trgcgrg  29008  tgcgr4  29024  tgcolg  29047  plngrotlem2  29296  lmiinv  29327  iseqlg  29442  elntg2  29593  lfuhgr  29756  cusgruvtxb  30033  upgrewlkle2  30217  clwwlkn1  30662  eupth2lem3lem3  30861  eupth2lem3lem6  30864  frgr3vlem2  30905  grpoid  31152  nvmeq0  31290  nvgt0  31306  imsmetlem  31322  nmlnogt0  31429  ip2eqi  31488  hvaddcan2  31703  hvmulcan2  31705  hvaddsub4  31710  hi2eq  31737  pjhtheu  32026  lnopeqi  32640  riesz1  32697  jpi  32902  chcv2  32988  cvp  33007  atnemeq0  33009  brabgaf  33272  fmptcof2  33323  nndiffz1  33448  nn0min  33482  xrge0addgt0  33648  rlocisunit  33907  lbslsp  34002  ressply1mon1p  34170  fldextrspunlsplem  34375  smatrcl  34498  lmlim  34649  carsggect  35020  eulerpartlems  35062  eulerpartlemgh  35080  ballotlemfc0  35195  ballotlemfcc  35196  signsvfpn  35284  signsvfnn  35285  reprdifc  35326  bnj1280  35720  fineqvnttrclselem3  35891  jltaleph  36026  prconf1acwevd  36048  onprcf1of1ord  36055  satffunlem1lem2  36335  elmrsubrn  36452  msubff1  36488  fz0n  36674  imageval  36870  nn0prpwlem  37288  filnetlem4  37347  onsuct0  37407  onint1  37415  dissneqlem  38455  fvineqsneu  38526  wl-sbalnae  38686  sin2h  38725  tan2h  38727  poimirlem18  38748  poimirlem21  38751  poimirlem24  38754  heicant  38765  mblfinlem3  38769  ovoliunnfl  38772  voliunnfl  38774  volsupnfl  38775  mbfresfi  38776  mbfposadd  38777  itg2addnclem  38781  itg2addnclem2  38782  itg2addnc  38784  itg2gt0cn  38785  itgaddnclem2  38789  ftc1anclem5  38807  areacirclem1  38818  areacirclem4  38821  areacirc  38823  isdmn3  39200  eldmres2  39406  cnvref4  39474  relbrcoss  39660  releldmqs  39867  lcvp  40289  lcv2  40291  lsatnem0  40294  atnem0  40567  cvlsupr2  40592  cvr2N  40660  athgt  40705  2llnmat  40773  pmap11  41011  pmapeq0  41015  2lnat  41033  paddclN  41091  pmapjat1  41102  ltrn2ateq  41429  dihcnvord  42523  dihcnv11  42524  dih0bN  42530  dih0sb  42534  dihlspsnat  42582  dihatexv2  42588  dihglblem6  42589  dochvalr  42606  dochn0nv  42624  djhcvat42  42664  dochsatshp  42700  dochshpsat  42703  dochkrsat2  42705  lcfl5a  42746  lcfl8a  42752  lclkrlem2a  42756  mapdcnvordN  42907  hdmap14lem4a  43120  hgmapeq0  43153  hdmaplkr  43162  hdmapellkr  43163  cxp111d  43586  sn-remul0ord  43652  sn-ltmulgt11d  43731  frlmfielbas  43760  eu6w  43880  rmxycomplete  44117  gicabl  44294  minregex2  44728  ntrneiel  45273  ntrneik4w  45292  ntrneik4  45293  extoimad  45356  radcnvrat  45490  pm14.123b  45601  iotavalb  45605  infxrunb3  46639  climreeq  46830  clim2f  46851  clim2f2  46885  dfodd4  48962  oddprmne2  49018  nnsgrpnmnd  49480  isidom3  49647  ovmpordxf  49656  eenglngeehlnmlem2  50056  iscnrm3  50271  uptrlem1  50531