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  2176  19.21t  2209  19.23t  2213  sbco2  2511  sbco3  2513  sbal1  2528  sbal2  2529  clelab  2876  ceqsralt  3471  csbiebt  3874  prsspwg  4774  ssprss  4775  reusv2lem5  5342  copsex2t  5435  ordtri2  6347  onmindif  6406  fnssresb  6609  fcnvres  6706  foelcdmi  6889  funimass5  6994  fmptco  7068  cbvfo  7229  isocnv  7270  isoini  7278  isoselem  7281  riota2df  7332  ovmpodxf  7502  caovcanrd  7555  onmindif2  7746  ordunisuc2  7780  dfom2  7804  frxp2  8080  xpord2pred  8081  xpord3pred  8088  ordge1n0  8415  ondif2  8423  oa00  8480  odi  8500  oeoe  8520  eceqoveq  8752  isfinite2  9188  unfilem1  9195  fodomfib  9219  fodomfibOLD  9221  inficl  9315  dffi3  9321  ordiso2  9407  ordtypelem9  9418  cantnfle  9567  cantnf  9589  wemapwe  9593  rankr1a  9735  bnd2  9792  iscard  9874  domtri2  9888  nnsdomel  9889  cardaleph  9986  dfac12lem2  10042  cfss  10162  axcc3  10335  fodomb  10423  iundom2g  10437  inar1  10672  ltpiord  10784  ordpinq  10840  suplem2pr  10950  enreceq  10963  subeq0  11393  negcon1  11419  subexsub  11541  subeqrev  11545  lesub  11602  ltsub13  11604  subge0  11636  mul0or  11763  mulcan1g  11776  div11OLD  11811  divmuleq  11832  mdiv  11963  ltmuldiv2  12002  lemuldiv2  12009  nn1suc  12153  addltmul  12363  elnnnn0  12430  znn0sub  12525  prime  12560  zbtwnre  12850  xadddi2  13202  supxrbnd  13233  fz1n  13448  fzrev3  13496  fzo0n  13587  fzonlt0  13588  ico01fl0  13729  divfl0  13734  modaddid  13820  modsubdir  13853  om2uzlt2i  13864  hashf1lem1  14368  wrdlenge1n0  14463  pfxccat3a  14651  cnpart  15153  sqrt11  15175  sqrtsq2  15181  absdiflt  15231  absdifle  15232  sqreulem  15273  sqreu  15274  eqsqrtor  15280  clim2  15417  climshft2  15495  isercoll  15581  sumrb  15626  supcvg  15769  prodrblem2  15844  sinbnd  16095  cosbnd  16096  sqrt2irr  16164  dvdscmulr  16201  dvdsmulcr  16202  oddm1even  16260  bitsmod  16353  bitsinv1lem  16358  qredeq  16574  cncongr2  16585  isprm3  16600  prmrp  16629  crth  16695  pcdvdsb  16787  pceq0  16789  unbenlem  16826  ramcl  16947  pwselbasb  17398  pwsle  17402  imasleval  17451  xpsfrnel2  17474  acsfn  17571  ismon2  17647  isepi2  17654  epii  17656  fthsect  17840  fthmon  17842  isipodrs  18449  ipodrsfi  18451  gsumval2a  18599  imasmnd2  18688  grpid  18894  grpidrcan  18922  grpidlcan  18923  grplmulf1o  18932  grpraddf1o  18933  imasgrp2  18974  eqg0subg  19114  ghmeqker  19161  gacan  19223  odmulgeq  19475  pgpssslw  19532  efgsfo  19657  efgred  19666  abladdsub4  19729  subgdmdprd  19954  imasrng  20101  imasring  20254  0ring01eqbi  20453  domneq0r  20645  lspsnss2  20944  znf1o  21494  znfld  21503  znunit  21506  znrrg  21508  iporthcom  21578  ip2eq  21596  obsne0  21668  lindfmm  21770  lindsmm  21771  lsslinds  21774  gsumbagdiaglem  21873  psdmul  22087  eltg3  22883  eltop  22895  eltop2  22896  eltop3  22897  lmbrf  23181  cncnpi  23199  dfconn2  23340  1stcfb  23366  elptr  23494  xkoccn  23540  txcn  23547  hausdiag  23566  hmeoimaf1o  23691  isfbas  23750  ufileu  23840  alexsubALTlem4  23971  tsmsf1o  24066  ismet2  24254  imasdsf1olem  24294  imasf1oxmet  24296  imasf1omet  24297  xmseq0  24385  imasf1oxms  24410  metucn  24492  nrmmetd  24495  nmgt0  24551  nlmmul0or  24604  xrsxmet  24731  metdseq0  24776  elpi1i  24979  cphsqrtcl2  25119  tcphcph  25170  lmmbrf  25195  caucfil  25216  lmclim  25236  cmsss  25284  srabn  25293  ovolfioo  25401  ovolficc  25402  elovolmr  25410  ovolctb  25424  ovolicc2lem3  25453  mbfmulc2lem  25581  mbfimaopnlem  25589  itg2mulclem  25680  iblrelem  25725  ellimc2  25811  mdegle0  26015  fta1glem2  26107  dgreq0  26204  plydivlem4  26237  plydivex  26238  fta1  26249  quotcan  26250  logeftb  26525  quad2  26782  cubic2  26791  dquartlem1  26794  atandm4  26822  fsumharmonic  26955  wilthlem1  27011  basellem8  27031  mumullem2  27123  fsumdvdsmul  27138  chpchtsum  27163  logfaclbnd  27166  dchrelbas4  27187  lgsne0  27279  lgsqrlem2  27291  lgsdchrval  27298  lgsquadlem1  27324  lgsquadlem2  27325  2sqlem7  27368  addsqrexnreu  27386  dchrisum0lem1  27460  nogt01o  27641  slenlt  27697  addscan1  27943  subseq0d  28050  mulscan2d  28124  mulscan1d  28125  muls0ord  28130  sltmuldiv2wd  28147  onnolt  28209  onslt  28210  om2noseqlt2  28236  zn0subs  28333  trgcgrg  28499  tgcgr4  28515  tgcolg  28538  lmiinv  28776  iseqlg  28851  elntg2  28970  cusgruvtxb  29407  upgrewlkle2  29592  clwwlkn1  30028  eupth2lem3lem3  30217  eupth2lem3lem6  30220  frgr3vlem2  30261  grpoid  30507  nvmeq0  30645  nvgt0  30661  imsmetlem  30677  nmlnogt0  30784  ip2eqi  30843  hvaddcan2  31058  hvmulcan2  31060  hvaddsub4  31065  hi2eq  31092  pjhtheu  31381  lnopeqi  31995  riesz1  32052  jpi  32257  chcv2  32343  cvp  32362  atnemeq0  32364  brabgaf  32596  fmptcof2  32646  funcnvmpt  32656  nndiffz1  32776  nn0min  32810  sgnneg  32823  xrge0addgt0  33005  lbslsp  33349  ressply1mon1p  33538  fldextrspunlsplem  33693  smatrcl  33816  lmlim  33967  carsggect  34338  eulerpartlems  34380  eulerpartlemgh  34398  ballotlemfc0  34513  ballotlemfcc  34514  signsvfpn  34605  signsvfnn  34606  reprdifc  34647  bnj1280  35039  fineqvnttrclselem3  35150  lfuhgr  35169  satffunlem1lem2  35454  elmrsubrn  35571  msubff1  35607  fz0n  35782  imageval  35979  nn0prpwlem  36373  filnetlem4  36432  onsuct0  36492  onint1  36500  dissneqlem  37391  fvineqsneu  37462  wl-sbalnae  37613  sin2h  37656  tan2h  37658  matunitlindflem1  37662  matunitlindflem2  37663  matunitlindf  37664  poimirlem18  37684  poimirlem21  37687  poimirlem24  37690  heicant  37701  mblfinlem3  37705  ovoliunnfl  37708  voliunnfl  37710  volsupnfl  37711  mbfresfi  37712  mbfposadd  37713  itg2addnclem  37717  itg2addnclem2  37718  itg2addnc  37720  itg2gt0cn  37721  itgaddnclem2  37725  ftc1anclem5  37743  areacirclem1  37754  areacirclem4  37757  areacirc  37759  isdmn3  38120  eldmres2  38320  cnvref4  38388  relbrcoss  38554  releldmqs  38762  lcvp  39145  lcv2  39147  lsatnem0  39150  atnem0  39423  cvlsupr2  39448  cvr2N  39516  athgt  39561  2llnmat  39629  pmap11  39867  pmapeq0  39871  2lnat  39889  paddclN  39947  pmapjat1  39958  ltrn2ateq  40285  dihcnvord  41379  dihcnv11  41380  dih0bN  41386  dih0sb  41390  dihlspsnat  41438  dihatexv2  41444  dihglblem6  41445  dochvalr  41462  dochn0nv  41480  djhcvat42  41520  dochsatshp  41556  dochshpsat  41559  dochkrsat2  41561  lcfl5a  41602  lcfl8a  41608  lclkrlem2a  41612  mapdcnvordN  41763  hdmap14lem4a  41976  hgmapeq0  42009  hdmaplkr  42018  hdmapellkr  42019  cxp111d  42441  sn-remul0ord  42507  sn-ltmulgt11d  42573  frlmfielbas  42599  eu6w  42775  rmxycomplete  43015  gicabl  43197  minregex2  43633  ntrneiel  44179  ntrneik4w  44198  ntrneik4  44199  extoimad  44262  radcnvrat  44412  pm14.123b  44524  iotavalb  44528  infxrunb3  45527  climreeq  45718  clim2f  45739  clim2f2  45773  dfodd4  47764  oddprmne2  47820  nnsgrpnmnd  48283  ovmpordxf  48444  eenglngeehlnmlem2  48844  iscnrm3  49057  uptrlem1  49316