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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr2d  310  3bitr2rd  311  3bitr4d  314  3bitr4rd  315  bianabs  551  mpbirand  720  sb3b  2508  sbcom3  2538  sbal1  2560  sbal2  2561  2reu4lem  4482  issn  4790  disjprg  5102  reuhypd  5385  snelpwg  5415  ordtri3  6417  ordsssuc  6472  iota1  6536  funbrfv2b  6965  dffn5  6966  feqmptdf  6978  unima  6983  dmfco  7004  fneqeql  7068  elpreima  7080  f1ompt  7135  dff13  7281  fliftcnv  7342  soisores  7358  isotr  7367  isoini  7369  caovord3  7658  releldm2  8078  fimaproj  8179  brtpos  8280  tpostpos  8291  oe1m  8581  oawordri  8586  oalimcl  8596  omlimcl  8614  omabs  8688  iserd  8772  qliftel  8849  qliftfun  8851  qliftf  8854  ecopovsym  8868  pw2f1olem  9128  mapen  9188  findcard3  9302  tfsnfin2  9380  suppeqfsuppbi  9398  mapfien  9427  supisolem  9493  cantnflem1  9717  wemapwe  9725  rankr1clem  9856  rankr1c  9857  ranklim  9885  r1pwALT  9887  r1pwcl  9888  isfin1-2  10490  isfin1-4  10492  fin71num  10502  axdc3lem2  10556  infinfg  10677  ltmnq  11084  prlem936  11159  ltsosr  11206  ltasr  11212  xrlenlt  11401  ltxrlt  11407  letri3  11422  ne0gt0  11442  subadd  11587  ltsubadd2  11814  lesubadd2  11816  suble  11821  ltsub23  11823  ltaddpos2  11834  ltsubpos  11835  subge02  11859  ltord2  11872  leord2  11873  ltaddsublt  11970  divmul  12004  divmul3  12006  rec11r  12043  ltdiv1  12208  ltdivmul2  12221  ledivmul2  12223  ltrec  12226  ltdiv2  12230  negfi  12293  negiso  12324  nnle1eq1  12395  avgle1  12613  avgle2  12614  avgle  12615  nn0le0eq0  12661  elz2  12738  znnnlt1  12750  zleltp1  12774  difrp  13187  xrltlen  13302  dfle2  13303  xrletri3  13310  xgepnf  13322  xlemnf  13324  qbtwnre  13356  xltnegi  13373  supxrre  13484  infxrre  13494  elioo5  13561  elfz5  13675  elfzm11  13756  predfz  13814  flbi  13983  flbi2  13984  fldiv4lem1div2uz2  14003  fznnfl  14029  zmodid2  14066  2submod  14102  lt2sq  14303  le2sq  14304  sqlecan  14380  bcval5  14489  pfxsuffeqwrdeq  14875  shftfib  15254  sgn3da  15283  mulre  15317  cnpart  15436  01sqrexlem6  15443  sqrmo  15447  elicc4abs  15516  abs2difabs  15531  cau4  15553  limsupgre  15677  clim2  15700  ello1mpt2  15718  lo1resb  15760  o1resb  15762  climeq  15763  climmpt2  15769  isercoll  15864  caucvgb  15876  fsumabs  15997  isumshft  16037  geomulcvg  16074  absefib  16395  dvdsval3  16455  addmulmodb  16464  dvdsabseq  16512  dvdsflip  16516  dvdsssfz1  16517  mod2eq1n2dvds  16546  ndvdsadd  16609  bitscmp  16637  smupvallem  16682  dvdssq  16771  lcmdvds  16812  ncoprmgcdgt1b  16855  isprm3  16887  isprm5  16912  phiprmpw  16982  prmdiv  16991  pc11  17087  pcz  17088  pockthlem  17112  prmreclem2  17124  prmreclem4  17126  prmreclem6  17128  1arith  17134  vdwapun  17181  rami  17222  ramcl  17236  pwsle  17693  ercpbllem  17749  invsym  17966  funcres2c  18107  latnle  18676  grpinvcnv  19246  subgacs  19400  eqger  19419  ghmqusker  19531  gexdvds2  19829  pgpfi1  19839  pgpfi  19849  lsmass  19913  lssnle  19918  lsmdisj3b  19934  lsmhash  19949  ablsubadd  20053  gsumval3lem2  20150  subgdmdprd  20280  pgpfac1lem2  20321  dvdsr02  20632  issubrg3  20882  isdomn3  20996  drngid2  21040  sdrgunit  21083  sdrgacs  21088  lssacs  21272  prmirred  21810  chrdvds  21862  chrcong  21863  chrnzr  21866  znleval  21890  znleval2  21891  cygznlem3  21905  frlmbas  22091  elfilspd  22139  lindfmm  22163  islindf4  22174  islindf5  22175  psrbaglefi  22264  coe1mul2lem1  22616  mdetunilem9  22965  matunitlindflem1  23024  matunitlindflem2  23025  matunitlindf  23026  isneip  23453  neiptopnei  23480  lpdifsn  23491  restopnb  23523  restopn2  23525  restdis  23526  restperf  23532  lmbr2  23607  cncls2  23621  cnprest  23637  cnprest2  23638  iscnrm2  23686  ist0-2  23692  ist1-3  23697  ishaus2  23699  cmpfi  23756  dfconn2  23767  1stccnp  23811  subislly  23830  hausmapdom  23849  tx1cn  23958  tx2cn  23959  txcnmpt  23973  txrest  23980  hauseqlcld  23995  tgqtop  24061  qtopcld  24062  ordthmeolem  24150  trfil2  24236  trfil3  24237  trnei  24241  ufildr  24280  fmfg  24298  rnelfm  24302  fmfnfm  24307  elflim  24320  flimrest  24332  cnflf  24351  cnflf2  24352  ptcmplem2  24402  ghmcnp  24464  tsmssubm  24492  iscfilu  24636  xmetgt0  24707  prdsxmetlem  24717  blcomps  24742  blcom  24743  xblpnfps  24744  xblpnf  24745  blpnf  24746  xmeter  24782  setsxms  24828  imasf1obl  24837  stdbdbl  24866  metrest  24873  metuel2  24914  dscopn  24922  xrtgioo  25156  metdstri  25201  cnmpopc  25279  iihalf2  25284  icopnfhmeo  25294  evth2  25311  lmmbr3  25611  iscau3  25629  metcld  25657  cfilucfil3  25671  srabn  25711  rrxmet  25759  minveclem4  25783  evthicc2  25811  ovolgelb  25831  shft2rab  25859  ovolshftlem1  25860  sca2rab  25863  ovolscalem1  25864  ioombl1lem4  25912  mbfmulc2lem  25998  ismbf3d  26005  mbfsup  26015  mbfinf  26016  i1f1lem  26040  i1fmulclem  26053  mbfi1fseqlem4  26069  itg2seq  26093  ditgneg  26207  limcdif  26226  limcnlp  26228  cnplimc  26237  rolle  26340  mvth  26342  dvne0  26361  lhop1lem  26363  itgsubst  26399  mdegle0  26425  deg1leb  26443  deg1le0  26459  q1peqb  26504  coemulhi  26603  dgrlt  26615  plydivlem3  26646  vieta1lem2  26664  aannenlem1  26685  ulmres  26745  reefiso  26805  pilem3  26810  ellogdm  26997  root1eq1  27113  angpieqvdlem  27186  angpieqvdlem2  27187  quad2  27197  1cubr  27200  quart  27219  rlimcnp  27323  wilthlem2  27426  isppw  27471  dvdsflsumcom  27545  fsumvma  27570  logfac2  27574  chpchtsum  27576  dchrmulcl  27606  dchrresb  27616  bclbnd  27637  bposlem1  27641  bposlem5  27645  gausslemma2dlem0c  27715  lgsquadlem1  27737  m1lgs  27745  2lgsoddprmlem2  27766  dchrisumlem3  27848  dchrisum0lem1  27873  ltsval2  28043  noextenddif  28055  lesloe  28141  lestri3  28142  eqcuts  28201  elmade2  28274  ltadds1  28408  negsunif  28471  ltsubs1  28492  ltsubadds2d  28506  mulsproplem12  28543  ltmuls2  28587  ltmuls1d  28589  divmulsw  28609  ltdivmuls2wd  28616  oniso  28687  n0subs  28779  n0lesltp1  28782  elzn0s  28814  avglts1d  28869  avglts2d  28870  bdaypw2n0bndlem  28879  z12sge0  28899  dfz12s2  28904  elreno2  28911  tgjustr  28966  trgcgrg  29008  lnrot1  29121  islnopp  29245  elplng  29288  plngcplem  29293  ismidb  29313  islmib  29322  axsegconlem6  29530  axeuclidlem  29570  axcontlem2  29573  axcontlem4  29575  axcontlem12  29583  lfuhgr2  29757  ausgrusgrb  29776  nb3grpr2  29994  cplgr2v  30043  umgr2v2enb1  30137  crctcsh  30443  clwwlknonwwlknonb  30727  eupth2lems  30869  nmoreltpnf  31401  isblo2  31415  nmlnogt0  31429  phoeqi  31489  ubthlem2  31503  hire  31726  normgt0  31759  ho01i  32460  ho02i  32461  hoeq1  32462  hoeq2  32463  nmopreltpnf  32501  adjeq  32567  leop  32755  leopmul2i  32767  pjnormssi  32800  pjimai  32808  jplem1  32900  mddmd2  32941  mdslmd1lem1  32957  mdslmd1lem2  32958  superpos  32986  atnssm0  33008  dmdbr5ati  33054  disjunsn  33260  fcoinvbr  33271  ofpreima  33331  funcnv5mpt  33333  suppiniseg  33350  isoun  33366  fpwrelmapffslem  33394  fpwrelmap  33395  iocinioc2  33441  xrdifh  33442  nndiffz1  33448  xdivmul  33561  cntzsnid  33711  cntrval2  33802  isarchi2  33816  isunitc  33872  erler  33896  rlocisunit  33907  elrsp  33997  lsmsnpridl  34021  lsmssass  34023  esplyind  34277  finexttrb  34367  algextdeglem6  34424  algextdeglem7  34425  smatrcl  34498  rhmpreimacnlem  34586  sqsscirc2  34611  xrmulc1cn  34632  esumfsup  34772  1stmbfm  34962  2ndmbfm  34963  mbfmcnt  34970  eulerpartlems  35062  eulerpartlemd  35068  ballotlemfc0  35195  ballotlemfcc  35196  ballotlemsima  35218  ballotlemfrcn0  35232  reprinfz1  35321  reprdifc  35326  bnj1173  35702  fwfffunres  35788  ecscottd  35844  fineqvnttrclse  35892  kardcard2  35934  j00smo  36005  vonf1wev  36036  vonf1owevOLD  36038  zltp1ne  36057  erdszelem7  36129  erdszelem9  36131  iscvm  36191  cvmlift3lem4  36254  rexxfr3dALT  36571  fscgr  37023  seglelin  37059  btwnoutside  37068  lineunray  37090  cldbnd  37292  isfne4  37306  fneval  37318  filnetlem4  37347  nndivsub  37423  bj-gabima  38031  dfgcd3  38437  fvineqsneu  38526  wl-sbhbt  38678  wl-sbcom2d  38685  wl-sbalnae  38686  sin2h  38725  cos2h  38726  ptrest  38729  poimirlem3  38733  poimirlem4  38734  poimirlem22  38752  poimirlem27  38757  mblfinlem3  38769  mblfinlem4  38770  ismblfin  38771  itg2addnclem  38781  itg2addnclem2  38782  itg2gt0cn  38785  iblabsnclem  38793  ftc1anclem6  38808  areacirclem2  38819  areacirclem5  38822  areacirc  38823  mettrifi  38883  drngoi  39077  eldm4  39405  exanres2  39427  disjecxrn  39536  exeupre  39615  brcoss2  39646  br1cossres2  39654  eldmcoss2  39673  eldm1cossres2  39675  brcosscnv2  39687  erimeq2  39887  disjqmap  39951  disjlem19  40028  prter3  40131  islshpat  40266  lsatnle  40293  ellkr2  40340  lshpkr  40366  lkr0f2  40410  lduallkr3  40411  lkreqN  40419  cvrval2  40523  isat3  40556  glbconN  40626  hlrelat5N  40650  cvrval4N  40663  atlt  40686  1cvrco  40721  pmaple  41010  isline2  41023  isline4N  41026  elpaddn0  41049  elpadd2at2  41056  cdlemkid4  42183  dia0  42301  cdlemm10N  42367  dibglbN  42415  dihmeetlem4preN  42555  dochkrshp3  42637  dvh4dimlem  42692  lcfl5  42745  mapdpglem3  42924  mapdheq  42977  hdmap1eq  43050  hdmapval2lem  43080  hdmapoc  43180  hlhillcs  43207  lcmineqlem18  43288  dvdsexpb  43580  renegadd  43616  resubadd  43623  redivmuld  43689  mulgt0b1d  43729  fsuppssind  43814  frlmnzcoordsca  43851  fz1eqin  43973  diophin  43976  jm2.19  44193  rmxdiophlem  44215  pw2f1ocnv  44237  wepwsolem  44242  gicabl  44294  idomodle  44385  onsupmaxb  44433  cantnf2  44519  tfsconcatb0  44538  tfsnfin  44546  ntrclsfveq2  45253  ntrclsss  45255  ntrclsk4  45264  extoimad  45356  radcnvrat  45490  bcc0  45516  hashomiso  46210  supxrre3rnmpt  46644  clim2f  46851  clim2f2  46885  liminfreuzlem  47017  liminfltlem  47019  xlimmnflimsup2  47067  xlimpnfliminf2  47076  xlimlimsupleliminf  47078  opprb  48306  funbrafv2b  48434  dfafn5a  48435  leaddsuble  48572  mod2addne  48645  iccpartgtprec  48707  flsqrt  48883  dfeven2  48952  dfodd3  48953  lindslinindimp2lem4  49778  snlindsntor  49788  regt1loggt0  49853  elbigo2  49869  elbigolo1  49874  fldivexpfllog2  49882  nnlog2ge0lt1  49883  blenpw2m1  49896  naryfvalelwrdf  49950  isprsd  50274  resccatlem  50392  functhinclem1  50784  thincciso  50793  thinciso  50810  isinito2lem  50838  fulltermc  50851  prstcprs  50903  oduoppcciso  50909  postc  50912  lmdran  51059  cmdlan  51060