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  4423  issn  4723  disjprgw  5025  disjprg  5026  reuhypd  5285  ordtri3  6195  ordsssuc  6245  iota1  6301  funbrfv2b  6698  dffn5  6699  feqmptdf  6710  unima  6714  dmfco  6734  fneqeql  6793  f1ompt  6852  dff13  6991  fliftcnv  7043  soisores  7059  isotr  7068  isoini  7070  caovord3  7341  releldm2  7724  fimaproj  7812  brtpos  7884  tpostpos  7895  oe1m  8154  oawordri  8159  oalimcl  8169  omlimcl  8187  omabs  8257  iserd  8298  qliftel  8363  qliftfun  8365  qliftf  8368  ecopovsym  8382  pw2f1olem  8604  mapen  8665  suppeqfsuppbi  8831  mapfien  8855  supisolem  8921  cantnflem1  9136  wemapwe  9144  rankr1clem  9233  rankr1c  9234  ranklim  9257  r1pwALT  9259  r1pwcl  9260  isfin1-2  9796  isfin1-4  9798  fin71num  9808  axdc3lem2  9862  ltmnq  10383  prlem936  10458  ltsosr  10505  ltasr  10511  xrlenlt  10695  ltxrlt  10700  letri3  10715  ne0gt0  10734  subadd  10878  ltsubadd2  11100  lesubadd2  11102  suble  11107  ltsub23  11109  ltaddpos2  11120  ltsubpos  11121  subge02  11145  ltord2  11158  leord2  11159  ltaddsublt  11256  divmul  11290  divmul3  11292  rec11r  11328  ltdiv1  11493  ltdivmul2  11506  ledivmul2  11508  ltrec  11511  ltdiv2  11515  negfi  11577  negiso  11608  nnle1eq1  11655  avgle1  11865  avgle2  11866  avgle  11867  nn0le0eq0  11913  elz2  11987  znnnlt1  11997  zleltp1  12021  difrp  12415  xrltlen  12527  dfle2  12528  xrletri3  12535  xgepnf  12546  xlemnf  12548  qbtwnre  12580  xltnegi  12597  supxrre  12708  infxrre  12717  elioo5  12782  elfz5  12894  elfzm11  12973  predfz  13027  flbi  13181  flbi2  13182  fldiv4lem1div2uz2  13201  fznnfl  13225  zmodid2  13262  2submod  13295  lt2sq  13494  le2sq  13495  sqlecan  13567  bcval5  13674  pfxsuffeqwrdeq  14051  shftfib  14423  mulre  14472  cnpart  14591  sqrlem6  14599  sqrmo  14603  elicc4abs  14671  abs2difabs  14686  cau4  14708  limsupgre  14830  clim2  14853  ello1mpt2  14871  lo1resb  14913  o1resb  14915  climeq  14916  climmpt2  14922  isercoll  15016  caucvgb  15028  fsumabs  15148  isumshft  15186  geomulcvg  15224  absefib  15543  dvdsval3  15603  dvdsabseq  15655  dvdsflip  15659  dvdsssfz1  15660  mod2eq1n2dvds  15688  ndvdsadd  15751  bitscmp  15777  smupvallem  15822  dvdssq  15901  lcmdvds  15942  ncoprmgcdgt1b  15985  isprm3  16017  isprm5  16041  phiprmpw  16103  prmdiv  16112  pc11  16206  pcz  16207  pockthlem  16231  prmreclem2  16243  prmreclem4  16245  prmreclem6  16247  1arith  16253  vdwapun  16300  rami  16341  ramcl  16355  pwsle  16757  ercpbllem  16813  invsym  17024  funcres2c  17163  latnle  17687  grpinvcnv  18159  subgacs  18305  eqger  18322  gexdvds2  18702  pgpfi1  18712  pgpfi  18722  lsmass  18787  lssnle  18792  lsmdisj3b  18808  lsmhash  18823  ablsubadd  18925  gsumval3lem2  19019  subgdmdprd  19149  pgpfac1lem2  19190  dvdsr02  19402  drngid2  19511  issubrg3  19556  sdrgacs  19573  lssacs  19732  prmirred  20188  chrdvds  20220  chrcong  20221  chrnzr  20222  znleval  20246  znleval2  20247  cygznlem3  20261  frlmbas  20444  elfilspd  20492  lindfmm  20516  islindf4  20527  islindf5  20528  psrbaglefi  20610  coe1mul2lem1  20896  mdetunilem9  21225  isneip  21710  neiptopnei  21737  lpdifsn  21748  restopnb  21780  restopn2  21782  restdis  21783  restperf  21789  lmbr2  21864  cncls2  21878  cnprest  21894  cnprest2  21895  iscnrm2  21943  ist0-2  21949  ist1-3  21954  ishaus2  21956  cmpfi  22013  dfconn2  22024  1stccnp  22067  subislly  22086  hausmapdom  22105  tx1cn  22214  tx2cn  22215  txcnmpt  22229  txrest  22236  hauseqlcld  22251  tgqtop  22317  qtopcld  22318  ordthmeolem  22406  trfil2  22492  trfil3  22493  trnei  22497  ufildr  22536  fmfg  22554  rnelfm  22558  fmfnfm  22563  elflim  22576  flimrest  22588  cnflf  22607  cnflf2  22608  ptcmplem2  22658  ghmcnp  22720  tsmssubm  22748  iscfilu  22894  xmetgt0  22965  prdsxmetlem  22975  blcomps  23000  blcom  23001  xblpnfps  23002  xblpnf  23003  blpnf  23004  xmeter  23040  setsxms  23086  imasf1obl  23095  stdbdbl  23124  metrest  23131  metuel2  23172  dscopn  23180  xrtgioo  23411  metdstri  23456  cnmpopc  23533  iihalf2  23538  icopnfhmeo  23548  evth2  23565  lmmbr3  23864  iscau3  23882  metcld  23910  cfilucfil3  23924  srabn  23964  rrxmet  24012  minveclem4  24036  evthicc2  24064  ovolgelb  24084  shft2rab  24112  ovolshftlem1  24113  sca2rab  24116  ovolscalem1  24117  ioombl1lem4  24165  mbfmulc2lem  24251  ismbf3d  24258  mbfsup  24268  mbfinf  24269  i1f1lem  24293  i1fmulclem  24306  mbfi1fseqlem4  24322  itg2seq  24346  ditgneg  24460  limcdif  24479  limcnlp  24481  cnplimc  24490  rolle  24593  mvth  24595  dvne0  24614  lhop1lem  24616  itgsubst  24652  mdegle0  24678  deg1leb  24696  deg1le0  24712  q1peqb  24755  coemulhi  24851  dgrlt  24863  plydivlem3  24891  vieta1lem2  24907  aannenlem1  24924  ulmres  24983  reefiso  25043  pilem3  25048  ellogdm  25230  root1eq1  25344  angpieqvdlem  25414  angpieqvdlem2  25415  quad2  25425  1cubr  25428  quart  25447  rlimcnp  25551  wilthlem2  25654  isppw  25699  dvdsflsumcom  25773  fsumvma  25797  logfac2  25801  chpchtsum  25803  dchrmulcl  25833  dchrresb  25843  bclbnd  25864  bposlem1  25868  bposlem5  25872  gausslemma2dlem0c  25942  lgsquadlem1  25964  m1lgs  25972  2lgsoddprmlem2  25993  dchrisumlem3  26075  dchrisum0lem1  26100  tgjustr  26268  trgcgrg  26309  lnrot1  26417  islnopp  26533  ismidb  26572  islmib  26581  axsegconlem6  26716  axeuclidlem  26756  axcontlem2  26759  axcontlem4  26761  axcontlem12  26769  ausgrusgrb  26958  nb3grpr2  27173  cplgr2v  27222  umgr2v2enb1  27316  crctcsh  27610  clwwlknonwwlknonb  27891  eupth2lems  28023  nmoreltpnf  28552  isblo2  28566  nmlnogt0  28580  phoeqi  28640  ubthlem2  28654  hire  28877  normgt0  28910  ho01i  29611  ho02i  29612  hoeq1  29613  hoeq2  29614  nmopreltpnf  29652  adjeq  29718  leop  29906  leopmul2i  29918  pjnormssi  29951  pjimai  29959  jplem1  30051  mddmd2  30092  mdslmd1lem1  30108  mdslmd1lem2  30109  superpos  30137  atnssm0  30159  dmdbr5ati  30205  disjunsn  30357  fcoinvbr  30371  ofpreima  30428  funcnv5mpt  30431  suppiniseg  30446  isoun  30461  fpwrelmapffslem  30494  fpwrelmap  30495  iocinioc2  30528  xrdifh  30529  nndiffz1  30535  xdivmul  30627  cntzsnid  30746  isarchi2  30864  elrsp  30989  lsmsnpridl  31005  lsmssass  31009  finexttrb  31140  smatrcl  31149  rhmpreimacnlem  31237  sqsscirc2  31262  xrmulc1cn  31283  esumfsup  31439  1stmbfm  31628  2ndmbfm  31629  mbfmcnt  31636  eulerpartlems  31728  eulerpartlemd  31734  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemsima  31883  ballotlemfrcn0  31897  sgn3da  31909  reprinfz1  32003  reprdifc  32008  bnj1173  32384  zltp1ne  32458  lfuhgr2  32478  erdszelem7  32557  erdszelem9  32559  iscvm  32619  cvmlift3lem4  32682  sltval2  33276  noextenddif  33288  sleloe  33346  sletri3  33347  fscgr  33654  seglelin  33690  btwnoutside  33699  lineunray  33721  cldbnd  33787  isfne4  33801  fneval  33813  filnetlem4  33842  nndivsub  33918  dfgcd3  34738  fvineqsneu  34828  wl-sbhbt  34955  wl-sbcom2d  34962  wl-sbalnae  34963  wl-ax11-lem8  34989  wl-dfrmof  35020  sin2h  35047  cos2h  35048  matunitlindflem1  35053  matunitlindflem2  35054  matunitlindf  35055  ptrest  35056  poimirlem3  35060  poimirlem4  35061  poimirlem22  35079  poimirlem27  35084  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  itg2addnclem  35108  itg2addnclem2  35109  itg2gt0cn  35112  iblabsnclem  35120  ftc1anclem6  35135  areacirclem2  35146  areacirclem5  35149  areacirc  35150  mettrifi  35195  drngoi  35389  eldm4  35691  exanres2  35714  brcoss2  35837  br1cossres2  35845  eldmcoss2  35859  eldm1cossres2  35861  brcosscnv2  35873  erim2  36071  prter3  36178  islshpat  36313  lsatnle  36340  ellkr2  36387  lshpkr  36413  lkr0f2  36457  lduallkr3  36458  lkreqN  36466  cvrval2  36570  isat3  36603  glbconN  36673  hlrelat5N  36697  cvrval4N  36710  atlt  36733  1cvrco  36768  pmaple  37057  isline2  37070  isline4N  37073  elpaddn0  37096  elpadd2at2  37103  cdlemkid4  38230  dia0  38348  cdlemm10N  38414  dibglbN  38462  dihmeetlem4preN  38602  dochkrshp3  38684  dvh4dimlem  38739  lcfl5  38792  mapdpglem3  38971  mapdheq  39024  hdmap1eq  39097  hdmapval2lem  39127  hdmapoc  39227  hlhillcs  39254  lcmineqlem18  39334  fsuppssind  39459  renegadd  39510  resubadd  39517  mulgt0b2d  39585  fz1eqin  39710  diophin  39713  jm2.19  39934  rmxdiophlem  39956  pw2f1ocnv  39978  wepwsolem  39986  gicabl  40043  idomodle  40140  isdomn3  40148  ntrclsfveq2  40764  ntrclsss  40766  ntrclsk4  40775  extoimad  40868  radcnvrat  41018  bcc0  41044  supxrre3rnmpt  42066  clim2f  42278  clim2f2  42312  liminfreuzlem  42444  liminfltlem  42446  xlimmnflimsup2  42494  xlimpnfliminf2  42503  xlimlimsupleliminf  42505  opprb  43623  funbrafv2b  43715  dfafn5a  43716  leaddsuble  43854  iccpartgtprec  43937  flsqrt  44110  dfeven2  44167  dfodd3  44168  lindslinindimp2lem4  44870  snlindsntor  44880  regt1loggt0  44950  elbigo2  44966  elbigolo1  44971  fldivexpfllog2  44979  nnlog2ge0lt1  44980  blenpw2m1  44993  naryfvalelwrdf  45047