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  544  mpbirand  705  sb3b  2501  sbcom3  2548  sbal1  2572  sbal2  2573  sbal2OLD  2574  2reu4lem  4465  issn  4763  disjprgw  5061  disjprg  5062  reuhypd  5320  ordtri3  6227  ordsssuc  6277  iota1  6332  funbrfv2b  6723  dffn5  6724  feqmptdf  6735  unima  6739  dmfco  6757  fneqeql  6816  f1ompt  6875  dff13  7013  fliftcnv  7064  soisores  7080  isotr  7089  isoini  7091  caovord3  7361  releldm2  7742  fimaproj  7829  brtpos  7901  tpostpos  7912  oe1m  8171  oawordri  8176  oalimcl  8186  omlimcl  8204  omabs  8274  iserd  8315  qliftel  8380  qliftfun  8382  qliftf  8385  ecopovsym  8399  pw2f1olem  8621  mapen  8681  suppeqfsuppbi  8847  mapfien  8871  supisolem  8937  cantnflem1  9152  wemapwe  9160  rankr1clem  9249  rankr1c  9250  ranklim  9273  r1pwALT  9275  r1pwcl  9276  isfin1-2  9807  isfin1-4  9809  fin71num  9819  axdc3lem2  9873  ltmnq  10394  prlem936  10469  ltsosr  10516  ltasr  10522  xrlenlt  10706  ltxrlt  10711  letri3  10726  ne0gt0  10745  subadd  10889  ltsubadd2  11111  lesubadd2  11113  suble  11118  ltsub23  11120  ltaddpos2  11131  ltsubpos  11132  subge02  11156  ltord2  11169  leord2  11170  ltaddsublt  11267  divmul  11301  divmul3  11303  rec11r  11339  ltdiv1  11504  ltdivmul2  11517  ledivmul2  11519  ltrec  11522  ltdiv2  11526  negfi  11589  negiso  11621  nnle1eq1  11668  avgle1  11878  avgle2  11879  avgle  11880  nn0le0eq0  11926  elz2  12000  znnnlt1  12010  zleltp1  12034  difrp  12428  xrltlen  12540  dfle2  12541  xrletri3  12548  xgepnf  12559  xlemnf  12561  qbtwnre  12593  xltnegi  12610  supxrre  12721  infxrre  12730  elioo5  12795  elfz5  12901  elfzm11  12979  predfz  13033  flbi  13187  flbi2  13188  fldiv4lem1div2uz2  13207  fznnfl  13231  zmodid2  13268  2submod  13301  lt2sq  13499  le2sq  13500  sqlecan  13572  bcval5  13679  pfxsuffeqwrdeq  14060  shftfib  14431  mulre  14480  cnpart  14599  sqrlem6  14607  sqrmo  14611  elicc4abs  14679  abs2difabs  14694  cau4  14716  limsupgre  14838  clim2  14861  ello1mpt2  14879  lo1resb  14921  o1resb  14923  climeq  14924  climmpt2  14930  isercoll  15024  caucvgb  15036  fsumabs  15156  isumshft  15194  geomulcvg  15232  absefib  15551  dvdsval3  15611  dvdsabseq  15663  dvdsflip  15667  dvdsssfz1  15668  mod2eq1n2dvds  15696  ndvdsadd  15761  bitscmp  15787  smupvallem  15832  dvdssq  15911  lcmdvds  15952  ncoprmgcdgt1b  15995  isprm3  16027  isprm5  16051  phiprmpw  16113  prmdiv  16122  pc11  16216  pcz  16217  pockthlem  16241  prmreclem2  16253  prmreclem4  16255  prmreclem6  16257  1arith  16263  vdwapun  16310  rami  16351  ramcl  16365  pwsle  16765  ercpbllem  16821  invsym  17032  funcres2c  17171  latnle  17695  grpinvcnv  18167  subgacs  18313  eqger  18330  gexdvds2  18710  pgpfi1  18720  pgpfi  18730  lsmass  18795  lssnle  18800  lsmdisj3b  18816  lsmhash  18831  ablsubadd  18932  gsumval3lem2  19026  subgdmdprd  19156  pgpfac1lem2  19197  dvdsr02  19406  drngid2  19518  issubrg3  19563  sdrgacs  19580  lssacs  19739  psrbaglefi  20152  coe1mul2lem1  20435  prmirred  20642  chrdvds  20675  chrcong  20676  chrnzr  20677  znleval  20701  znleval2  20702  cygznlem3  20716  frlmbas  20899  elfilspd  20947  lindfmm  20971  islindf4  20982  islindf5  20983  mdetunilem9  21229  isneip  21713  neiptopnei  21740  lpdifsn  21751  restopnb  21783  restopn2  21785  restdis  21786  restperf  21792  lmbr2  21867  cncls2  21881  cnprest  21897  cnprest2  21898  iscnrm2  21946  ist0-2  21952  ist1-3  21957  ishaus2  21959  cmpfi  22016  dfconn2  22027  1stccnp  22070  subislly  22089  hausmapdom  22108  tx1cn  22217  tx2cn  22218  txcnmpt  22232  txrest  22239  hauseqlcld  22254  tgqtop  22320  qtopcld  22321  ordthmeolem  22409  trfil2  22495  trfil3  22496  trnei  22500  ufildr  22539  fmfg  22557  rnelfm  22561  fmfnfm  22566  elflim  22579  flimrest  22591  cnflf  22610  cnflf2  22611  ptcmplem2  22661  ghmcnp  22723  tsmssubm  22751  iscfilu  22897  xmetgt0  22968  prdsxmetlem  22978  blcomps  23003  blcom  23004  xblpnfps  23005  xblpnf  23006  blpnf  23007  xmeter  23043  setsxms  23089  imasf1obl  23098  stdbdbl  23127  metrest  23134  metuel2  23175  dscopn  23183  xrtgioo  23414  metdstri  23459  cnmpopc  23532  iihalf2  23537  icopnfhmeo  23547  evth2  23564  lmmbr3  23863  iscau3  23881  metcld  23909  cfilucfil3  23923  srabn  23963  rrxmet  24011  minveclem4  24035  evthicc2  24061  ovolgelb  24081  shft2rab  24109  ovolshftlem1  24110  sca2rab  24113  ovolscalem1  24114  ioombl1lem4  24162  mbfmulc2lem  24248  ismbf3d  24255  mbfsup  24265  mbfinf  24266  i1f1lem  24290  i1fmulclem  24303  mbfi1fseqlem4  24319  itg2seq  24343  ditgneg  24455  limcdif  24474  limcnlp  24476  cnplimc  24485  rolle  24587  mvth  24589  dvne0  24608  lhop1lem  24610  itgsubst  24646  mdegle0  24671  deg1leb  24689  deg1le0  24705  q1peqb  24748  coemulhi  24844  dgrlt  24856  plydivlem3  24884  vieta1lem2  24900  aannenlem1  24917  ulmres  24976  reefiso  25036  pilem3  25041  ellogdm  25222  root1eq1  25336  angpieqvdlem  25406  angpieqvdlem2  25407  quad2  25417  1cubr  25420  quart  25439  rlimcnp  25543  wilthlem2  25646  isppw  25691  dvdsflsumcom  25765  fsumvma  25789  logfac2  25793  chpchtsum  25795  dchrmulcl  25825  dchrresb  25835  bclbnd  25856  bposlem1  25860  bposlem5  25864  gausslemma2dlem0c  25934  lgsquadlem1  25956  m1lgs  25964  2lgsoddprmlem2  25985  dchrisumlem3  26067  dchrisum0lem1  26092  tgjustr  26260  trgcgrg  26301  lnrot1  26409  islnopp  26525  ismidb  26564  islmib  26573  axsegconlem6  26708  axeuclidlem  26748  axcontlem2  26751  axcontlem4  26753  axcontlem12  26761  ausgrusgrb  26950  nb3grpr2  27165  cplgr2v  27214  umgr2v2enb1  27308  crctcsh  27602  clwwlknonwwlknonb  27885  eupth2lems  28017  nmoreltpnf  28546  isblo2  28560  nmlnogt0  28574  phoeqi  28634  ubthlem2  28648  hire  28871  normgt0  28904  ho01i  29605  ho02i  29606  hoeq1  29607  hoeq2  29608  nmopreltpnf  29646  adjeq  29712  leop  29900  leopmul2i  29912  pjnormssi  29945  pjimai  29953  jplem1  30045  mddmd2  30086  mdslmd1lem1  30102  mdslmd1lem2  30103  superpos  30131  atnssm0  30153  dmdbr5ati  30199  disjunsn  30344  fcoinvbr  30358  ofpreima  30410  funcnv5mpt  30413  isoun  30437  fpwrelmapffslem  30468  fpwrelmap  30469  iocinioc2  30502  xrdifh  30503  nndiffz1  30509  xdivmul  30601  cntzsnid  30696  isarchi2  30814  lsmsnpridl  30948  finexttrb  31052  smatrcl  31061  sqsscirc2  31152  xrmulc1cn  31173  esumfsup  31329  1stmbfm  31518  2ndmbfm  31519  mbfmcnt  31526  eulerpartlems  31618  eulerpartlemd  31624  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemsima  31773  ballotlemfrcn0  31787  sgn3da  31799  reprinfz1  31893  reprdifc  31898  bnj1173  32274  zltp1ne  32348  lfuhgr2  32365  erdszelem7  32444  erdszelem9  32446  iscvm  32506  cvmlift3lem4  32569  sltval2  33163  noextenddif  33175  sleloe  33233  sletri3  33234  fscgr  33541  seglelin  33577  btwnoutside  33586  lineunray  33608  cldbnd  33674  isfne4  33688  fneval  33700  filnetlem4  33729  nndivsub  33805  dfgcd3  34608  fvineqsneu  34695  wl-sbhbt  34805  wl-sbcom2d  34812  wl-sbalnae  34813  wl-ax11-lem8  34839  wl-dfrmof  34870  sin2h  34897  cos2h  34898  matunitlindflem1  34903  matunitlindflem2  34904  matunitlindf  34905  ptrest  34906  poimirlem3  34910  poimirlem4  34911  poimirlem22  34929  poimirlem27  34934  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  itg2addnclem  34958  itg2addnclem2  34959  itg2gt0cn  34962  iblabsnclem  34970  ftc1anclem6  34987  areacirclem2  34998  areacirclem5  35001  areacirc  35002  mettrifi  35047  drngoi  35244  eldm4  35546  exanres2  35569  brcoss2  35692  br1cossres2  35700  eldmcoss2  35714  eldm1cossres2  35716  brcosscnv2  35728  erim2  35926  prter3  36033  islshpat  36168  lsatnle  36195  ellkr2  36242  lshpkr  36268  lkr0f2  36312  lduallkr3  36313  lkreqN  36321  cvrval2  36425  isat3  36458  glbconN  36528  hlrelat5N  36552  cvrval4N  36565  atlt  36588  1cvrco  36623  pmaple  36912  isline2  36925  isline4N  36928  elpaddn0  36951  elpadd2at2  36958  cdlemkid4  38085  dia0  38203  cdlemm10N  38269  dibglbN  38317  dihmeetlem4preN  38457  dochkrshp3  38539  dvh4dimlem  38594  lcfl5  38647  mapdpglem3  38826  mapdheq  38879  hdmap1eq  38952  hdmapval2lem  38982  hdmapoc  39082  hlhillcs  39109  renegadd  39251  resubadd  39258  fz1eqin  39415  diophin  39418  jm2.19  39639  rmxdiophlem  39661  pw2f1ocnv  39683  wepwsolem  39691  gicabl  39748  idomodle  39845  isdomn3  39853  ntrclsfveq2  40460  ntrclsss  40462  ntrclsk4  40471  extoimad  40564  radcnvrat  40695  bcc0  40721  supxrre3rnmpt  41752  clim2f  41966  clim2f2  42000  liminfreuzlem  42132  liminfltlem  42134  xlimmnflimsup2  42182  xlimpnfliminf2  42191  xlimlimsupleliminf  42193  opprb  43315  funbrafv2b  43407  dfafn5a  43408  leaddsuble  43546  iccpartgtprec  43629  flsqrt  43805  dfeven2  43863  dfodd3  43864  lindslinindimp2lem4  44565  snlindsntor  44575  regt1loggt0  44645  elbigo2  44661  elbigolo1  44666  fldivexpfllog2  44674  nnlog2ge0lt1  44675  blenpw2m1  44688