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  707  sb3b  2475  sbcom3  2505  sbal1  2527  sbal2  2528  2reu4lem  4488  issn  4799  disjprg  5106  reuhypd  5377  snelpwg  5405  ordtri3  6371  ordsssuc  6426  iota1  6491  funbrfv2b  6921  dffn5  6922  feqmptdf  6934  unima  6939  dmfco  6960  fneqeql  7021  f1ompt  7086  dff13  7232  fliftcnv  7289  soisores  7305  isotr  7314  isoini  7316  caovord3  7605  releldm2  8025  fimaproj  8117  brtpos  8217  tpostpos  8228  oe1m  8512  oawordri  8517  oalimcl  8527  omlimcl  8545  omabs  8618  iserd  8700  qliftel  8776  qliftfun  8778  qliftf  8781  ecopovsym  8795  pw2f1olem  9050  mapen  9111  findcard3  9236  suppeqfsuppbi  9337  mapfien  9366  supisolem  9432  cantnflem1  9649  wemapwe  9657  rankr1clem  9780  rankr1c  9781  ranklim  9804  r1pwALT  9806  r1pwcl  9807  isfin1-2  10345  isfin1-4  10347  fin71num  10357  axdc3lem2  10411  ltmnq  10932  prlem936  11007  ltsosr  11054  ltasr  11060  xrlenlt  11246  ltxrlt  11251  letri3  11266  ne0gt0  11286  subadd  11431  ltsubadd2  11656  lesubadd2  11658  suble  11663  ltsub23  11665  ltaddpos2  11676  ltsubpos  11677  subge02  11701  ltord2  11714  leord2  11715  ltaddsublt  11812  divmul  11847  divmul3  11849  rec11r  11888  ltdiv1  12054  ltdivmul2  12067  ledivmul2  12069  ltrec  12072  ltdiv2  12076  negfi  12139  negiso  12170  nnle1eq1  12223  avgle1  12429  avgle2  12430  avgle  12431  nn0le0eq0  12477  elz2  12554  znnnlt1  12567  zleltp1  12591  difrp  12998  xrltlen  13113  dfle2  13114  xrletri3  13121  xgepnf  13132  xlemnf  13134  qbtwnre  13166  xltnegi  13183  supxrre  13294  infxrre  13304  elioo5  13371  elfz5  13484  elfzm11  13563  predfz  13621  flbi  13785  flbi2  13786  fldiv4lem1div2uz2  13805  fznnfl  13831  zmodid2  13868  2submod  13904  lt2sq  14105  le2sq  14106  sqlecan  14181  bcval5  14290  pfxsuffeqwrdeq  14670  shftfib  15045  mulre  15094  cnpart  15213  01sqrexlem6  15220  sqrmo  15224  elicc4abs  15293  abs2difabs  15308  cau4  15330  limsupgre  15454  clim2  15477  ello1mpt2  15495  lo1resb  15537  o1resb  15539  climeq  15540  climmpt2  15546  isercoll  15641  caucvgb  15653  fsumabs  15774  isumshft  15812  geomulcvg  15849  absefib  16173  dvdsval3  16233  addmulmodb  16242  dvdsabseq  16290  dvdsflip  16294  dvdsssfz1  16295  mod2eq1n2dvds  16324  ndvdsadd  16387  bitscmp  16415  smupvallem  16460  dvdssq  16544  lcmdvds  16585  ncoprmgcdgt1b  16628  isprm3  16660  isprm5  16684  phiprmpw  16753  prmdiv  16762  pc11  16858  pcz  16859  pockthlem  16883  prmreclem2  16895  prmreclem4  16897  prmreclem6  16899  1arith  16905  vdwapun  16952  rami  16993  ramcl  17007  pwsle  17462  ercpbllem  17518  invsym  17731  funcres2c  17872  latnle  18439  grpinvcnv  18945  subgacs  19100  eqger  19117  ghmqusker  19226  gexdvds2  19522  pgpfi1  19532  pgpfi  19542  lsmass  19606  lssnle  19611  lsmdisj3b  19627  lsmhash  19642  ablsubadd  19746  gsumval3lem2  19843  subgdmdprd  19973  pgpfac1lem2  20014  dvdsr02  20288  issubrg3  20516  isdomn3  20631  drngid2  20668  sdrgunit  20712  sdrgacs  20717  lssacs  20880  prmirred  21391  chrdvds  21443  chrcong  21444  chrnzr  21447  znleval  21471  znleval2  21472  cygznlem3  21486  frlmbas  21671  elfilspd  21719  lindfmm  21743  islindf4  21754  islindf5  21755  psrbaglefi  21842  coe1mul2lem1  22160  mdetunilem9  22514  isneip  22999  neiptopnei  23026  lpdifsn  23037  restopnb  23069  restopn2  23071  restdis  23072  restperf  23078  lmbr2  23153  cncls2  23167  cnprest  23183  cnprest2  23184  iscnrm2  23232  ist0-2  23238  ist1-3  23243  ishaus2  23245  cmpfi  23302  dfconn2  23313  1stccnp  23356  subislly  23375  hausmapdom  23394  tx1cn  23503  tx2cn  23504  txcnmpt  23518  txrest  23525  hauseqlcld  23540  tgqtop  23606  qtopcld  23607  ordthmeolem  23695  trfil2  23781  trfil3  23782  trnei  23786  ufildr  23825  fmfg  23843  rnelfm  23847  fmfnfm  23852  elflim  23865  flimrest  23877  cnflf  23896  cnflf2  23897  ptcmplem2  23947  ghmcnp  24009  tsmssubm  24037  iscfilu  24182  xmetgt0  24253  prdsxmetlem  24263  blcomps  24288  blcom  24289  xblpnfps  24290  xblpnf  24291  blpnf  24292  xmeter  24328  setsxms  24374  imasf1obl  24383  stdbdbl  24412  metrest  24419  metuel2  24460  dscopn  24468  xrtgioo  24702  metdstri  24747  cnmpopc  24829  iihalf2  24835  icopnfhmeo  24848  evth2  24866  lmmbr3  25167  iscau3  25185  metcld  25213  cfilucfil3  25227  srabn  25267  rrxmet  25315  minveclem4  25339  evthicc2  25368  ovolgelb  25388  shft2rab  25416  ovolshftlem1  25417  sca2rab  25420  ovolscalem1  25421  ioombl1lem4  25469  mbfmulc2lem  25555  ismbf3d  25562  mbfsup  25572  mbfinf  25573  i1f1lem  25597  i1fmulclem  25610  mbfi1fseqlem4  25626  itg2seq  25650  ditgneg  25765  limcdif  25784  limcnlp  25786  cnplimc  25795  rolle  25901  mvth  25904  dvne0  25923  lhop1lem  25925  itgsubst  25963  mdegle0  25989  deg1leb  26007  deg1le0  26023  q1peqb  26068  coemulhi  26166  dgrlt  26179  plydivlem3  26210  vieta1lem2  26226  aannenlem1  26243  ulmres  26304  reefiso  26365  pilem3  26370  ellogdm  26555  root1eq1  26672  angpieqvdlem  26745  angpieqvdlem2  26746  quad2  26756  1cubr  26759  quart  26778  rlimcnp  26882  wilthlem2  26986  isppw  27031  dvdsflsumcom  27105  fsumvma  27131  logfac2  27135  chpchtsum  27137  dchrmulcl  27167  dchrresb  27177  bclbnd  27198  bposlem1  27202  bposlem5  27206  gausslemma2dlem0c  27276  lgsquadlem1  27298  m1lgs  27306  2lgsoddprmlem2  27327  dchrisumlem3  27409  dchrisum0lem1  27434  sltval2  27575  noextenddif  27587  sleloe  27673  sletri3  27674  eqscut  27724  elmade2  27787  sltadd1  27906  negsunif  27968  sltsub1  27987  sltsubadd2d  28001  mulsproplem12  28037  sltmul2  28081  sltmul1d  28083  divsmulw  28103  sltdivmul2wd  28110  onsiso  28176  n0subs  28260  n0sleltp1  28263  elzn0s  28293  zs12ge0  28349  tgjustr  28408  trgcgrg  28449  lnrot1  28557  islnopp  28673  ismidb  28712  islmib  28721  axsegconlem6  28856  axeuclidlem  28896  axcontlem2  28899  axcontlem4  28901  axcontlem12  28909  ausgrusgrb  29099  nb3grpr2  29317  cplgr2v  29366  umgr2v2enb1  29461  crctcsh  29761  clwwlknonwwlknonb  30042  eupth2lems  30174  nmoreltpnf  30705  isblo2  30719  nmlnogt0  30733  phoeqi  30793  ubthlem2  30807  hire  31030  normgt0  31063  ho01i  31764  ho02i  31765  hoeq1  31766  hoeq2  31767  nmopreltpnf  31805  adjeq  31871  leop  32059  leopmul2i  32071  pjnormssi  32104  pjimai  32112  jplem1  32204  mddmd2  32245  mdslmd1lem1  32261  mdslmd1lem2  32262  superpos  32290  atnssm0  32312  dmdbr5ati  32358  disjunsn  32530  fcoinvbr  32541  ofpreima  32596  funcnv5mpt  32599  suppiniseg  32616  isoun  32632  fpwrelmapffslem  32662  fpwrelmap  32663  iocinioc2  32709  xrdifh  32710  nndiffz1  32716  sgn3da  32766  xdivmul  32852  cntzsnid  33016  cntrval2  33135  isarchi2  33146  erler  33223  elrsp  33350  lsmsnpridl  33376  lsmssass  33380  r1pid2OLD  33581  finexttrb  33667  algextdeglem6  33719  algextdeglem7  33720  smatrcl  33793  rhmpreimacnlem  33881  sqsscirc2  33906  xrmulc1cn  33927  esumfsup  34067  1stmbfm  34258  2ndmbfm  34259  mbfmcnt  34266  eulerpartlems  34358  eulerpartlemd  34364  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemsima  34514  ballotlemfrcn0  34528  reprinfz1  34620  reprdifc  34625  bnj1173  34999  vonf1owev  35102  zltp1ne  35104  lfuhgr2  35113  erdszelem7  35191  erdszelem9  35193  iscvm  35253  cvmlift3lem4  35316  rexxfr3dALT  35633  fscgr  36075  seglelin  36111  btwnoutside  36120  lineunray  36142  cldbnd  36321  isfne4  36335  fneval  36347  filnetlem4  36376  nndivsub  36452  bj-gabima  36935  dfgcd3  37319  fvineqsneu  37406  wl-sbhbt  37549  wl-sbcom2d  37556  wl-sbalnae  37557  wl-ax11-lem8  37587  sin2h  37611  cos2h  37612  matunitlindflem1  37617  matunitlindflem2  37618  matunitlindf  37619  ptrest  37620  poimirlem3  37624  poimirlem4  37625  poimirlem22  37643  poimirlem27  37648  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  itg2addnclem  37672  itg2addnclem2  37673  itg2gt0cn  37676  iblabsnclem  37684  ftc1anclem6  37699  areacirclem2  37710  areacirclem5  37713  areacirc  37714  mettrifi  37758  drngoi  37952  eldm4  38270  exanres2  38292  disjecxrn  38382  brcoss2  38430  br1cossres2  38438  eldmcoss2  38457  eldm1cossres2  38459  brcosscnv2  38471  erimeq2  38677  disjlem19  38800  prter3  38882  islshpat  39017  lsatnle  39044  ellkr2  39091  lshpkr  39117  lkr0f2  39161  lduallkr3  39162  lkreqN  39170  cvrval2  39274  isat3  39307  glbconN  39377  glbconNOLD  39378  hlrelat5N  39402  cvrval4N  39415  atlt  39438  1cvrco  39473  pmaple  39762  isline2  39775  isline4N  39778  elpaddn0  39801  elpadd2at2  39808  cdlemkid4  40935  dia0  41053  cdlemm10N  41119  dibglbN  41167  dihmeetlem4preN  41307  dochkrshp3  41389  dvh4dimlem  41444  lcfl5  41497  mapdpglem3  41676  mapdheq  41729  hdmap1eq  41802  hdmapval2lem  41832  hdmapoc  41932  hlhillcs  41959  lcmineqlem18  42041  dvdsexpb  42330  renegadd  42367  resubadd  42374  redivmuld  42440  mulgt0b1d  42467  fsuppssind  42588  fz1eqin  42764  diophin  42767  jm2.19  42989  rmxdiophlem  43011  pw2f1ocnv  43033  wepwsolem  43038  gicabl  43095  idomodle  43187  onsupmaxb  43235  cantnf2  43321  tfsconcatb0  43340  tfsnfin  43348  ntrclsfveq2  44057  ntrclsss  44059  ntrclsk4  44068  extoimad  44160  radcnvrat  44310  bcc0  44336  supxrre3rnmpt  45432  clim2f  45641  clim2f2  45675  liminfreuzlem  45807  liminfltlem  45809  xlimmnflimsup2  45857  xlimpnfliminf2  45866  xlimlimsupleliminf  45868  opprb  47036  funbrafv2b  47164  dfafn5a  47165  leaddsuble  47302  mod2addne  47369  iccpartgtprec  47425  flsqrt  47598  dfeven2  47654  dfodd3  47655  lindslinindimp2lem4  48454  snlindsntor  48464  regt1loggt0  48529  elbigo2  48545  elbigolo1  48550  fldivexpfllog2  48558  nnlog2ge0lt1  48559  blenpw2m1  48572  naryfvalelwrdf  48626  isprsd  48947  resccatlem  49066  functhinclem1  49437  thincciso  49446  thinciso  49463  isinito2lem  49491  fulltermc  49504  prstcprs  49553  oduoppcciso  49559  postc  49562  lmdran  49664  cmdlan  49665