Theorem bitr4d 281

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3bitr2d  306  3bitr2rd  307  3bitr4d  310  3bitr4rd  311  bianabs  542  mpbirand  704  sb3b  2475  sbcom3  2508  sbal1  2531  sbal2  2532  2reu4lem  4470  issn  4777  disjprgw  5087  disjprg  5088  reuhypd  5362  snelpwg  5387  ordtri3  6338  ordsssuc  6390  iota1  6456  funbrfv2b  6883  dffn5  6884  feqmptdf  6895  unima  6899  dmfco  6920  fneqeql  6979  f1ompt  7041  dff13  7184  fliftcnv  7238  soisores  7254  isotr  7263  isoini  7265  caovord3  7547  releldm2  7952  fimaproj  8043  brtpos  8121  tpostpos  8132  oe1m  8447  oawordri  8452  oalimcl  8462  omlimcl  8480  omabs  8552  iserd  8595  qliftel  8660  qliftfun  8662  qliftf  8665  ecopovsym  8679  pw2f1olem  8941  mapen  9006  findcard3  9150  suppeqfsuppbi  9240  mapfien  9265  supisolem  9330  cantnflem1  9546  wemapwe  9554  rankr1clem  9677  rankr1c  9678  ranklim  9701  r1pwALT  9703  r1pwcl  9704  isfin1-2  10242  isfin1-4  10244  fin71num  10254  axdc3lem2  10308  ltmnq  10829  prlem936  10904  ltsosr  10951  ltasr  10957  xrlenlt  11141  ltxrlt  11146  letri3  11161  ne0gt0  11181  subadd  11325  ltsubadd2  11547  lesubadd2  11549  suble  11554  ltsub23  11556  ltaddpos2  11567  ltsubpos  11568  subge02  11592  ltord2  11605  leord2  11606  ltaddsublt  11703  divmul  11737  divmul3  11739  rec11r  11775  ltdiv1  11940  ltdivmul2  11953  ledivmul2  11955  ltrec  11958  ltdiv2  11962  negfi  12025  negiso  12056  nnle1eq1  12104  avgle1  12314  avgle2  12315  avgle  12316  nn0le0eq0  12362  elz2  12438  znnnlt1  12448  zleltp1  12472  difrp  12869  xrltlen  12981  dfle2  12982  xrletri3  12989  xgepnf  13000  xlemnf  13002  qbtwnre  13034  xltnegi  13051  supxrre  13162  infxrre  13171  elioo5  13237  elfz5  13349  elfzm11  13428  predfz  13482  flbi  13637  flbi2  13638  fldiv4lem1div2uz2  13657  fznnfl  13683  zmodid2  13720  2submod  13753  lt2sq  13953  le2sq  13954  sqlecan  14026  bcval5  14133  pfxsuffeqwrdeq  14509  shftfib  14882  mulre  14931  cnpart  15050  sqrlem6  15058  sqrmo  15062  elicc4abs  15130  abs2difabs  15145  cau4  15167  limsupgre  15289  clim2  15312  ello1mpt2  15330  lo1resb  15372  o1resb  15374  climeq  15375  climmpt2  15381  isercoll  15478  caucvgb  15490  fsumabs  15612  isumshft  15650  geomulcvg  15687  absefib  16006  dvdsval3  16066  dvdsabseq  16121  dvdsflip  16125  dvdsssfz1  16126  mod2eq1n2dvds  16155  ndvdsadd  16218  bitscmp  16244  smupvallem  16289  dvdssq  16369  lcmdvds  16410  ncoprmgcdgt1b  16453  isprm3  16485  isprm5  16509  phiprmpw  16574  prmdiv  16583  pc11  16678  pcz  16679  pockthlem  16703  prmreclem2  16715  prmreclem4  16717  prmreclem6  16719  1arith  16725  vdwapun  16772  rami  16813  ramcl  16827  pwsle  17300  ercpbllem  17356  invsym  17571  funcres2c  17714  latnle  18288  grpinvcnv  18739  subgacs  18885  eqger  18902  gexdvds2  19286  pgpfi1  19296  pgpfi  19306  lsmass  19370  lssnle  19375  lsmdisj3b  19391  lsmhash  19406  ablsubadd  19508  gsumval3lem2  19602  subgdmdprd  19732  pgpfac1lem2  19773  dvdsr02  19993  drngid2  20112  issubrg3  20157  sdrgacs  20175  lssacs  20335  prmirred  20802  chrdvds  20838  chrcong  20839  chrnzr  20840  znleval  20868  znleval2  20869  cygznlem3  20883  frlmbas  21068  elfilspd  21116  lindfmm  21140  islindf4  21151  islindf5  21152  psrbaglefi  21241  psrbaglefiOLD  21242  coe1mul2lem1  21544  mdetunilem9  21875  isneip  22362  neiptopnei  22389  lpdifsn  22400  restopnb  22432  restopn2  22434  restdis  22435  restperf  22441  lmbr2  22516  cncls2  22530  cnprest  22546  cnprest2  22547  iscnrm2  22595  ist0-2  22601  ist1-3  22606  ishaus2  22608  cmpfi  22665  dfconn2  22676  1stccnp  22719  subislly  22738  hausmapdom  22757  tx1cn  22866  tx2cn  22867  txcnmpt  22881  txrest  22888  hauseqlcld  22903  tgqtop  22969  qtopcld  22970  ordthmeolem  23058  trfil2  23144  trfil3  23145  trnei  23149  ufildr  23188  fmfg  23206  rnelfm  23210  fmfnfm  23215  elflim  23228  flimrest  23240  cnflf  23259  cnflf2  23260  ptcmplem2  23310  ghmcnp  23372  tsmssubm  23400  iscfilu  23546  xmetgt0  23617  prdsxmetlem  23627  blcomps  23652  blcom  23653  xblpnfps  23654  xblpnf  23655  blpnf  23656  xmeter  23692  setsxms  23740  imasf1obl  23750  stdbdbl  23779  metrest  23786  metuel2  23827  dscopn  23835  xrtgioo  24075  metdstri  24120  cnmpopc  24197  iihalf2  24202  icopnfhmeo  24212  evth2  24229  lmmbr3  24530  iscau3  24548  metcld  24576  cfilucfil3  24590  srabn  24630  rrxmet  24678  minveclem4  24702  evthicc2  24730  ovolgelb  24750  shft2rab  24778  ovolshftlem1  24779  sca2rab  24782  ovolscalem1  24783  ioombl1lem4  24831  mbfmulc2lem  24917  ismbf3d  24924  mbfsup  24934  mbfinf  24935  i1f1lem  24959  i1fmulclem  24973  mbfi1fseqlem4  24989  itg2seq  25013  ditgneg  25127  limcdif  25146  limcnlp  25148  cnplimc  25157  rolle  25260  mvth  25262  dvne0  25281  lhop1lem  25283  itgsubst  25319  mdegle0  25348  deg1leb  25366  deg1le0  25382  q1peqb  25425  coemulhi  25521  dgrlt  25533  plydivlem3  25561  vieta1lem2  25577  aannenlem1  25594  ulmres  25653  reefiso  25713  pilem3  25718  ellogdm  25900  root1eq1  26014  angpieqvdlem  26084  angpieqvdlem2  26085  quad2  26095  1cubr  26098  quart  26117  rlimcnp  26221  wilthlem2  26324  isppw  26369  dvdsflsumcom  26443  fsumvma  26467  logfac2  26471  chpchtsum  26473  dchrmulcl  26503  dchrresb  26513  bclbnd  26534  bposlem1  26538  bposlem5  26542  gausslemma2dlem0c  26612  lgsquadlem1  26634  m1lgs  26642  2lgsoddprmlem2  26663  dchrisumlem3  26745  dchrisum0lem1  26770  sltval2  26910  noextenddif  26922  sleloe  27008  sletri3  27009  eqscut  27050  tgjustr  27124  trgcgrg  27165  lnrot1  27273  islnopp  27389  ismidb  27428  islmib  27437  axsegconlem6  27579  axeuclidlem  27619  axcontlem2  27622  axcontlem4  27624  axcontlem12  27632  ausgrusgrb  27824  nb3grpr2  28039  cplgr2v  28088  umgr2v2enb1  28182  crctcsh  28477  clwwlknonwwlknonb  28758  eupth2lems  28890  nmoreltpnf  29419  isblo2  29433  nmlnogt0  29447  phoeqi  29507  ubthlem2  29521  hire  29744  normgt0  29777  ho01i  30478  ho02i  30479  hoeq1  30480  hoeq2  30481  nmopreltpnf  30519  adjeq  30585  leop  30773  leopmul2i  30785  pjnormssi  30818  pjimai  30826  jplem1  30918  mddmd2  30959  mdslmd1lem1  30975  mdslmd1lem2  30976  superpos  31004  atnssm0  31026  dmdbr5ati  31072  disjunsn  31220  fcoinvbr  31234  ofpreima  31289  funcnv5mpt  31292  suppiniseg  31307  isoun  31321  fpwrelmapffslem  31354  fpwrelmap  31355  iocinioc2  31387  xrdifh  31388  nndiffz1  31394  xdivmul  31486  cntzsnid  31608  isarchi2  31726  elrsp  31866  lsmsnpridl  31883  lsmssass  31887  finexttrb  32035  smatrcl  32044  rhmpreimacnlem  32132  sqsscirc2  32157  xrmulc1cn  32178  esumfsup  32336  1stmbfm  32527  2ndmbfm  32528  mbfmcnt  32535  eulerpartlems  32627  eulerpartlemd  32633  ballotlemfc0  32759  ballotlemfcc  32760  ballotlemsima  32782  ballotlemfrcn0  32796  sgn3da  32808  reprinfz1  32902  reprdifc  32907  bnj1173  33281  zltp1ne  33367  lfuhgr2  33379  erdszelem7  33458  erdszelem9  33460  iscvm  33520  cvmlift3lem4  33583  elmade2  34148  fscgr  34478  seglelin  34514  btwnoutside  34523  lineunray  34545  cldbnd  34611  isfne4  34625  fneval  34637  filnetlem4  34666  nndivsub  34742  bj-gabima  35223  dfgcd3  35608  fvineqsneu  35695  wl-sbhbt  35822  wl-sbcom2d  35829  wl-sbalnae  35830  wl-ax11-lem8  35856  sin2h  35880  cos2h  35881  matunitlindflem1  35886  matunitlindflem2  35887  matunitlindf  35888  ptrest  35889  poimirlem3  35893  poimirlem4  35894  poimirlem22  35912  poimirlem27  35917  mblfinlem3  35929  mblfinlem4  35930  ismblfin  35931  itg2addnclem  35941  itg2addnclem2  35942  itg2gt0cn  35945  iblabsnclem  35953  ftc1anclem6  35968  areacirclem2  35979  areacirclem5  35982  areacirc  35983  mettrifi  36028  drngoi  36222  eldm4  36547  exanres2  36571  disjecxrn  36664  brcoss2  36707  br1cossres2  36715  eldmcoss2  36734  eldm1cossres2  36736  brcosscnv2  36748  erimeq2  36953  disjlem19  37076  prter3  37157  islshpat  37292  lsatnle  37319  ellkr2  37366  lshpkr  37392  lkr0f2  37436  lduallkr3  37437  lkreqN  37445  cvrval2  37549  isat3  37582  glbconN  37652  glbconNOLD  37653  hlrelat5N  37677  cvrval4N  37690  atlt  37713  1cvrco  37748  pmaple  38037  isline2  38050  isline4N  38053  elpaddn0  38076  elpadd2at2  38083  cdlemkid4  39210  dia0  39328  cdlemm10N  39394  dibglbN  39442  dihmeetlem4preN  39582  dochkrshp3  39664  dvh4dimlem  39719  lcfl5  39772  mapdpglem3  39951  mapdheq  40004  hdmap1eq  40077  hdmapval2lem  40107  hdmapoc  40207  hlhillcs  40238  lcmineqlem18  40316  fsuppssind  40550  dvdsexpb  40610  renegadd  40623  resubadd  40630  mulgt0b2d  40698  fz1eqin  40861  diophin  40864  jm2.19  41086  rmxdiophlem  41108  pw2f1ocnv  41130  wepwsolem  41138  gicabl  41195  idomodle  41292  isdomn3  41300  ntrclsfveq2  42000  ntrclsss  42002  ntrclsk4  42011  extoimad  42104  radcnvrat  42261  bcc0  42287  supxrre3rnmpt  43312  clim2f  43521  clim2f2  43555  liminfreuzlem  43687  liminfltlem  43689  xlimmnflimsup2  43737  xlimpnfliminf2  43746  xlimlimsupleliminf  43748  opprb  44884  funbrafv2b  45010  dfafn5a  45011  leaddsuble  45148  iccpartgtprec  45231  flsqrt  45404  dfeven2  45460  dfodd3  45461  lindslinindimp2lem4  46161  snlindsntor  46171  regt1loggt0  46241  elbigo2  46257  elbigolo1  46262  fldivexpfllog2  46270  nnlog2ge0lt1  46271  blenpw2m1  46284  naryfvalelwrdf  46338  isprsd  46608  functhinclem1  46681  thincciso  46689  thinciso  46700  prstcprs  46715  postc  46722