Theorem bitr4d 285

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3bitr2d  310  3bitr2rd  311  3bitr4d  314  3bitr4rd  315  bianabs  545  mpbirand  706  sb3b  2490  sbcom3  2525  sbal1  2548  sbal2  2549  sbal2OLD  2550  2reu4lem  4418  issn  4720  disjprgw  5027  disjprg  5028  reuhypd  5288  ordtri3  6205  ordsssuc  6255  iota1  6312  funbrfv2b  6711  dffn5  6712  feqmptdf  6723  unima  6727  dmfco  6748  fneqeql  6807  f1ompt  6866  dff13  7005  fliftcnv  7058  soisores  7074  isotr  7083  isoini  7085  caovord3  7357  releldm2  7746  fimaproj  7834  brtpos  7911  tpostpos  7922  oe1m  8181  oawordri  8186  oalimcl  8196  omlimcl  8214  omabs  8284  iserd  8325  qliftel  8390  qliftfun  8392  qliftf  8395  ecopovsym  8409  pw2f1olem  8642  mapen  8703  suppeqfsuppbi  8880  mapfien  8905  supisolem  8970  cantnflem1  9185  wemapwe  9193  rankr1clem  9282  rankr1c  9283  ranklim  9306  r1pwALT  9308  r1pwcl  9309  isfin1-2  9845  isfin1-4  9847  fin71num  9857  axdc3lem2  9911  ltmnq  10432  prlem936  10507  ltsosr  10554  ltasr  10560  xrlenlt  10744  ltxrlt  10749  letri3  10764  ne0gt0  10783  subadd  10927  ltsubadd2  11149  lesubadd2  11151  suble  11156  ltsub23  11158  ltaddpos2  11169  ltsubpos  11170  subge02  11194  ltord2  11207  leord2  11208  ltaddsublt  11305  divmul  11339  divmul3  11341  rec11r  11377  ltdiv1  11542  ltdivmul2  11555  ledivmul2  11557  ltrec  11560  ltdiv2  11564  negfi  11626  negiso  11657  nnle1eq1  11704  avgle1  11914  avgle2  11915  avgle  11916  nn0le0eq0  11962  elz2  12038  znnnlt1  12048  zleltp1  12072  difrp  12468  xrltlen  12580  dfle2  12581  xrletri3  12588  xgepnf  12599  xlemnf  12601  qbtwnre  12633  xltnegi  12650  supxrre  12761  infxrre  12770  elioo5  12836  elfz5  12948  elfzm11  13027  predfz  13081  flbi  13235  flbi2  13236  fldiv4lem1div2uz2  13255  fznnfl  13279  zmodid2  13316  2submod  13349  lt2sq  13548  le2sq  13549  sqlecan  13621  bcval5  13728  pfxsuffeqwrdeq  14107  shftfib  14479  mulre  14528  cnpart  14647  sqrlem6  14655  sqrmo  14659  elicc4abs  14727  abs2difabs  14742  cau4  14764  limsupgre  14886  clim2  14909  ello1mpt2  14927  lo1resb  14969  o1resb  14971  climeq  14972  climmpt2  14978  isercoll  15072  caucvgb  15084  fsumabs  15204  isumshft  15242  geomulcvg  15280  absefib  15599  dvdsval3  15659  dvdsabseq  15714  dvdsflip  15718  dvdsssfz1  15719  mod2eq1n2dvds  15748  ndvdsadd  15811  bitscmp  15837  smupvallem  15882  dvdssq  15963  lcmdvds  16004  ncoprmgcdgt1b  16047  isprm3  16079  isprm5  16103  phiprmpw  16168  prmdiv  16177  pc11  16271  pcz  16272  pockthlem  16296  prmreclem2  16308  prmreclem4  16310  prmreclem6  16312  1arith  16318  vdwapun  16365  rami  16406  ramcl  16420  pwsle  16823  ercpbllem  16879  invsym  17091  funcres2c  17230  latnle  17761  grpinvcnv  18234  subgacs  18380  eqger  18397  gexdvds2  18777  pgpfi1  18787  pgpfi  18797  lsmass  18862  lssnle  18867  lsmdisj3b  18883  lsmhash  18898  ablsubadd  19000  gsumval3lem2  19094  subgdmdprd  19224  pgpfac1lem2  19265  dvdsr02  19477  drngid2  19586  issubrg3  19631  sdrgacs  19648  lssacs  19807  prmirred  20264  chrdvds  20296  chrcong  20297  chrnzr  20298  znleval  20322  znleval2  20323  cygznlem3  20337  frlmbas  20520  elfilspd  20568  lindfmm  20592  islindf4  20603  islindf5  20604  psrbaglefi  20694  psrbaglefiOLD  20695  coe1mul2lem1  20991  mdetunilem9  21320  isneip  21805  neiptopnei  21832  lpdifsn  21843  restopnb  21875  restopn2  21877  restdis  21878  restperf  21884  lmbr2  21959  cncls2  21973  cnprest  21989  cnprest2  21990  iscnrm2  22038  ist0-2  22044  ist1-3  22049  ishaus2  22051  cmpfi  22108  dfconn2  22119  1stccnp  22162  subislly  22181  hausmapdom  22200  tx1cn  22309  tx2cn  22310  txcnmpt  22324  txrest  22331  hauseqlcld  22346  tgqtop  22412  qtopcld  22413  ordthmeolem  22501  trfil2  22587  trfil3  22588  trnei  22592  ufildr  22631  fmfg  22649  rnelfm  22653  fmfnfm  22658  elflim  22671  flimrest  22683  cnflf  22702  cnflf2  22703  ptcmplem2  22753  ghmcnp  22815  tsmssubm  22843  iscfilu  22989  xmetgt0  23060  prdsxmetlem  23070  blcomps  23095  blcom  23096  xblpnfps  23097  xblpnf  23098  blpnf  23099  xmeter  23135  setsxms  23181  imasf1obl  23190  stdbdbl  23219  metrest  23226  metuel2  23267  dscopn  23275  xrtgioo  23507  metdstri  23552  cnmpopc  23629  iihalf2  23634  icopnfhmeo  23644  evth2  23661  lmmbr3  23960  iscau3  23978  metcld  24006  cfilucfil3  24020  srabn  24060  rrxmet  24108  minveclem4  24132  evthicc2  24160  ovolgelb  24180  shft2rab  24208  ovolshftlem1  24209  sca2rab  24212  ovolscalem1  24213  ioombl1lem4  24261  mbfmulc2lem  24347  ismbf3d  24354  mbfsup  24364  mbfinf  24365  i1f1lem  24389  i1fmulclem  24402  mbfi1fseqlem4  24418  itg2seq  24442  ditgneg  24556  limcdif  24575  limcnlp  24577  cnplimc  24586  rolle  24689  mvth  24691  dvne0  24710  lhop1lem  24712  itgsubst  24748  mdegle0  24777  deg1leb  24795  deg1le0  24811  q1peqb  24854  coemulhi  24950  dgrlt  24962  plydivlem3  24990  vieta1lem2  25006  aannenlem1  25023  ulmres  25082  reefiso  25142  pilem3  25147  ellogdm  25329  root1eq1  25443  angpieqvdlem  25513  angpieqvdlem2  25514  quad2  25524  1cubr  25527  quart  25546  rlimcnp  25650  wilthlem2  25753  isppw  25798  dvdsflsumcom  25872  fsumvma  25896  logfac2  25900  chpchtsum  25902  dchrmulcl  25932  dchrresb  25942  bclbnd  25963  bposlem1  25967  bposlem5  25971  gausslemma2dlem0c  26041  lgsquadlem1  26063  m1lgs  26071  2lgsoddprmlem2  26092  dchrisumlem3  26174  dchrisum0lem1  26199  tgjustr  26367  trgcgrg  26408  lnrot1  26516  islnopp  26632  ismidb  26671  islmib  26680  axsegconlem6  26815  axeuclidlem  26855  axcontlem2  26858  axcontlem4  26860  axcontlem12  26868  ausgrusgrb  27057  nb3grpr2  27272  cplgr2v  27321  umgr2v2enb1  27415  crctcsh  27709  clwwlknonwwlknonb  27990  eupth2lems  28122  nmoreltpnf  28651  isblo2  28665  nmlnogt0  28679  phoeqi  28739  ubthlem2  28753  hire  28976  normgt0  29009  ho01i  29710  ho02i  29711  hoeq1  29712  hoeq2  29713  nmopreltpnf  29751  adjeq  29817  leop  30005  leopmul2i  30017  pjnormssi  30050  pjimai  30058  jplem1  30150  mddmd2  30191  mdslmd1lem1  30207  mdslmd1lem2  30208  superpos  30236  atnssm0  30258  dmdbr5ati  30304  disjunsn  30455  fcoinvbr  30469  ofpreima  30526  funcnv5mpt  30529  suppiniseg  30544  isoun  30558  fpwrelmapffslem  30591  fpwrelmap  30592  iocinioc2  30624  xrdifh  30625  nndiffz1  30631  xdivmul  30723  cntzsnid  30847  isarchi2  30965  elrsp  31090  lsmsnpridl  31107  lsmssass  31111  finexttrb  31258  smatrcl  31267  rhmpreimacnlem  31355  sqsscirc2  31380  xrmulc1cn  31401  esumfsup  31557  1stmbfm  31746  2ndmbfm  31747  mbfmcnt  31754  eulerpartlems  31846  eulerpartlemd  31852  ballotlemfc0  31978  ballotlemfcc  31979  ballotlemsima  32001  ballotlemfrcn0  32015  sgn3da  32027  reprinfz1  32121  reprdifc  32126  bnj1173  32502  zltp1ne  32576  lfuhgr2  32596  erdszelem7  32675  erdszelem9  32677  iscvm  32737  cvmlift3lem4  32800  sltval2  33444  noextenddif  33456  sleloe  33542  sletri3  33543  eqscut  33582  elmade2  33630  fscgr  33953  seglelin  33989  btwnoutside  33998  lineunray  34020  cldbnd  34086  isfne4  34100  fneval  34112  filnetlem4  34141  nndivsub  34217  dfgcd3  35040  fvineqsneu  35130  wl-sbhbt  35257  wl-sbcom2d  35264  wl-sbalnae  35265  wl-ax11-lem8  35291  wl-dfrmof  35322  sin2h  35349  cos2h  35350  matunitlindflem1  35355  matunitlindflem2  35356  matunitlindf  35357  ptrest  35358  poimirlem3  35362  poimirlem4  35363  poimirlem22  35381  poimirlem27  35386  mblfinlem3  35398  mblfinlem4  35399  ismblfin  35400  itg2addnclem  35410  itg2addnclem2  35411  itg2gt0cn  35414  iblabsnclem  35422  ftc1anclem6  35437  areacirclem2  35448  areacirclem5  35451  areacirc  35452  mettrifi  35497  drngoi  35691  eldm4  35993  exanres2  36016  brcoss2  36139  br1cossres2  36147  eldmcoss2  36161  eldm1cossres2  36163  brcosscnv2  36175  erim2  36373  prter3  36480  islshpat  36615  lsatnle  36642  ellkr2  36689  lshpkr  36715  lkr0f2  36759  lduallkr3  36760  lkreqN  36768  cvrval2  36872  isat3  36905  glbconN  36975  hlrelat5N  36999  cvrval4N  37012  atlt  37035  1cvrco  37070  pmaple  37359  isline2  37372  isline4N  37375  elpaddn0  37398  elpadd2at2  37405  cdlemkid4  38532  dia0  38650  cdlemm10N  38716  dibglbN  38764  dihmeetlem4preN  38904  dochkrshp3  38986  dvh4dimlem  39041  lcfl5  39094  mapdpglem3  39273  mapdheq  39326  hdmap1eq  39399  hdmapval2lem  39429  hdmapoc  39529  hlhillcs  39556  lcmineqlem18  39635  fsuppssind  39809  renegadd  39874  resubadd  39881  mulgt0b2d  39949  fz1eqin  40105  diophin  40108  jm2.19  40329  rmxdiophlem  40351  pw2f1ocnv  40373  wepwsolem  40381  gicabl  40438  idomodle  40535  isdomn3  40543  ntrclsfveq2  41159  ntrclsss  41161  ntrclsk4  41170  extoimad  41263  radcnvrat  41413  bcc0  41439  supxrre3rnmpt  42454  clim2f  42666  clim2f2  42700  liminfreuzlem  42832  liminfltlem  42834  xlimmnflimsup2  42882  xlimpnfliminf2  42891  xlimlimsupleliminf  42893  opprb  44011  funbrafv2b  44105  dfafn5a  44106  leaddsuble  44244  iccpartgtprec  44327  flsqrt  44500  dfeven2  44556  dfodd3  44557  lindslinindimp2lem4  45257  snlindsntor  45267  regt1loggt0  45337  elbigo2  45353  elbigolo1  45358  fldivexpfllog2  45366  nnlog2ge0lt1  45367  blenpw2m1  45380  naryfvalelwrdf  45434