Theorem bitr4d 284

Description: Deduction form of bitr4i 280. (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 225	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 281	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3bitr2d  309  3bitr2rd  310  3bitr4d  313  3bitr4rd  314  bianabs  549  mpbirand  717  sb3b  2508  sbcom3  2538  sbal1  2560  sbal2  2561  2reu4lem  4478  issn  4791  disjprg  5097  reuhypd  5377  snelpwg  5411  ordtri3  6382  ordsssuc  6437  iota1  6500  funbrfv2b  6924  dffn5  6925  feqmptdf  6937  unima  6942  dmfco  6963  fneqeql  7027  f1ompt  7092  dff13  7238  fliftcnv  7295  soisores  7311  isotr  7320  isoini  7322  caovord3  7609  releldm2  8024  fimaproj  8115  brtpos  8215  tpostpos  8226  oe1m  8514  oawordri  8519  oalimcl  8529  omlimcl  8547  omabs  8621  iserd  8705  qliftel  8782  qliftfun  8784  qliftf  8787  ecopovsym  8801  pw2f1olem  9053  mapen  9113  findcard3  9227  tfsnfin2  9304  suppeqfsuppbi  9323  mapfien  9352  supisolem  9418  cantnflem1  9642  wemapwe  9650  rankr1clem  9776  rankr1c  9777  ranklim  9800  r1pwALT  9802  r1pwcl  9803  isfin1-2  10353  isfin1-4  10355  fin71num  10365  axdc3lem2  10419  infinfg  10534  ltmnq  10941  prlem936  11016  ltsosr  11063  ltasr  11069  xrlenlt  11258  ltxrlt  11264  letri3  11279  ne0gt0  11299  subadd  11444  ltsubadd2  11669  lesubadd2  11671  suble  11676  ltsub23  11678  ltaddpos2  11689  ltsubpos  11690  subge02  11714  ltord2  11727  leord2  11728  ltaddsublt  11825  divmul  11859  divmul3  11861  rec11r  11901  ltdiv1  12066  ltdivmul2  12079  ledivmul2  12081  ltrec  12084  ltdiv2  12088  negfi  12151  negiso  12182  nnle1eq1  12253  avgle1  12471  avgle2  12472  avgle  12473  nn0le0eq0  12519  elz2  12596  znnnlt1  12608  zleltp1  12632  difrp  13043  xrltlen  13158  dfle2  13159  xrletri3  13166  xgepnf  13178  xlemnf  13180  qbtwnre  13212  xltnegi  13229  supxrre  13340  infxrre  13350  elioo5  13417  elfz5  13531  elfzm11  13610  predfz  13668  flbi  13836  flbi2  13837  fldiv4lem1div2uz2  13856  fznnfl  13882  zmodid2  13919  2submod  13955  lt2sq  14156  le2sq  14157  sqlecan  14232  bcval5  14341  pfxsuffeqwrdeq  14721  shftfib  15095  sgn3da  15124  mulre  15158  cnpart  15277  01sqrexlem6  15284  sqrmo  15288  elicc4abs  15357  abs2difabs  15372  cau4  15394  limsupgre  15518  clim2  15541  ello1mpt2  15559  lo1resb  15601  o1resb  15603  climeq  15604  climmpt2  15610  isercoll  15705  caucvgb  15717  fsumabs  15839  isumshft  15879  geomulcvg  15916  absefib  16240  dvdsval3  16300  addmulmodb  16309  dvdsabseq  16357  dvdsflip  16361  dvdsssfz1  16362  mod2eq1n2dvds  16391  ndvdsadd  16454  bitscmp  16482  smupvallem  16527  dvdssq  16611  lcmdvds  16652  ncoprmgcdgt1b  16695  isprm3  16727  isprm5  16752  phiprmpw  16821  prmdiv  16830  pc11  16926  pcz  16927  pockthlem  16951  prmreclem2  16963  prmreclem4  16965  prmreclem6  16967  1arith  16973  vdwapun  17020  rami  17061  ramcl  17075  pwsle  17532  ercpbllem  17588  invsym  17805  funcres2c  17946  latnle  18515  grpinvcnv  19058  subgacs  19212  eqger  19229  ghmqusker  19337  gexdvds2  19635  pgpfi1  19645  pgpfi  19655  lsmass  19719  lssnle  19724  lsmdisj3b  19740  lsmhash  19755  ablsubadd  19859  gsumval3lem2  19956  subgdmdprd  20086  pgpfac1lem2  20127  dvdsr02  20431  issubrg3  20660  isdomn3  20774  drngid2  20810  sdrgunit  20852  sdrgacs  20857  lssacs  21041  prmirred  21533  chrdvds  21585  chrcong  21586  chrnzr  21589  znleval  21613  znleval2  21614  cygznlem3  21628  frlmbas  21814  elfilspd  21862  lindfmm  21886  islindf4  21897  islindf5  21898  psrbaglefi  21985  coe1mul2lem1  22337  mdetunilem9  22687  isneip  23172  neiptopnei  23199  lpdifsn  23210  restopnb  23242  restopn2  23244  restdis  23245  restperf  23251  lmbr2  23326  cncls2  23340  cnprest  23356  cnprest2  23357  iscnrm2  23405  ist0-2  23411  ist1-3  23416  ishaus2  23418  cmpfi  23475  dfconn2  23486  1stccnp  23529  subislly  23548  hausmapdom  23567  tx1cn  23676  tx2cn  23677  txcnmpt  23691  txrest  23698  hauseqlcld  23713  tgqtop  23779  qtopcld  23780  ordthmeolem  23868  trfil2  23954  trfil3  23955  trnei  23959  ufildr  23998  fmfg  24016  rnelfm  24020  fmfnfm  24025  elflim  24038  flimrest  24050  cnflf  24069  cnflf2  24070  ptcmplem2  24120  ghmcnp  24182  tsmssubm  24210  iscfilu  24354  xmetgt0  24425  prdsxmetlem  24435  blcomps  24460  blcom  24461  xblpnfps  24462  xblpnf  24463  blpnf  24464  xmeter  24500  setsxms  24546  imasf1obl  24555  stdbdbl  24584  metrest  24591  metuel2  24632  dscopn  24640  xrtgioo  24874  metdstri  24919  cnmpopc  24997  iihalf2  25002  icopnfhmeo  25012  evth2  25029  lmmbr3  25329  iscau3  25347  metcld  25375  cfilucfil3  25389  srabn  25429  rrxmet  25477  minveclem4  25501  evthicc2  25529  ovolgelb  25549  shft2rab  25577  ovolshftlem1  25578  sca2rab  25581  ovolscalem1  25582  ioombl1lem4  25630  mbfmulc2lem  25716  ismbf3d  25723  mbfsup  25733  mbfinf  25734  i1f1lem  25758  i1fmulclem  25771  mbfi1fseqlem4  25787  itg2seq  25811  ditgneg  25926  limcdif  25945  limcnlp  25947  cnplimc  25956  rolle  26059  mvth  26061  dvne0  26080  lhop1lem  26082  itgsubst  26118  mdegle0  26144  deg1leb  26162  deg1le0  26178  q1peqb  26223  coemulhi  26321  dgrlt  26333  plydivlem3  26366  vieta1lem2  26382  aannenlem1  26399  ulmres  26458  reefiso  26518  pilem3  26523  ellogdm  26711  root1eq1  26827  angpieqvdlem  26900  angpieqvdlem2  26901  quad2  26911  1cubr  26914  quart  26933  rlimcnp  27037  wilthlem2  27140  isppw  27185  dvdsflsumcom  27259  fsumvma  27284  logfac2  27288  chpchtsum  27290  dchrmulcl  27320  dchrresb  27330  bclbnd  27351  bposlem1  27355  bposlem5  27359  gausslemma2dlem0c  27429  lgsquadlem1  27451  m1lgs  27459  2lgsoddprmlem2  27480  dchrisumlem3  27562  dchrisum0lem1  27587  ltsval2  27727  noextenddif  27739  lesloe  27825  lestri3  27826  eqcuts  27885  elmade2  27958  ltadds1  28092  negsunif  28155  ltsubs1  28176  ltsubadds2d  28190  mulsproplem12  28227  ltmuls2  28271  ltmuls1d  28273  divmulsw  28293  ltdivmuls2wd  28300  oniso  28371  n0subs  28463  n0lesltp1  28466  elzn0s  28498  avglts1d  28553  avglts2d  28554  bdaypw2n0bndlem  28563  z12sge0  28583  dfz12s2  28588  elreno2  28595  tgjustr  28650  trgcgrg  28691  lnrot1  28799  islnopp  28919  ismidb  28958  islmib  28967  elplng  28994  plngcplem  28999  axsegconlem6  29130  axeuclidlem  29170  axcontlem2  29173  axcontlem4  29175  axcontlem12  29183  ausgrusgrb  29373  nb3grpr2  29591  cplgr2v  29640  umgr2v2enb1  29734  crctcsh  30031  clwwlknonwwlknonb  30315  eupth2lems  30447  nmoreltpnf  30979  isblo2  30993  nmlnogt0  31007  phoeqi  31067  ubthlem2  31081  hire  31304  normgt0  31337  ho01i  32038  ho02i  32039  hoeq1  32040  hoeq2  32041  nmopreltpnf  32079  adjeq  32145  leop  32333  leopmul2i  32345  pjnormssi  32378  pjimai  32386  jplem1  32478  mddmd2  32519  mdslmd1lem1  32535  mdslmd1lem2  32536  superpos  32564  atnssm0  32586  dmdbr5ati  32632  disjunsn  32800  fcoinvbr  32811  ofpreima  32873  funcnv5mpt  32875  suppiniseg  32894  isoun  32910  fpwrelmapffslem  32940  fpwrelmap  32941  iocinioc2  32987  xrdifh  32988  nndiffz1  32994  xdivmul  33108  cntzsnid  33266  cntrval2  33357  isarchi2  33371  isunitc  33428  erler  33452  rlocisunit  33463  elrsp  33561  lsmsnpridl  33587  lsmssass  33591  esplyind  33874  finexttrb  33964  algextdeglem6  34021  algextdeglem7  34022  smatrcl  34095  rhmpreimacnlem  34183  sqsscirc2  34208  xrmulc1cn  34229  esumfsup  34369  1stmbfm  34559  2ndmbfm  34560  mbfmcnt  34567  eulerpartlems  34659  eulerpartlemd  34665  ballotlemfc0  34792  ballotlemfcc  34793  ballotlemsima  34815  ballotlemfrcn0  34829  reprinfz1  34918  reprdifc  34923  bnj1173  35299  fineqvnttrclse  35424  vonf1wev  35455  vonf1owevOLD  35457  zltp1ne  35464  lfuhgr2  35474  erdszelem7  35552  erdszelem9  35554  iscvm  35614  cvmlift3lem4  35677  rexxfr3dALT  35994  fscgr  36435  seglelin  36471  btwnoutside  36480  lineunray  36502  cldbnd  36691  isfne4  36705  fneval  36717  filnetlem4  36746  nndivsub  36822  bj-gabima  37430  dfgcd3  37821  fvineqsneu  37910  wl-sbhbt  38062  wl-sbcom2d  38069  wl-sbalnae  38070  sin2h  38114  cos2h  38115  matunitlindflem1  38120  matunitlindflem2  38121  matunitlindf  38122  ptrest  38123  poimirlem3  38127  poimirlem4  38128  poimirlem22  38146  poimirlem27  38151  mblfinlem3  38163  mblfinlem4  38164  ismblfin  38165  itg2addnclem  38175  itg2addnclem2  38176  itg2gt0cn  38179  iblabsnclem  38187  ftc1anclem6  38202  areacirclem2  38213  areacirclem5  38216  areacirc  38217  mettrifi  38261  drngoi  38455  eldm4  38785  exanres2  38807  disjecxrn  38916  exeupre  38995  brcoss2  39026  br1cossres2  39034  eldmcoss2  39053  eldm1cossres2  39055  brcosscnv2  39067  erimeq2  39267  disjqmap  39331  disjlem19  39408  prter3  39511  islshpat  39646  lsatnle  39673  ellkr2  39720  lshpkr  39746  lkr0f2  39790  lduallkr3  39791  lkreqN  39799  cvrval2  39903  isat3  39936  glbconN  40006  hlrelat5N  40030  cvrval4N  40043  atlt  40066  1cvrco  40101  pmaple  40390  isline2  40403  isline4N  40406  elpaddn0  40429  elpadd2at2  40436  cdlemkid4  41563  dia0  41681  cdlemm10N  41747  dibglbN  41795  dihmeetlem4preN  41935  dochkrshp3  42017  dvh4dimlem  42072  lcfl5  42125  mapdpglem3  42304  mapdheq  42357  hdmap1eq  42430  hdmapval2lem  42460  hdmapoc  42560  hlhillcs  42587  lcmineqlem18  42668  dvdsexpb  42949  renegadd  42986  resubadd  42993  redivmuld  43059  mulgt0b1d  43099  fsuppssind  43180  fz1eqin  43355  diophin  43358  jm2.19  43575  rmxdiophlem  43597  pw2f1ocnv  43619  wepwsolem  43624  gicabl  43681  idomodle  43773  onsupmaxb  43821  cantnf2  43907  tfsconcatb0  43926  tfsnfin  43934  ntrclsfveq2  44642  ntrclsss  44644  ntrclsk4  44653  extoimad  44745  radcnvrat  44881  bcc0  44907  supxrre3rnmpt  45994  clim2f  46201  clim2f2  46235  liminfreuzlem  46367  liminfltlem  46369  xlimmnflimsup2  46417  xlimpnfliminf2  46426  xlimlimsupleliminf  46428  opprb  47616  funbrafv2b  47744  dfafn5a  47745  leaddsuble  47882  mod2addne  47955  iccpartgtprec  48017  flsqrt  48193  dfeven2  48262  dfodd3  48263  lindslinindimp2lem4  49074  snlindsntor  49084  regt1loggt0  49149  elbigo2  49165  elbigolo1  49170  fldivexpfllog2  49178  nnlog2ge0lt1  49179  blenpw2m1  49192  naryfvalelwrdf  49246  isprsd  49567  resccatlem  49685  functhinclem1  50056  thincciso  50065  thinciso  50082  isinito2lem  50110  fulltermc  50123  prstcprs  50172  oduoppcciso  50178  postc  50181  lmdran  50283  cmdlan  50284