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  2481  sbcom3  2511  sbal1  2533  sbal2  2534  2reu4lem  4522  issn  4832  disjprg  5139  reuhypd  5419  snelpwg  5447  ordtri3  6420  ordsssuc  6473  iota1  6538  funbrfv2b  6966  dffn5  6967  feqmptdf  6979  unima  6984  dmfco  7005  fneqeql  7066  f1ompt  7131  dff13  7275  fliftcnv  7331  soisores  7347  isotr  7356  isoini  7358  caovord3  7646  releldm2  8068  fimaproj  8160  brtpos  8260  tpostpos  8271  oe1m  8583  oawordri  8588  oalimcl  8598  omlimcl  8616  omabs  8689  iserd  8771  qliftel  8840  qliftfun  8842  qliftf  8845  ecopovsym  8859  pw2f1olem  9116  mapen  9181  findcard3  9318  suppeqfsuppbi  9419  mapfien  9448  supisolem  9513  cantnflem1  9729  wemapwe  9737  rankr1clem  9860  rankr1c  9861  ranklim  9884  r1pwALT  9886  r1pwcl  9887  isfin1-2  10425  isfin1-4  10427  fin71num  10437  axdc3lem2  10491  ltmnq  11012  prlem936  11087  ltsosr  11134  ltasr  11140  xrlenlt  11326  ltxrlt  11331  letri3  11346  ne0gt0  11366  subadd  11511  ltsubadd2  11734  lesubadd2  11736  suble  11741  ltsub23  11743  ltaddpos2  11754  ltsubpos  11755  subge02  11779  ltord2  11792  leord2  11793  ltaddsublt  11890  divmul  11925  divmul3  11927  rec11r  11966  ltdiv1  12132  ltdivmul2  12145  ledivmul2  12147  ltrec  12150  ltdiv2  12154  negfi  12217  negiso  12248  nnle1eq1  12296  avgle1  12506  avgle2  12507  avgle  12508  nn0le0eq0  12554  elz2  12631  znnnlt1  12644  zleltp1  12668  difrp  13073  xrltlen  13188  dfle2  13189  xrletri3  13196  xgepnf  13207  xlemnf  13209  qbtwnre  13241  xltnegi  13258  supxrre  13369  infxrre  13378  elioo5  13444  elfz5  13556  elfzm11  13635  predfz  13693  flbi  13856  flbi2  13857  fldiv4lem1div2uz2  13876  fznnfl  13902  zmodid2  13939  2submod  13973  lt2sq  14173  le2sq  14174  sqlecan  14248  bcval5  14357  pfxsuffeqwrdeq  14736  shftfib  15111  mulre  15160  cnpart  15279  01sqrexlem6  15286  sqrmo  15290  elicc4abs  15358  abs2difabs  15373  cau4  15395  limsupgre  15517  clim2  15540  ello1mpt2  15558  lo1resb  15600  o1resb  15602  climeq  15603  climmpt2  15609  isercoll  15704  caucvgb  15716  fsumabs  15837  isumshft  15875  geomulcvg  15912  absefib  16234  dvdsval3  16294  addmulmodb  16303  dvdsabseq  16350  dvdsflip  16354  dvdsssfz1  16355  mod2eq1n2dvds  16384  ndvdsadd  16447  bitscmp  16475  smupvallem  16520  dvdssq  16604  lcmdvds  16645  ncoprmgcdgt1b  16688  isprm3  16720  isprm5  16744  phiprmpw  16813  prmdiv  16822  pc11  16918  pcz  16919  pockthlem  16943  prmreclem2  16955  prmreclem4  16957  prmreclem6  16959  1arith  16965  vdwapun  17012  rami  17053  ramcl  17067  pwsle  17537  ercpbllem  17593  invsym  17806  funcres2c  17948  latnle  18518  grpinvcnv  19024  subgacs  19179  eqger  19196  ghmqusker  19305  gexdvds2  19603  pgpfi1  19613  pgpfi  19623  lsmass  19687  lssnle  19692  lsmdisj3b  19708  lsmhash  19723  ablsubadd  19827  gsumval3lem2  19924  subgdmdprd  20054  pgpfac1lem2  20095  dvdsr02  20372  issubrg3  20600  isdomn3  20715  drngid2  20752  sdrgunit  20797  sdrgacs  20802  lssacs  20965  prmirred  21485  chrdvds  21541  chrcong  21542  chrnzr  21545  znleval  21573  znleval2  21574  cygznlem3  21588  frlmbas  21775  elfilspd  21823  lindfmm  21847  islindf4  21858  islindf5  21859  psrbaglefi  21946  coe1mul2lem1  22270  mdetunilem9  22626  isneip  23113  neiptopnei  23140  lpdifsn  23151  restopnb  23183  restopn2  23185  restdis  23186  restperf  23192  lmbr2  23267  cncls2  23281  cnprest  23297  cnprest2  23298  iscnrm2  23346  ist0-2  23352  ist1-3  23357  ishaus2  23359  cmpfi  23416  dfconn2  23427  1stccnp  23470  subislly  23489  hausmapdom  23508  tx1cn  23617  tx2cn  23618  txcnmpt  23632  txrest  23639  hauseqlcld  23654  tgqtop  23720  qtopcld  23721  ordthmeolem  23809  trfil2  23895  trfil3  23896  trnei  23900  ufildr  23939  fmfg  23957  rnelfm  23961  fmfnfm  23966  elflim  23979  flimrest  23991  cnflf  24010  cnflf2  24011  ptcmplem2  24061  ghmcnp  24123  tsmssubm  24151  iscfilu  24297  xmetgt0  24368  prdsxmetlem  24378  blcomps  24403  blcom  24404  xblpnfps  24405  xblpnf  24406  blpnf  24407  xmeter  24443  setsxms  24491  imasf1obl  24501  stdbdbl  24530  metrest  24537  metuel2  24578  dscopn  24586  xrtgioo  24828  metdstri  24873  cnmpopc  24955  iihalf2  24961  icopnfhmeo  24974  evth2  24992  lmmbr3  25294  iscau3  25312  metcld  25340  cfilucfil3  25354  srabn  25394  rrxmet  25442  minveclem4  25466  evthicc2  25495  ovolgelb  25515  shft2rab  25543  ovolshftlem1  25544  sca2rab  25547  ovolscalem1  25548  ioombl1lem4  25596  mbfmulc2lem  25682  ismbf3d  25689  mbfsup  25699  mbfinf  25700  i1f1lem  25724  i1fmulclem  25737  mbfi1fseqlem4  25753  itg2seq  25777  ditgneg  25892  limcdif  25911  limcnlp  25913  cnplimc  25922  rolle  26028  mvth  26031  dvne0  26050  lhop1lem  26052  itgsubst  26090  mdegle0  26116  deg1leb  26134  deg1le0  26150  q1peqb  26195  coemulhi  26293  dgrlt  26306  plydivlem3  26337  vieta1lem2  26353  aannenlem1  26370  ulmres  26431  reefiso  26492  pilem3  26497  ellogdm  26681  root1eq1  26798  angpieqvdlem  26871  angpieqvdlem2  26872  quad2  26882  1cubr  26885  quart  26904  rlimcnp  27008  wilthlem2  27112  isppw  27157  dvdsflsumcom  27231  fsumvma  27257  logfac2  27261  chpchtsum  27263  dchrmulcl  27293  dchrresb  27303  bclbnd  27324  bposlem1  27328  bposlem5  27332  gausslemma2dlem0c  27402  lgsquadlem1  27424  m1lgs  27432  2lgsoddprmlem2  27453  dchrisumlem3  27535  dchrisum0lem1  27560  sltval2  27701  noextenddif  27713  sleloe  27799  sletri3  27800  eqscut  27850  elmade2  27907  sltadd1  28025  negsunif  28087  sltsub1  28106  sltsubadd2d  28120  mulsproplem12  28153  sltmul2  28197  sltmul1d  28199  divsmulw  28218  sltdivmul2wd  28225  n0subs  28360  elzn0s  28384  tgjustr  28482  trgcgrg  28523  lnrot1  28631  islnopp  28747  ismidb  28786  islmib  28795  axsegconlem6  28937  axeuclidlem  28977  axcontlem2  28980  axcontlem4  28982  axcontlem12  28990  ausgrusgrb  29182  nb3grpr2  29400  cplgr2v  29449  umgr2v2enb1  29544  crctcsh  29844  clwwlknonwwlknonb  30125  eupth2lems  30257  nmoreltpnf  30788  isblo2  30802  nmlnogt0  30816  phoeqi  30876  ubthlem2  30890  hire  31113  normgt0  31146  ho01i  31847  ho02i  31848  hoeq1  31849  hoeq2  31850  nmopreltpnf  31888  adjeq  31954  leop  32142  leopmul2i  32154  pjnormssi  32187  pjimai  32195  jplem1  32287  mddmd2  32328  mdslmd1lem1  32344  mdslmd1lem2  32345  superpos  32373  atnssm0  32395  dmdbr5ati  32441  disjunsn  32607  fcoinvbr  32618  ofpreima  32675  funcnv5mpt  32678  suppiniseg  32695  isoun  32711  fpwrelmapffslem  32743  fpwrelmap  32744  iocinioc2  32781  xrdifh  32782  nndiffz1  32788  xdivmul  32907  cntzsnid  33072  isarchi2  33192  erler  33269  elrsp  33400  lsmsnpridl  33426  lsmssass  33430  r1pid2OLD  33629  finexttrb  33715  algextdeglem6  33763  algextdeglem7  33764  smatrcl  33795  rhmpreimacnlem  33883  sqsscirc2  33908  xrmulc1cn  33929  esumfsup  34071  1stmbfm  34262  2ndmbfm  34263  mbfmcnt  34270  eulerpartlems  34362  eulerpartlemd  34368  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemsima  34518  ballotlemfrcn0  34532  sgn3da  34544  reprinfz1  34637  reprdifc  34642  bnj1173  35016  zltp1ne  35115  lfuhgr2  35124  erdszelem7  35202  erdszelem9  35204  iscvm  35264  cvmlift3lem4  35327  rexxfr3dALT  35644  fscgr  36081  seglelin  36117  btwnoutside  36126  lineunray  36148  cldbnd  36327  isfne4  36341  fneval  36353  filnetlem4  36382  nndivsub  36458  bj-gabima  36941  dfgcd3  37325  fvineqsneu  37412  wl-sbhbt  37555  wl-sbcom2d  37562  wl-sbalnae  37563  wl-ax11-lem8  37593  sin2h  37617  cos2h  37618  matunitlindflem1  37623  matunitlindflem2  37624  matunitlindf  37625  ptrest  37626  poimirlem3  37630  poimirlem4  37631  poimirlem22  37649  poimirlem27  37654  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  itg2addnclem  37678  itg2addnclem2  37679  itg2gt0cn  37682  iblabsnclem  37690  ftc1anclem6  37705  areacirclem2  37716  areacirclem5  37719  areacirc  37720  mettrifi  37764  drngoi  37958  eldm4  38275  exanres2  38298  disjecxrn  38390  brcoss2  38433  br1cossres2  38441  eldmcoss2  38460  eldm1cossres2  38462  brcosscnv2  38474  erimeq2  38679  disjlem19  38802  prter3  38883  islshpat  39018  lsatnle  39045  ellkr2  39092  lshpkr  39118  lkr0f2  39162  lduallkr3  39163  lkreqN  39171  cvrval2  39275  isat3  39308  glbconN  39378  glbconNOLD  39379  hlrelat5N  39403  cvrval4N  39416  atlt  39439  1cvrco  39474  pmaple  39763  isline2  39776  isline4N  39779  elpaddn0  39802  elpadd2at2  39809  cdlemkid4  40936  dia0  41054  cdlemm10N  41120  dibglbN  41168  dihmeetlem4preN  41308  dochkrshp3  41390  dvh4dimlem  41445  lcfl5  41498  mapdpglem3  41677  mapdheq  41730  hdmap1eq  41803  hdmapval2lem  41833  hdmapoc  41933  hlhillcs  41964  lcmineqlem18  42047  dvdsexpb  42370  renegadd  42402  resubadd  42409  mulgt0b2d  42490  fsuppssind  42603  fz1eqin  42780  diophin  42783  jm2.19  43005  rmxdiophlem  43027  pw2f1ocnv  43049  wepwsolem  43054  gicabl  43111  idomodle  43203  onsupmaxb  43251  cantnf2  43338  tfsconcatb0  43357  tfsnfin  43365  ntrclsfveq2  44074  ntrclsss  44076  ntrclsk4  44085  extoimad  44177  radcnvrat  44333  bcc0  44359  supxrre3rnmpt  45440  clim2f  45651  clim2f2  45685  liminfreuzlem  45817  liminfltlem  45819  xlimmnflimsup2  45867  xlimpnfliminf2  45876  xlimlimsupleliminf  45878  opprb  47043  funbrafv2b  47171  dfafn5a  47172  leaddsuble  47309  iccpartgtprec  47407  flsqrt  47580  dfeven2  47636  dfodd3  47637  lindslinindimp2lem4  48378  snlindsntor  48388  regt1loggt0  48457  elbigo2  48473  elbigolo1  48478  fldivexpfllog2  48486  nnlog2ge0lt1  48487  blenpw2m1  48500  naryfvalelwrdf  48554  isprsd  48852  functhinclem1  49093  thincciso  49102  thinciso  49117  fulltermc  49143  prstcprs  49164  oduoppcciso  49170  postc  49173