Theorem bitr4d 282

Description: Deduction form of bitr4i 278. (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 223	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 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:  3bitr2d  307  3bitr2rd  308  3bitr4d  311  3bitr4rd  312  bianabs  541  mpbirand  708  sb3b  2481  sbcom3  2511  sbal1  2533  sbal2  2534  2reu4lem  4477  issn  4789  disjprg  5095  reuhypd  5365  snelpwg  5392  ordtri3  6354  ordsssuc  6409  iota1  6472  funbrfv2b  6892  dffn5  6893  feqmptdf  6905  unima  6910  dmfco  6931  fneqeql  6993  f1ompt  7058  dff13  7203  fliftcnv  7260  soisores  7276  isotr  7285  isoini  7287  caovord3  7574  releldm2  7990  fimaproj  8080  brtpos  8180  tpostpos  8191  oe1m  8475  oawordri  8480  oalimcl  8490  omlimcl  8508  omabs  8582  iserd  8665  qliftel  8742  qliftfun  8744  qliftf  8747  ecopovsym  8761  pw2f1olem  9014  mapen  9074  findcard3  9188  tfsnfin2  9268  suppeqfsuppbi  9287  mapfien  9316  supisolem  9382  cantnflem1  9603  wemapwe  9611  rankr1clem  9737  rankr1c  9738  ranklim  9761  r1pwALT  9763  r1pwcl  9764  isfin1-2  10300  isfin1-4  10302  fin71num  10312  axdc3lem2  10366  infinfg  10481  ltmnq  10888  prlem936  10963  ltsosr  11010  ltasr  11016  xrlenlt  11202  ltxrlt  11208  letri3  11223  ne0gt0  11243  subadd  11388  ltsubadd2  11613  lesubadd2  11615  suble  11620  ltsub23  11622  ltaddpos2  11633  ltsubpos  11634  subge02  11658  ltord2  11671  leord2  11672  ltaddsublt  11769  divmul  11804  divmul3  11806  rec11r  11845  ltdiv1  12011  ltdivmul2  12024  ledivmul2  12026  ltrec  12029  ltdiv2  12033  negfi  12096  negiso  12127  nnle1eq1  12180  avgle1  12386  avgle2  12387  avgle  12388  nn0le0eq0  12434  elz2  12511  znnnlt1  12523  zleltp1  12547  difrp  12950  xrltlen  13065  dfle2  13066  xrletri3  13073  xgepnf  13085  xlemnf  13087  qbtwnre  13119  xltnegi  13136  supxrre  13247  infxrre  13257  elioo5  13324  elfz5  13437  elfzm11  13516  predfz  13574  flbi  13741  flbi2  13742  fldiv4lem1div2uz2  13761  fznnfl  13787  zmodid2  13824  2submod  13860  lt2sq  14061  le2sq  14062  sqlecan  14137  bcval5  14246  pfxsuffeqwrdeq  14626  shftfib  15000  mulre  15049  cnpart  15168  01sqrexlem6  15175  sqrmo  15179  elicc4abs  15248  abs2difabs  15263  cau4  15285  limsupgre  15409  clim2  15432  ello1mpt2  15450  lo1resb  15492  o1resb  15494  climeq  15495  climmpt2  15501  isercoll  15596  caucvgb  15608  fsumabs  15729  isumshft  15767  geomulcvg  15804  absefib  16128  dvdsval3  16188  addmulmodb  16197  dvdsabseq  16245  dvdsflip  16249  dvdsssfz1  16250  mod2eq1n2dvds  16279  ndvdsadd  16342  bitscmp  16370  smupvallem  16415  dvdssq  16499  lcmdvds  16540  ncoprmgcdgt1b  16583  isprm3  16615  isprm5  16639  phiprmpw  16708  prmdiv  16717  pc11  16813  pcz  16814  pockthlem  16838  prmreclem2  16850  prmreclem4  16852  prmreclem6  16854  1arith  16860  vdwapun  16907  rami  16948  ramcl  16962  pwsle  17418  ercpbllem  17474  invsym  17691  funcres2c  17832  latnle  18401  grpinvcnv  18941  subgacs  19095  eqger  19112  ghmqusker  19221  gexdvds2  19519  pgpfi1  19529  pgpfi  19539  lsmass  19603  lssnle  19608  lsmdisj3b  19624  lsmhash  19639  ablsubadd  19743  gsumval3lem2  19840  subgdmdprd  19970  pgpfac1lem2  20011  dvdsr02  20313  issubrg3  20538  isdomn3  20653  drngid2  20690  sdrgunit  20734  sdrgacs  20739  lssacs  20923  prmirred  21434  chrdvds  21486  chrcong  21487  chrnzr  21490  znleval  21514  znleval2  21515  cygznlem3  21529  frlmbas  21715  elfilspd  21763  lindfmm  21787  islindf4  21798  islindf5  21799  psrbaglefi  21887  coe1mul2lem1  22214  mdetunilem9  22569  isneip  23054  neiptopnei  23081  lpdifsn  23092  restopnb  23124  restopn2  23126  restdis  23127  restperf  23133  lmbr2  23208  cncls2  23222  cnprest  23238  cnprest2  23239  iscnrm2  23287  ist0-2  23293  ist1-3  23298  ishaus2  23300  cmpfi  23357  dfconn2  23368  1stccnp  23411  subislly  23430  hausmapdom  23449  tx1cn  23558  tx2cn  23559  txcnmpt  23573  txrest  23580  hauseqlcld  23595  tgqtop  23661  qtopcld  23662  ordthmeolem  23750  trfil2  23836  trfil3  23837  trnei  23841  ufildr  23880  fmfg  23898  rnelfm  23902  fmfnfm  23907  elflim  23920  flimrest  23932  cnflf  23951  cnflf2  23952  ptcmplem2  24002  ghmcnp  24064  tsmssubm  24092  iscfilu  24236  xmetgt0  24307  prdsxmetlem  24317  blcomps  24342  blcom  24343  xblpnfps  24344  xblpnf  24345  blpnf  24346  xmeter  24382  setsxms  24428  imasf1obl  24437  stdbdbl  24466  metrest  24473  metuel2  24514  dscopn  24522  xrtgioo  24756  metdstri  24801  cnmpopc  24883  iihalf2  24889  icopnfhmeo  24902  evth2  24920  lmmbr3  25221  iscau3  25239  metcld  25267  cfilucfil3  25281  srabn  25321  rrxmet  25369  minveclem4  25393  evthicc2  25422  ovolgelb  25442  shft2rab  25470  ovolshftlem1  25471  sca2rab  25474  ovolscalem1  25475  ioombl1lem4  25523  mbfmulc2lem  25609  ismbf3d  25616  mbfsup  25626  mbfinf  25627  i1f1lem  25651  i1fmulclem  25664  mbfi1fseqlem4  25680  itg2seq  25704  ditgneg  25819  limcdif  25838  limcnlp  25840  cnplimc  25849  rolle  25955  mvth  25958  dvne0  25977  lhop1lem  25979  itgsubst  26017  mdegle0  26043  deg1leb  26061  deg1le0  26077  q1peqb  26122  coemulhi  26220  dgrlt  26233  plydivlem3  26264  vieta1lem2  26280  aannenlem1  26297  ulmres  26358  reefiso  26419  pilem3  26424  ellogdm  26609  root1eq1  26726  angpieqvdlem  26799  angpieqvdlem2  26800  quad2  26810  1cubr  26813  quart  26832  rlimcnp  26936  wilthlem2  27040  isppw  27085  dvdsflsumcom  27159  fsumvma  27185  logfac2  27189  chpchtsum  27191  dchrmulcl  27221  dchrresb  27231  bclbnd  27252  bposlem1  27256  bposlem5  27260  gausslemma2dlem0c  27330  lgsquadlem1  27352  m1lgs  27360  2lgsoddprmlem2  27381  dchrisumlem3  27463  dchrisum0lem1  27488  ltsval2  27629  noextenddif  27641  lesloe  27727  lestri3  27728  eqcuts  27786  elmade2  27859  ltadds1  27993  negsunif  28056  ltsubs1  28077  ltsubadds2d  28091  mulsproplem12  28128  ltmuls2  28172  ltmuls1d  28174  divmulsw  28194  ltdivmuls2wd  28201  oniso  28272  n0subs  28364  n0lesltp1  28367  elzn0s  28399  avglts1d  28454  avglts2d  28455  bdaypw2n0bndlem  28464  z12sge0  28484  dfz12s2  28489  elreno2  28496  tgjustr  28551  trgcgrg  28592  lnrot1  28700  islnopp  28816  ismidb  28855  islmib  28864  axsegconlem6  29000  axeuclidlem  29040  axcontlem2  29043  axcontlem4  29045  axcontlem12  29053  ausgrusgrb  29243  nb3grpr2  29461  cplgr2v  29510  umgr2v2enb1  29605  crctcsh  29902  clwwlknonwwlknonb  30186  eupth2lems  30318  nmoreltpnf  30849  isblo2  30863  nmlnogt0  30877  phoeqi  30937  ubthlem2  30951  hire  31174  normgt0  31207  ho01i  31908  ho02i  31909  hoeq1  31910  hoeq2  31911  nmopreltpnf  31949  adjeq  32015  leop  32203  leopmul2i  32215  pjnormssi  32248  pjimai  32256  jplem1  32348  mddmd2  32389  mdslmd1lem1  32405  mdslmd1lem2  32406  superpos  32434  atnssm0  32456  dmdbr5ati  32502  disjunsn  32673  fcoinvbr  32684  ofpreima  32747  funcnv5mpt  32749  suppiniseg  32768  isoun  32784  fpwrelmapffslem  32814  fpwrelmap  32815  iocinioc2  32862  xrdifh  32863  nndiffz1  32869  sgn3da  32918  xdivmul  33009  cntzsnid  33166  cntrval2  33257  isarchi2  33271  erler  33351  elrsp  33457  lsmsnpridl  33483  lsmssass  33487  r1pid2OLD  33694  esplyind  33744  finexttrb  33835  algextdeglem6  33892  algextdeglem7  33893  smatrcl  33966  rhmpreimacnlem  34054  sqsscirc2  34079  xrmulc1cn  34100  esumfsup  34240  1stmbfm  34430  2ndmbfm  34431  mbfmcnt  34438  eulerpartlems  34530  eulerpartlemd  34536  ballotlemfc0  34663  ballotlemfcc  34664  ballotlemsima  34686  ballotlemfrcn0  34700  reprinfz1  34792  reprdifc  34797  bnj1173  35171  fineqvnttrclse  35293  vonf1owev  35315  zltp1ne  35317  lfuhgr2  35326  erdszelem7  35404  erdszelem9  35406  iscvm  35466  cvmlift3lem4  35529  rexxfr3dALT  35846  fscgr  36287  seglelin  36323  btwnoutside  36332  lineunray  36354  cldbnd  36533  isfne4  36547  fneval  36559  filnetlem4  36588  nndivsub  36664  bj-gabima  37154  dfgcd3  37542  fvineqsneu  37629  wl-sbhbt  37772  wl-sbcom2d  37779  wl-sbalnae  37780  sin2h  37824  cos2h  37825  matunitlindflem1  37830  matunitlindflem2  37831  matunitlindf  37832  ptrest  37833  poimirlem3  37837  poimirlem4  37838  poimirlem22  37856  poimirlem27  37861  mblfinlem3  37873  mblfinlem4  37874  ismblfin  37875  itg2addnclem  37885  itg2addnclem2  37886  itg2gt0cn  37889  iblabsnclem  37897  ftc1anclem6  37912  areacirclem2  37923  areacirclem5  37926  areacirc  37927  mettrifi  37971  drngoi  38165  eldm4  38495  exanres2  38517  disjecxrn  38626  exeupre  38705  brcoss2  38736  br1cossres2  38744  eldmcoss2  38763  eldm1cossres2  38765  brcosscnv2  38777  erimeq2  38977  disjqmap  39041  disjlem19  39118  prter3  39221  islshpat  39356  lsatnle  39383  ellkr2  39430  lshpkr  39456  lkr0f2  39500  lduallkr3  39501  lkreqN  39509  cvrval2  39613  isat3  39646  glbconN  39716  hlrelat5N  39740  cvrval4N  39753  atlt  39776  1cvrco  39811  pmaple  40100  isline2  40113  isline4N  40116  elpaddn0  40139  elpadd2at2  40146  cdlemkid4  41273  dia0  41391  cdlemm10N  41457  dibglbN  41505  dihmeetlem4preN  41645  dochkrshp3  41727  dvh4dimlem  41782  lcfl5  41835  mapdpglem3  42014  mapdheq  42067  hdmap1eq  42140  hdmapval2lem  42170  hdmapoc  42270  hlhillcs  42297  lcmineqlem18  42379  dvdsexpb  42668  renegadd  42705  resubadd  42712  redivmuld  42778  mulgt0b1d  42805  fsuppssind  42914  fz1eqin  43089  diophin  43092  jm2.19  43313  rmxdiophlem  43335  pw2f1ocnv  43357  wepwsolem  43362  gicabl  43419  idomodle  43511  onsupmaxb  43559  cantnf2  43645  tfsconcatb0  43664  tfsnfin  43672  ntrclsfveq2  44380  ntrclsss  44382  ntrclsk4  44391  extoimad  44483  radcnvrat  44633  bcc0  44659  supxrre3rnmpt  45750  clim2f  45957  clim2f2  45991  liminfreuzlem  46123  liminfltlem  46125  xlimmnflimsup2  46173  xlimpnfliminf2  46182  xlimlimsupleliminf  46184  opprb  47354  funbrafv2b  47482  dfafn5a  47483  leaddsuble  47620  mod2addne  47687  iccpartgtprec  47743  flsqrt  47916  dfeven2  47972  dfodd3  47973  lindslinindimp2lem4  48784  snlindsntor  48794  regt1loggt0  48859  elbigo2  48875  elbigolo1  48880  fldivexpfllog2  48888  nnlog2ge0lt1  48889  blenpw2m1  48902  naryfvalelwrdf  48956  isprsd  49277  resccatlem  49395  functhinclem1  49766  thincciso  49775  thinciso  49792  isinito2lem  49820  fulltermc  49833  prstcprs  49882  oduoppcciso  49888  postc  49891  lmdran  49993  cmdlan  49994