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  2476  sbcom3  2506  sbal1  2528  sbal2  2529  2reu4lem  4471  issn  4783  disjprg  5089  reuhypd  5359  snelpwg  5386  ordtri3  6348  ordsssuc  6403  iota1  6466  funbrfv2b  6885  dffn5  6886  feqmptdf  6898  unima  6903  dmfco  6924  fneqeql  6985  f1ompt  7050  dff13  7194  fliftcnv  7251  soisores  7267  isotr  7276  isoini  7278  caovord3  7565  releldm2  7981  fimaproj  8071  brtpos  8171  tpostpos  8182  oe1m  8466  oawordri  8471  oalimcl  8481  omlimcl  8499  omabs  8572  iserd  8654  qliftel  8730  qliftfun  8732  qliftf  8735  ecopovsym  8749  pw2f1olem  9000  mapen  9060  findcard3  9173  suppeqfsuppbi  9269  mapfien  9298  supisolem  9364  cantnflem1  9585  wemapwe  9593  rankr1clem  9719  rankr1c  9720  ranklim  9743  r1pwALT  9745  r1pwcl  9746  isfin1-2  10282  isfin1-4  10284  fin71num  10294  axdc3lem2  10348  ltmnq  10869  prlem936  10944  ltsosr  10991  ltasr  10997  xrlenlt  11183  ltxrlt  11189  letri3  11204  ne0gt0  11224  subadd  11369  ltsubadd2  11594  lesubadd2  11596  suble  11601  ltsub23  11603  ltaddpos2  11614  ltsubpos  11615  subge02  11639  ltord2  11652  leord2  11653  ltaddsublt  11750  divmul  11785  divmul3  11787  rec11r  11826  ltdiv1  11992  ltdivmul2  12005  ledivmul2  12007  ltrec  12010  ltdiv2  12014  negfi  12077  negiso  12108  nnle1eq1  12161  avgle1  12367  avgle2  12368  avgle  12369  nn0le0eq0  12415  elz2  12492  znnnlt1  12505  zleltp1  12529  difrp  12936  xrltlen  13051  dfle2  13052  xrletri3  13059  xgepnf  13070  xlemnf  13072  qbtwnre  13104  xltnegi  13121  supxrre  13232  infxrre  13242  elioo5  13309  elfz5  13422  elfzm11  13501  predfz  13559  flbi  13726  flbi2  13727  fldiv4lem1div2uz2  13746  fznnfl  13772  zmodid2  13809  2submod  13845  lt2sq  14046  le2sq  14047  sqlecan  14122  bcval5  14231  pfxsuffeqwrdeq  14611  shftfib  14985  mulre  15034  cnpart  15153  01sqrexlem6  15160  sqrmo  15164  elicc4abs  15233  abs2difabs  15248  cau4  15270  limsupgre  15394  clim2  15417  ello1mpt2  15435  lo1resb  15477  o1resb  15479  climeq  15480  climmpt2  15486  isercoll  15581  caucvgb  15593  fsumabs  15714  isumshft  15752  geomulcvg  15789  absefib  16113  dvdsval3  16173  addmulmodb  16182  dvdsabseq  16230  dvdsflip  16234  dvdsssfz1  16235  mod2eq1n2dvds  16264  ndvdsadd  16327  bitscmp  16355  smupvallem  16400  dvdssq  16484  lcmdvds  16525  ncoprmgcdgt1b  16568  isprm3  16600  isprm5  16624  phiprmpw  16693  prmdiv  16702  pc11  16798  pcz  16799  pockthlem  16823  prmreclem2  16835  prmreclem4  16837  prmreclem6  16839  1arith  16845  vdwapun  16892  rami  16933  ramcl  16947  pwsle  17402  ercpbllem  17458  invsym  17675  funcres2c  17816  latnle  18385  grpinvcnv  18925  subgacs  19079  eqger  19096  ghmqusker  19205  gexdvds2  19503  pgpfi1  19513  pgpfi  19523  lsmass  19587  lssnle  19592  lsmdisj3b  19608  lsmhash  19623  ablsubadd  19727  gsumval3lem2  19824  subgdmdprd  19954  pgpfac1lem2  19995  dvdsr02  20296  issubrg3  20521  isdomn3  20636  drngid2  20673  sdrgunit  20717  sdrgacs  20722  lssacs  20906  prmirred  21417  chrdvds  21469  chrcong  21470  chrnzr  21473  znleval  21497  znleval2  21498  cygznlem3  21512  frlmbas  21698  elfilspd  21746  lindfmm  21770  islindf4  21781  islindf5  21782  psrbaglefi  21869  coe1mul2lem1  22187  mdetunilem9  22541  isneip  23026  neiptopnei  23053  lpdifsn  23064  restopnb  23096  restopn2  23098  restdis  23099  restperf  23105  lmbr2  23180  cncls2  23194  cnprest  23210  cnprest2  23211  iscnrm2  23259  ist0-2  23265  ist1-3  23270  ishaus2  23272  cmpfi  23329  dfconn2  23340  1stccnp  23383  subislly  23402  hausmapdom  23421  tx1cn  23530  tx2cn  23531  txcnmpt  23545  txrest  23552  hauseqlcld  23567  tgqtop  23633  qtopcld  23634  ordthmeolem  23722  trfil2  23808  trfil3  23809  trnei  23813  ufildr  23852  fmfg  23870  rnelfm  23874  fmfnfm  23879  elflim  23892  flimrest  23904  cnflf  23923  cnflf2  23924  ptcmplem2  23974  ghmcnp  24036  tsmssubm  24064  iscfilu  24208  xmetgt0  24279  prdsxmetlem  24289  blcomps  24314  blcom  24315  xblpnfps  24316  xblpnf  24317  blpnf  24318  xmeter  24354  setsxms  24400  imasf1obl  24409  stdbdbl  24438  metrest  24445  metuel2  24486  dscopn  24494  xrtgioo  24728  metdstri  24773  cnmpopc  24855  iihalf2  24861  icopnfhmeo  24874  evth2  24892  lmmbr3  25193  iscau3  25211  metcld  25239  cfilucfil3  25253  srabn  25293  rrxmet  25341  minveclem4  25365  evthicc2  25394  ovolgelb  25414  shft2rab  25442  ovolshftlem1  25443  sca2rab  25446  ovolscalem1  25447  ioombl1lem4  25495  mbfmulc2lem  25581  ismbf3d  25588  mbfsup  25598  mbfinf  25599  i1f1lem  25623  i1fmulclem  25636  mbfi1fseqlem4  25652  itg2seq  25676  ditgneg  25791  limcdif  25810  limcnlp  25812  cnplimc  25821  rolle  25927  mvth  25930  dvne0  25949  lhop1lem  25951  itgsubst  25989  mdegle0  26015  deg1leb  26033  deg1le0  26049  q1peqb  26094  coemulhi  26192  dgrlt  26205  plydivlem3  26236  vieta1lem2  26252  aannenlem1  26269  ulmres  26330  reefiso  26391  pilem3  26396  ellogdm  26581  root1eq1  26698  angpieqvdlem  26771  angpieqvdlem2  26772  quad2  26782  1cubr  26785  quart  26804  rlimcnp  26908  wilthlem2  27012  isppw  27057  dvdsflsumcom  27131  fsumvma  27157  logfac2  27161  chpchtsum  27163  dchrmulcl  27193  dchrresb  27203  bclbnd  27224  bposlem1  27228  bposlem5  27232  gausslemma2dlem0c  27302  lgsquadlem1  27324  m1lgs  27332  2lgsoddprmlem2  27353  dchrisumlem3  27435  dchrisum0lem1  27460  sltval2  27601  noextenddif  27613  sleloe  27699  sletri3  27700  eqscut  27752  elmade2  27819  sltadd1  27941  negsunif  28003  sltsub1  28022  sltsubadd2d  28036  mulsproplem12  28072  sltmul2  28116  sltmul1d  28118  divsmulw  28138  sltdivmul2wd  28145  onsiso  28211  n0subs  28295  n0sleltp1  28298  elzn0s  28328  avgslt1d  28382  avgslt2d  28383  zs12ge0  28399  tgjustr  28458  trgcgrg  28499  lnrot1  28607  islnopp  28723  ismidb  28762  islmib  28771  axsegconlem6  28907  axeuclidlem  28947  axcontlem2  28950  axcontlem4  28952  axcontlem12  28960  ausgrusgrb  29150  nb3grpr2  29368  cplgr2v  29417  umgr2v2enb1  29512  crctcsh  29809  clwwlknonwwlknonb  30093  eupth2lems  30225  nmoreltpnf  30756  isblo2  30770  nmlnogt0  30784  phoeqi  30844  ubthlem2  30858  hire  31081  normgt0  31114  ho01i  31815  ho02i  31816  hoeq1  31817  hoeq2  31818  nmopreltpnf  31856  adjeq  31922  leop  32110  leopmul2i  32122  pjnormssi  32155  pjimai  32163  jplem1  32255  mddmd2  32296  mdslmd1lem1  32312  mdslmd1lem2  32313  superpos  32341  atnssm0  32363  dmdbr5ati  32409  disjunsn  32581  fcoinvbr  32592  ofpreima  32654  funcnv5mpt  32657  suppiniseg  32674  isoun  32690  fpwrelmapffslem  32722  fpwrelmap  32723  iocinioc2  32769  xrdifh  32770  nndiffz1  32776  sgn3da  32824  xdivmul  32912  cntzsnid  33056  cntrval2  33147  isarchi2  33161  erler  33239  elrsp  33344  lsmsnpridl  33370  lsmssass  33374  r1pid2OLD  33576  finexttrb  33685  algextdeglem6  33742  algextdeglem7  33743  smatrcl  33816  rhmpreimacnlem  33904  sqsscirc2  33929  xrmulc1cn  33950  esumfsup  34090  1stmbfm  34280  2ndmbfm  34281  mbfmcnt  34288  eulerpartlems  34380  eulerpartlemd  34386  ballotlemfc0  34513  ballotlemfcc  34514  ballotlemsima  34536  ballotlemfrcn0  34550  reprinfz1  34642  reprdifc  34647  bnj1173  35021  fineqvnttrclse  35151  vonf1owev  35159  zltp1ne  35161  lfuhgr2  35170  erdszelem7  35248  erdszelem9  35250  iscvm  35310  cvmlift3lem4  35373  rexxfr3dALT  35690  fscgr  36131  seglelin  36167  btwnoutside  36176  lineunray  36198  cldbnd  36377  isfne4  36391  fneval  36403  filnetlem4  36432  nndivsub  36508  bj-gabima  36991  dfgcd3  37375  fvineqsneu  37462  wl-sbhbt  37605  wl-sbcom2d  37612  wl-sbalnae  37613  sin2h  37656  cos2h  37657  matunitlindflem1  37662  matunitlindflem2  37663  matunitlindf  37664  ptrest  37665  poimirlem3  37669  poimirlem4  37670  poimirlem22  37688  poimirlem27  37693  mblfinlem3  37705  mblfinlem4  37706  ismblfin  37707  itg2addnclem  37717  itg2addnclem2  37718  itg2gt0cn  37721  iblabsnclem  37729  ftc1anclem6  37744  areacirclem2  37755  areacirclem5  37758  areacirc  37759  mettrifi  37803  drngoi  37997  eldm4  38319  exanres2  38341  disjecxrn  38442  exeupre  38509  brcoss2  38540  br1cossres2  38548  eldmcoss2  38567  eldm1cossres2  38569  brcosscnv2  38581  erimeq2  38782  disjlem19  38905  prter3  38987  islshpat  39122  lsatnle  39149  ellkr2  39196  lshpkr  39222  lkr0f2  39266  lduallkr3  39267  lkreqN  39275  cvrval2  39379  isat3  39412  glbconN  39482  hlrelat5N  39506  cvrval4N  39519  atlt  39542  1cvrco  39577  pmaple  39866  isline2  39879  isline4N  39882  elpaddn0  39905  elpadd2at2  39912  cdlemkid4  41039  dia0  41157  cdlemm10N  41223  dibglbN  41271  dihmeetlem4preN  41411  dochkrshp3  41493  dvh4dimlem  41548  lcfl5  41601  mapdpglem3  41780  mapdheq  41833  hdmap1eq  41906  hdmapval2lem  41936  hdmapoc  42036  hlhillcs  42063  lcmineqlem18  42145  dvdsexpb  42434  renegadd  42471  resubadd  42478  redivmuld  42544  mulgt0b1d  42571  fsuppssind  42692  fz1eqin  42867  diophin  42870  jm2.19  43091  rmxdiophlem  43113  pw2f1ocnv  43135  wepwsolem  43140  gicabl  43197  idomodle  43289  onsupmaxb  43337  cantnf2  43423  tfsconcatb0  43442  tfsnfin  43450  ntrclsfveq2  44159  ntrclsss  44161  ntrclsk4  44170  extoimad  44262  radcnvrat  44412  bcc0  44438  supxrre3rnmpt  45532  clim2f  45739  clim2f2  45773  liminfreuzlem  45905  liminfltlem  45907  xlimmnflimsup2  45955  xlimpnfliminf2  45964  xlimlimsupleliminf  45966  opprb  47136  funbrafv2b  47264  dfafn5a  47265  leaddsuble  47402  mod2addne  47469  iccpartgtprec  47525  flsqrt  47698  dfeven2  47754  dfodd3  47755  lindslinindimp2lem4  48567  snlindsntor  48577  regt1loggt0  48642  elbigo2  48658  elbigolo1  48663  fldivexpfllog2  48671  nnlog2ge0lt1  48672  blenpw2m1  48685  naryfvalelwrdf  48739  isprsd  49060  resccatlem  49179  functhinclem1  49550  thincciso  49559  thinciso  49576  isinito2lem  49604  fulltermc  49617  prstcprs  49666  oduoppcciso  49672  postc  49675  lmdran  49777  cmdlan  49778