Theorem bitr4d 273

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

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  3bitr2d  298  3bitr2rd  299  3bitr4d  302  3bitr4rd  303  bianabs  537  mpbirand  698  mpbiran2d  699  sbcom3  2502  sbal1  2552  sbal2  2553  issn  4517  disjprg  4807  reuhypd  5060  ordtri3  5946  ordsssuc  5996  iota1  6047  funbrfv2b  6431  dffn5  6432  feqmptdf  6442  dmfco  6463  fneqeql  6517  f1ompt  6573  dff13  6706  fliftcnv  6755  soisores  6771  isotr  6780  isoini  6782  caovord3  7047  releldm2  7420  brtpos  7566  tpostpos  7577  oe1m  7832  oawordri  7837  oalimcl  7847  omlimcl  7865  omabs  7934  iserd  7975  qliftel  8035  qliftfun  8037  qliftf  8040  ecopovsym  8055  pw2f1olem  8273  mapen  8333  suppeqfsuppbi  8498  funsnfsupp  8508  mapfien  8522  supisolem  8588  cantnflem1  8803  wemapwe  8811  rankr1clem  8900  rankr1c  8901  ranklim  8924  r1pwALT  8926  r1pwcl  8927  isfin1-2  9462  isfin1-4  9464  fin71num  9474  axdc3lem2  9528  ltmnq  10049  prlem936  10124  ltsosr  10170  ltasr  10176  xrlenlt  10359  ltxrlt  10364  letri3  10379  ne0gt0  10398  subadd  10540  ltsubadd2  10755  lesubadd2  10757  suble  10762  ltsub23  10764  ltaddpos2  10775  ltsubpos  10776  subge02  10800  ltord2  10813  leord2  10814  ltaddsublt  10910  divmul  10944  divmul3  10946  rec11r  10980  ltdiv1  11143  ltdivmul2  11156  ledivmul2  11158  ltrec  11161  ltdiv2  11165  negfi  11227  negiso  11259  nnle1eq1  11307  avgle1  11520  avgle2  11521  avgle  11522  nn0le0eq0  11570  elz2  11643  znnnlt1  11654  zleltp1  11678  uzin  11923  difrp  12069  xrltlen  12182  dfle2  12183  xrletri3  12190  xgepnf  12201  xlemnf  12203  qbtwnre  12235  xltnegi  12252  supxrre  12362  supxrre1  12365  infxrre  12371  ixxun  12396  elioo5  12436  elfz5  12544  elfzm11  12621  uzsplit  12622  predfz  12675  flbi  12828  flbi2  12829  fldiv4lem1div2uz2  12848  fznnfl  12872  zmodid2  12909  2submod  12942  lt2sq  13147  le2sq  13148  sqlecan  13181  bcval5  13312  pfxsuffeqwrdeq  13688  shftfib  14100  mulre  14149  cnpart  14268  sqrlem6  14276  sqrmo  14280  elicc4abs  14347  abs2difabs  14362  cau4  14384  limsupgre  14500  clim2  14523  ello12  14535  ello1mpt2  14541  elo12  14546  lo1resb  14583  o1resb  14585  climeq  14586  climmpt2  14592  isercoll  14686  caucvgb  14698  fsumss  14744  fsumabs  14820  isumshft  14858  geomulcvg  14894  fprodss  14964  absefib  15213  dvdsval3  15272  dvdsabseq  15323  dvdsflip  15327  dvdsssfz1  15328  mod2eq1n2dvds  15356  ndvdsadd  15418  bitscmp  15444  smupvallem  15489  dvdssq  15564  lcmdvds  15605  ncoprmgcdgt1b  15648  isprm3  15679  isprm5  15701  phiprmpw  15763  prmdiv  15772  pc11  15866  pcz  15867  pockthlem  15891  prmreclem2  15903  prmreclem4  15905  prmreclem6  15907  1arith  15913  vdwapun  15960  ramval  15994  rami  16001  ramcl  16015  pwsle  16421  ercpbllem  16477  invsym  16690  funcres2c  16829  latnle  17354  grpinvcnv  17753  subgacs  17896  eqger  17911  gexdvds2  18267  pgpfi1  18277  pgpfi  18287  lsmass  18350  lssnle  18354  lsmdisj3b  18370  lsmhash  18385  ablsubadd  18486  gsumval3lem2  18576  subgdmdprd  18703  pgpfac1lem2  18744  dvdsr02  18926  drngid2  19035  issubrg3  19080  lssacs  19242  lspsnel5  19270  psrbaglefi  19649  coe1mul2lem1  19913  prmirred  20119  chrdvds  20152  chrcong  20153  chrnzr  20154  znleval  20178  znleval2  20179  cygznlem3  20193  frlmbas  20378  elfilspd  20421  lindfmm  20445  islindf4  20456  islindf5  20457  mdetunilem9  20706  discld  21176  isneip  21192  neiptopnei  21219  lpdifsn  21230  restopnb  21262  restopn2  21264  restdis  21265  restperf  21271  lmbr2  21346  cncls2  21360  cnprest  21376  cnprest2  21377  iscnrm2  21425  ist0-2  21431  cnt0  21433  ist1-3  21436  ishaus2  21438  cmpfi  21494  dfconn2  21505  1stccnp  21548  1stccn  21549  subislly  21567  hausmapdom  21586  kgencn  21642  tx1cn  21695  tx2cn  21696  txcnmpt  21710  txrest  21717  hauseqlcld  21732  tgqtop  21798  qtopcld  21799  qtopcn  21800  ordthmeolem  21887  trfil2  21973  trfil3  21974  trnei  21978  ufildr  22017  fmfg  22035  rnelfm  22039  fmfnfm  22044  elflim  22057  fbflim  22062  flimrest  22069  isflf  22079  cnflf  22088  cnflf2  22089  fclscf  22111  cnfcf  22128  ptcmplem2  22139  ghmcnp  22200  tsmssubm  22228  iscfilu  22374  xmetgt0  22445  prdsxmetlem  22455  elbl2ps  22476  elbl2  22477  blcomps  22480  blcom  22481  xblpnfps  22482  xblpnf  22483  blpnf  22484  xmeter  22520  setsxms  22566  imasf1obl  22575  stdbdbl  22604  metrest  22611  metcn  22630  txmetcn  22635  metuel2  22652  dscopn  22660  xrtgioo  22891  metdstri  22936  cncffvrn  22983  cnmpt2pc  23009  iihalf2  23014  icopnfhmeo  23024  evth2  23041  lmmbr3  23340  iscau3  23358  lmclimf  23384  metcld  23386  cfilucfil3  23400  srabn  23440  rrxmet  23483  minveclem4  23495  evthicc2  23521  ovolfioo  23528  ovolficc  23529  ovolgelb  23541  ovoliun  23566  shft2rab  23569  ovolshftlem1  23570  sca2rab  23573  ovolscalem1  23574  ismbl2  23588  ioombl1lem4  23622  mbfmulc2lem  23708  mbfmax  23710  mbfposr  23713  ismbf3d  23715  mbfaddlem  23721  mbfsup  23725  mbfinf  23726  i1f1lem  23750  i1fmulclem  23763  mbfi1fseqlem4  23779  itg2seq  23803  itg2monolem1  23811  itg2cnlem1  23822  itgfsum  23887  ditgneg  23915  limcdif  23934  limcnlp  23936  cnplimc  23945  rolle  24047  mvth  24049  dvne0  24068  lhop1lem  24070  itgsubst  24106  mdegle0  24131  deg1leb  24149  deg1le0  24165  q1peqb  24208  coemulhi  24304  dgrlt  24316  plydivlem3  24344  vieta1lem2  24360  aannenlem1  24377  ulmres  24436  reefiso  24496  pilem3  24501  pilem3OLD  24502  ellogdm  24679  root1eq1  24790  angpieqvdlem  24849  angpieqvdlem2  24850  quad2  24860  1cubr  24863  quart  24882  rlimcnp  24986  wilthlem2  25089  isppw  25134  dvdsflsumcom  25208  fsumvma  25232  logfac2  25236  chpchtsum  25238  dchrmulcl  25268  dchreq  25277  dchrresb  25278  bclbnd  25299  bposlem1  25303  bposlem5  25307  lgsneg  25340  gausslemma2dlem0c  25377  lgsquadlem1  25399  lgsquadlem2  25400  m1lgs  25407  2lgsoddprmlem2  25428  dchrisumlem3  25474  dchrisum0lem1  25499  trgcgrg  25704  tgellng  25742  lnrot1  25812  islnopp  25925  ismidb  25964  islmib  25973  isleag  26027  ttgelitv  26057  axsegconlem6  26096  axeuclidlem  26136  axcontlem2  26139  axcontlem4  26141  axcontlem12  26149  ausgrusgrb  26341  nb3grpr2  26567  cplgr2v  26622  umgr2v2enb1  26716  crctcsh  27012  wspthsnwspthsnonOLD  27142  dfconngr1  27469  eupth2lems  27519  nmoreltpnf  28083  isblo2  28097  nmlnogt0  28111  phoeqi  28172  ubthlem2  28186  hire  28410  normgt0  28443  ho01i  29146  ho02i  29147  hoeq1  29148  hoeq2  29149  nmopreltpnf  29187  adjeq  29253  leop  29441  leopmul2i  29453  pjnormssi  29486  pjimai  29494  jplem1  29586  mddmd2  29627  mdslmd1lem1  29643  mdslmd1lem2  29644  superpos  29672  atnssm0  29694  dmdbr5ati  29740  disjunsn  29858  fcoinvbr  29870  ofpreima  29918  funcnv5mpt  29921  isoun  29931  fpwrelmapffslem  29959  fpwrelmap  29960  iocinioc2  29993  xrdifh  29994  nndiffz1  30000  xdivmul  30083  isarchi2  30189  smatrcl  30312  fimaproj  30350  sqsscirc2  30405  xrmulc1cn  30426  ismntoplly  30519  esumfsup  30582  1stmbfm  30772  2ndmbfm  30773  mbfmcnt  30780  eulerpartlems  30872  eulerpartlemd  30878  ballotlemfc0  31005  ballotlemfcc  31006  ballotlemsima  31028  ballotlemfrcn0  31042  sgn3da  31054  reprinfz1  31154  reprdifc  31159  bnj1173  31521  erdszelem7  31630  erdszelem9  31632  iscvm  31692  cvmlift3lem4  31755  sltval2  32256  noextenddif  32268  sleloe  32326  sletri3  32327  fscgr  32634  seglelin  32670  btwnoutside  32679  lineunray  32701  cldbnd  32767  isfne4  32781  fneval  32793  filnetlem4  32822  nndivsub  32898  dfgcd3  33607  wl-sbhbt  33764  wl-sbcom2d  33772  wl-sbalnae  33773  wl-ax11-lem8  33797  sin2h  33826  cos2h  33827  matunitlindflem1  33832  matunitlindflem2  33833  matunitlindf  33834  ptrest  33835  poimirlem3  33839  poimirlem4  33840  poimirlem22  33858  poimirlem27  33863  mblfinlem3  33875  mblfinlem4  33876  ismblfin  33877  itg2addnclem  33887  itg2addnclem2  33888  itg2gt0cn  33891  iblabsnclem  33899  ftc1anclem6  33916  areacirclem2  33927  areacirclem5  33930  areacirc  33931  cover2  33934  mettrifi  33978  drngoi  34175  eldm4  34472  exanres2  34500  brcoss2  34619  br1cossres2  34627  eldmcoss2  34641  eldm1cossres2  34643  brcosscnv2  34655  prter3  34841  islshpat  34976  lsatnle  35003  ellkr2  35050  lshpkr  35076  lkr0f2  35120  lduallkr3  35121  lkreqN  35129  cvrval2  35233  isat3  35266  glbconN  35336  hlrelat5N  35360  cvrval4N  35373  atlt  35396  1cvrco  35431  pmaple  35720  isline2  35733  isline4N  35736  elpaddn0  35759  elpadd2at2  35766  cdlemkid4  36893  dia0  37011  cdlemm10N  37077  dibglbN  37125  dihmeetlem4preN  37265  dochkrshp3  37347  dvh4dimlem  37402  lcfl5  37455  mapdpglem3  37634  mapdheq  37687  hdmap1eq  37760  hdmapval2lem  37790  hdmapoc  37890  hlhillcs  37917  fz1eqin  38013  diophin  38017  jm2.19  38240  rmxdiophlem  38262  pw2f1ocnv  38284  wepwsolem  38292  gicabl  38349  sdrgacs  38451  idomodle  38454  isdomn3  38462  ntrclsfveq2  39036  ntrclsss  39038  ntrclsk4  39047  extoimad  39141  radcnvrat  39190  bcc0  39216  unima  39996  supxrre3rnmpt  40296  clim2f  40509  clim2f2  40543  liminfreuzlem  40675  liminfltlem  40677  2reu4a  41863  funbrafv2b  41910  dfafn5a  41911  leaddsuble  42049  iccpartgtprec  42093  flsqrt  42187  dfeven2  42241  dfodd3  42242  lindslinindimp2lem4  42922  snlindsntor  42932  regt1loggt0  43002  elbigo2  43018  elbigolo1  43023  fldivexpfllog2  43031  nnlog2ge0lt1  43032  blenpw2m1  43045