Theorem bitr4d 271

Description: Deduction form of bitr4i 267. (Contributed by NM, 30-Jun-1993.)

Hypotheses

Ref	Expression
bitr4d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
bitr4d	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4d

Step	Hyp	Ref	Expression
1		bitr4d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr4d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	2	bicomd 213	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 268	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  3bitr2d  296  3bitr2rd  297  3bitr4d  300  3bitr4rd  301  mpbirand  530  bianabs  924  sbcom3  2411  sbal1  2460  sbal2  2461  issn  4363  disjprg  4648  reuhypd  4895  ordtri3  5759  ordsssuc  5812  iota1  5865  funbrfv2b  6240  dffn5  6241  feqmptdf  6251  dmfco  6272  fneqeql  6325  f1ompt  6382  dff13  6512  fliftcnv  6561  soisores  6577  isotr  6586  isoini  6588  caovord3  6847  releldm2  7218  brtpos  7361  tpostpos  7372  oe1m  7625  oawordri  7630  oalimcl  7640  omlimcl  7658  omabs  7727  iserd  7768  qliftel  7830  qliftfun  7832  qliftf  7835  ecopovsym  7849  pw2f1olem  8064  mapen  8124  suppeqfsuppbi  8289  funsnfsupp  8299  mapfien  8313  supisolem  8379  cantnflem1  8586  wemapwe  8594  rankr1clem  8683  rankr1c  8684  ranklim  8707  r1pwALT  8709  r1pwcl  8710  isfin1-2  9207  isfin1-4  9209  fin71num  9219  axdc3lem2  9273  ltmnq  9794  prlem936  9869  ltsosr  9915  ltasr  9921  xrlenlt  10103  ltxrlt  10108  letri3  10123  ne0gt0  10142  subadd  10284  ltsubadd2  10499  lesubadd2  10501  suble  10506  ltsub23  10508  ltaddpos2  10519  ltsubpos  10520  subge02  10544  ltord2  10557  leord2  10558  ltaddsublt  10654  divmul  10688  divmul3  10690  rec11r  10724  ltdiv1  10887  ltdivmul2  10900  ledivmul2  10902  ltrec  10905  ltdiv2  10909  negfi  10971  negiso  11003  nnle1eq1  11048  avgle1  11272  avgle2  11273  avgle  11274  nn0le0eq0  11321  elz2  11394  znnnlt1  11404  zleltp1  11428  uzin  11720  difrp  11868  xrltlen  11979  dfle2  11980  xrletri3  11985  xgepnf  11996  xlemnf  11998  qbtwnre  12030  xltnegi  12047  supxrre  12157  supxrre1  12160  infxrre  12166  ixxun  12191  elioo5  12231  elfz5  12334  elfzm11  12411  uzsplit  12412  predfz  12464  flbi  12617  flbi2  12618  fldiv4lem1div2uz2  12637  fznnfl  12661  zmodid2  12698  2submod  12731  lt2sq  12937  le2sq  12938  sqlecan  12971  bcval5  13105  shftfib  13812  mulre  13861  cnpart  13980  sqrlem6  13988  sqrmo  13992  elicc4abs  14059  abs2difabs  14074  cau4  14096  limsupgre  14212  clim2  14235  ello12  14247  ello1mpt2  14253  elo12  14258  lo1resb  14295  o1resb  14297  climeq  14298  climmpt2  14304  isercoll  14398  caucvgb  14410  fsumss  14456  fsumabs  14533  isumshft  14571  geomulcvg  14607  fprodss  14678  absefib  14928  dvdsval3  14987  dvdsabseq  15035  dvdsflip  15039  dvdsssfz1  15040  mod2eq1n2dvds  15071  ndvdsadd  15134  bitscmp  15160  smupvallem  15205  dvdssq  15280  lcmdvds  15321  ncoprmgcdgt1b  15364  coprmdvdsOLD  15367  isprm3  15396  isprm5  15419  phiprmpw  15481  prmdiv  15490  pc11  15584  pcz  15585  pockthlem  15609  prmreclem2  15621  prmreclem4  15623  prmreclem6  15625  1arith  15631  vdwapun  15678  ramval  15712  rami  15719  ramcl  15733  pwsle  16152  ercpbllem  16208  invsym  16422  funcres2c  16561  latnle  17085  grpinvcnv  17483  subgacs  17629  eqger  17644  gexdvds2  18000  pgpfi1  18010  pgpfi  18020  lsmass  18083  lssnle  18087  lsmdisj3b  18103  lsmhash  18118  ablsubadd  18217  gsumval3lem2  18307  subgdmdprd  18433  pgpfac1lem2  18474  dvdsr02  18656  drngid2  18763  issubrg3  18808  lssacs  18967  lspsnel5  18995  psrbaglefi  19372  coe1mul2lem1  19637  prmirred  19843  chrdvds  19876  chrcong  19877  chrnzr  19878  znleval  19903  znleval2  19904  cygznlem3  19918  frlmbas  20099  elfilspd  20142  lindfmm  20166  islindf4  20177  islindf5  20178  mdetunilem9  20426  discld  20893  isneip  20909  neiptopnei  20936  lpdifsn  20947  restopnb  20979  restopn2  20981  restdis  20982  restperf  20988  lmbr2  21063  cncls2  21077  cnprest  21093  cnprest2  21094  iscnrm2  21142  ist0-2  21148  cnt0  21150  ist1-3  21153  ishaus2  21155  cmpfi  21211  dfconn2  21222  1stccnp  21265  1stccn  21266  subislly  21284  hausmapdom  21303  kgencn  21359  tx1cn  21412  tx2cn  21413  txcnmpt  21427  txrest  21434  hauseqlcld  21449  tgqtop  21515  qtopcld  21516  qtopcn  21517  ordthmeolem  21604  trfil2  21691  trfil3  21692  trnei  21696  ufildr  21735  fmfg  21753  rnelfm  21757  fmfnfm  21762  elflim  21775  fbflim  21780  flimrest  21787  isflf  21797  cnflf  21806  cnflf2  21807  fclscf  21829  cnfcf  21846  ptcmplem2  21857  ghmcnp  21918  tsmssubm  21946  iscfilu  22092  xmetgt0  22163  prdsxmetlem  22173  elbl2ps  22194  elbl2  22195  blcomps  22198  blcom  22199  xblpnfps  22200  xblpnf  22201  blpnf  22202  xmeter  22238  setsxms  22284  imasf1obl  22293  stdbdbl  22322  metrest  22329  metcn  22348  txmetcn  22353  metuel2  22370  dscopn  22378  xrtgioo  22609  metdstri  22654  cncffvrn  22701  cnmpt2pc  22727  iihalf2  22732  icopnfhmeo  22742  evth2  22759  lmmbr3  23058  iscau3  23076  lmclimf  23102  metcld  23104  cfilucfil3  23117  srabn  23156  rrxmet  23191  minveclem4  23203  evthicc2  23229  ovolfioo  23236  ovolficc  23237  ovolgelb  23248  ovoliun  23273  shft2rab  23276  ovolshftlem1  23277  sca2rab  23280  ovolscalem1  23281  ismbl2  23295  ioombl1lem4  23329  mbfmulc2lem  23414  mbfmax  23416  mbfposr  23419  ismbf3d  23421  mbfaddlem  23427  mbfsup  23431  mbfinf  23432  i1f1lem  23456  i1fmulclem  23469  mbfi1fseqlem4  23485  itg2seq  23509  itg2monolem1  23517  itg2cnlem1  23528  itgfsum  23593  ditgneg  23621  limcdif  23640  limcnlp  23642  cnplimc  23651  rolle  23753  mvth  23755  dvne0  23774  lhop1lem  23776  itgsubst  23812  mdegle0  23837  deg1leb  23855  deg1le0  23871  q1peqb  23914  coemulhi  24010  dgrlt  24022  plydivlem3  24050  vieta1lem2  24066  aannenlem1  24083  ulmres  24142  reefiso  24202  pilem3  24207  ellogdm  24385  root1eq1  24496  angpieqvdlem  24555  angpieqvdlem2  24556  quad2  24566  1cubr  24569  quart  24588  rlimcnp  24692  wilthlem2  24795  isppw  24840  dvdsflsumcom  24914  fsumvma  24938  logfac2  24942  chpchtsum  24944  dchrmulcl  24974  dchreq  24983  dchrresb  24984  bclbnd  25005  bposlem1  25009  bposlem5  25013  lgsneg  25046  gausslemma2dlem0c  25083  lgsquadlem1  25105  lgsquadlem2  25106  m1lgs  25113  2lgsoddprmlem2  25134  dchrisumlem3  25180  dchrisum0lem1  25205  trgcgrg  25410  tgellng  25448  lnrot1  25518  islnopp  25631  ismidb  25670  islmib  25679  isleag  25733  ttgelitv  25763  axsegconlem6  25802  axeuclidlem  25842  axcontlem2  25845  axcontlem4  25847  axcontlem12  25855  ausgrusgrb  26060  nb3grpr2  26285  cplgr2v  26328  umgr2v2enb1  26422  crctcsh  26716  wspthsnwspthsnon  26811  dfconngr1  27048  eupth2lems  27098  nmoreltpnf  27624  isblo2  27638  nmlnogt0  27652  phoeqi  27713  ubthlem2  27727  hire  27951  normgt0  27984  ho01i  28687  ho02i  28688  hoeq1  28689  hoeq2  28690  nmopreltpnf  28728  adjeq  28794  leop  28982  leopmul2i  28994  pjnormssi  29027  pjimai  29035  jplem1  29127  mddmd2  29168  mdslmd1lem1  29184  mdslmd1lem2  29185  superpos  29213  atnssm0  29235  dmdbr5ati  29281  disjunsn  29407  fcoinvbr  29419  ofpreima  29465  funcnv5mpt  29469  isoun  29479  fpwrelmapffslem  29507  fpwrelmap  29508  iocinioc2  29541  xrdifh  29542  nndiffz1  29548  xdivmul  29633  isarchi2  29739  smatrcl  29862  fimaproj  29900  sqsscirc2  29955  xrmulc1cn  29976  ismntoplly  30069  esumfsup  30132  1stmbfm  30322  2ndmbfm  30323  mbfmcnt  30330  eulerpartlems  30422  eulerpartlemd  30428  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemsima  30577  ballotlemfrcn0  30591  sgn3da  30603  reprinfz1  30700  reprdifc  30705  bnj1173  31070  erdszelem7  31179  erdszelem9  31181  iscvm  31241  cvmlift3lem4  31304  sltval2  31809  noextenddif  31821  sleloe  31879  sletri3  31880  fscgr  32187  seglelin  32223  btwnoutside  32232  lineunray  32254  cldbnd  32321  isfne4  32335  fneval  32347  filnetlem4  32376  nndivsub  32456  dfgcd3  33170  wl-sbhbt  33335  wl-sbcom2d  33344  wl-sbalnae  33345  wl-ax11-lem8  33369  sin2h  33399  cos2h  33400  matunitlindflem1  33405  matunitlindflem2  33406  matunitlindf  33407  ptrest  33408  poimirlem3  33412  poimirlem4  33413  poimirlem22  33431  poimirlem27  33436  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2addnclem  33461  itg2addnclem2  33462  itg2gt0cn  33465  iblabsnclem  33473  ftc1anclem6  33490  areacirclem2  33501  areacirclem5  33504  areacirc  33505  cover2  33508  mettrifi  33553  drngoi  33750  eldm4  34037  exanres2  34065  prter3  34167  islshpat  34304  lsatnle  34331  ellkr2  34378  lshpkr  34404  lkr0f2  34448  lduallkr3  34449  lkreqN  34457  cvrval2  34561  isat3  34594  glbconN  34663  hlrelat5N  34687  cvrval4N  34700  atlt  34723  1cvrco  34758  pmaple  35047  isline2  35060  isline4N  35063  elpaddn0  35086  elpadd2at2  35093  cdlemkid4  36222  dia0  36341  cdlemm10N  36407  dibglbN  36455  dihmeetlem4preN  36595  dochkrshp3  36677  dvh4dimlem  36732  lcfl5  36785  mapdpglem3  36964  mapdheq  37017  hdmap1eq  37091  hdmapval2lem  37123  hdmapoc  37223  hlhillcs  37250  fz1eqin  37332  diophin  37336  jm2.19  37560  rmxdiophlem  37582  pw2f1ocnv  37604  wepwsolem  37612  gicabl  37669  sdrgacs  37771  idomodle  37774  isdomn3  37782  ntrclsfveq2  38359  ntrclsss  38361  ntrclsk4  38370  extoimad  38464  radcnvrat  38513  bcc0  38539  unima  39346  supxrre3rnmpt  39656  clim2f  39868  clim2f2  39902  liminfreuzlem  40034  liminfltlem  40036  2reu4a  41189  dfdfat2  41211  funbrafv2b  41239  dfafn5a  41240  leaddsuble  41311  iccpartgtprec  41356  pfxsuffeqwrdeq  41406  flsqrt  41508  dfeven2  41562  dfodd3  41563  lindslinindimp2lem4  42250  snlindsntor  42260  regt1loggt0  42330  elbigo2  42346  elbigolo1  42351  fldivexpfllog2  42359  nnlog2ge0lt1  42360  blenpw2m1  42373