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  550  mpbirand  719  sb3b  2506  sbcom3  2536  sbal1  2558  sbal2  2559  2reu4lem  4483  issn  4796  disjprg  5104  reuhypd  5390  snelpwg  5424  ordtri3  6397  ordsssuc  6452  iota1  6515  funbrfv2b  6938  dffn5  6939  feqmptdf  6951  unima  6956  dmfco  6977  fneqeql  7041  f1ompt  7106  dff13  7252  fliftcnv  7309  soisores  7325  isotr  7334  isoini  7336  caovord3  7623  releldm2  8039  fimaproj  8130  brtpos  8230  tpostpos  8241  oe1m  8529  oawordri  8534  oalimcl  8544  omlimcl  8562  omabs  8636  iserd  8720  qliftel  8797  qliftfun  8799  qliftf  8802  ecopovsym  8816  pw2f1olem  9068  mapen  9128  findcard3  9242  tfsnfin2  9319  suppeqfsuppbi  9338  mapfien  9367  supisolem  9433  cantnflem1  9657  wemapwe  9665  rankr1clem  9791  rankr1c  9792  ranklim  9815  r1pwALT  9817  r1pwcl  9818  isfin1-2  10368  isfin1-4  10370  fin71num  10380  axdc3lem2  10434  infinfg  10549  ltmnq  10956  prlem936  11031  ltsosr  11078  ltasr  11084  xrlenlt  11273  ltxrlt  11279  letri3  11294  ne0gt0  11314  subadd  11459  ltsubadd2  11684  lesubadd2  11686  suble  11691  ltsub23  11693  ltaddpos2  11704  ltsubpos  11705  subge02  11729  ltord2  11742  leord2  11743  ltaddsublt  11840  divmul  11874  divmul3  11876  rec11r  11913  ltdiv1  12078  ltdivmul2  12091  ledivmul2  12093  ltrec  12096  ltdiv2  12100  negfi  12163  negiso  12194  nnle1eq1  12265  avgle1  12483  avgle2  12484  avgle  12485  nn0le0eq0  12531  elz2  12608  znnnlt1  12620  zleltp1  12644  difrp  13055  xrltlen  13170  dfle2  13171  xrletri3  13178  xgepnf  13190  xlemnf  13192  qbtwnre  13224  xltnegi  13241  supxrre  13352  infxrre  13362  elioo5  13429  elfz5  13543  elfzm11  13622  predfz  13680  flbi  13848  flbi2  13849  fldiv4lem1div2uz2  13868  fznnfl  13894  zmodid2  13931  2submod  13967  lt2sq  14168  le2sq  14169  sqlecan  14244  bcval5  14353  pfxsuffeqwrdeq  14734  shftfib  15108  sgn3da  15137  mulre  15171  cnpart  15290  01sqrexlem6  15297  sqrmo  15301  elicc4abs  15370  abs2difabs  15385  cau4  15407  limsupgre  15531  clim2  15554  ello1mpt2  15572  lo1resb  15614  o1resb  15616  climeq  15617  climmpt2  15623  isercoll  15718  caucvgb  15730  fsumabs  15852  isumshft  15892  geomulcvg  15929  absefib  16253  dvdsval3  16313  addmulmodb  16322  dvdsabseq  16370  dvdsflip  16374  dvdsssfz1  16375  mod2eq1n2dvds  16404  ndvdsadd  16467  bitscmp  16495  smupvallem  16540  dvdssq  16624  lcmdvds  16665  ncoprmgcdgt1b  16708  isprm3  16740  isprm5  16765  phiprmpw  16834  prmdiv  16843  pc11  16939  pcz  16940  pockthlem  16964  prmreclem2  16976  prmreclem4  16978  prmreclem6  16980  1arith  16986  vdwapun  17033  rami  17074  ramcl  17088  pwsle  17545  ercpbllem  17601  invsym  17818  funcres2c  17959  latnle  18528  grpinvcnv  19072  subgacs  19226  eqger  19245  ghmqusker  19356  gexdvds2  19654  pgpfi1  19664  pgpfi  19674  lsmass  19738  lssnle  19743  lsmdisj3b  19759  lsmhash  19774  ablsubadd  19878  gsumval3lem2  19975  subgdmdprd  20105  pgpfac1lem2  20146  dvdsr02  20453  issubrg3  20684  isdomn3  20798  drngid2  20836  sdrgunit  20878  sdrgacs  20883  lssacs  21067  prmirred  21603  chrdvds  21655  chrcong  21656  chrnzr  21659  znleval  21683  znleval2  21684  cygznlem3  21698  frlmbas  21884  elfilspd  21932  lindfmm  21956  islindf4  21967  islindf5  21968  psrbaglefi  22055  coe1mul2lem1  22407  mdetunilem9  22756  isneip  23241  neiptopnei  23268  lpdifsn  23279  restopnb  23311  restopn2  23313  restdis  23314  restperf  23320  lmbr2  23395  cncls2  23409  cnprest  23425  cnprest2  23426  iscnrm2  23474  ist0-2  23480  ist1-3  23485  ishaus2  23487  cmpfi  23544  dfconn2  23555  1stccnp  23598  subislly  23617  hausmapdom  23636  tx1cn  23745  tx2cn  23746  txcnmpt  23760  txrest  23767  hauseqlcld  23782  tgqtop  23848  qtopcld  23849  ordthmeolem  23937  trfil2  24023  trfil3  24024  trnei  24028  ufildr  24067  fmfg  24085  rnelfm  24089  fmfnfm  24094  elflim  24107  flimrest  24119  cnflf  24138  cnflf2  24139  ptcmplem2  24189  ghmcnp  24251  tsmssubm  24279  iscfilu  24423  xmetgt0  24494  prdsxmetlem  24504  blcomps  24529  blcom  24530  xblpnfps  24531  xblpnf  24532  blpnf  24533  xmeter  24569  setsxms  24615  imasf1obl  24624  stdbdbl  24653  metrest  24660  metuel2  24701  dscopn  24709  xrtgioo  24943  metdstri  24988  cnmpopc  25066  iihalf2  25071  icopnfhmeo  25081  evth2  25098  lmmbr3  25398  iscau3  25416  metcld  25444  cfilucfil3  25458  srabn  25498  rrxmet  25546  minveclem4  25570  evthicc2  25598  ovolgelb  25618  shft2rab  25646  ovolshftlem1  25647  sca2rab  25650  ovolscalem1  25651  ioombl1lem4  25699  mbfmulc2lem  25785  ismbf3d  25792  mbfsup  25802  mbfinf  25803  i1f1lem  25827  i1fmulclem  25840  mbfi1fseqlem4  25856  itg2seq  25880  ditgneg  25995  limcdif  26014  limcnlp  26016  cnplimc  26025  rolle  26128  mvth  26130  dvne0  26149  lhop1lem  26151  itgsubst  26187  mdegle0  26213  deg1leb  26231  deg1le0  26247  q1peqb  26292  coemulhi  26390  dgrlt  26402  plydivlem3  26435  vieta1lem2  26451  aannenlem1  26468  ulmres  26527  reefiso  26587  pilem3  26592  ellogdm  26780  root1eq1  26896  angpieqvdlem  26969  angpieqvdlem2  26970  quad2  26980  1cubr  26983  quart  27002  rlimcnp  27106  wilthlem2  27209  isppw  27254  dvdsflsumcom  27328  fsumvma  27353  logfac2  27357  chpchtsum  27359  dchrmulcl  27389  dchrresb  27399  bclbnd  27420  bposlem1  27424  bposlem5  27428  gausslemma2dlem0c  27498  lgsquadlem1  27520  m1lgs  27528  2lgsoddprmlem2  27549  dchrisumlem3  27631  dchrisum0lem1  27656  ltsval2  27796  noextenddif  27808  lesloe  27894  lestri3  27895  eqcuts  27954  elmade2  28027  ltadds1  28161  negsunif  28224  ltsubs1  28245  ltsubadds2d  28259  mulsproplem12  28296  ltmuls2  28340  ltmuls1d  28342  divmulsw  28362  ltdivmuls2wd  28369  oniso  28440  n0subs  28532  n0lesltp1  28535  elzn0s  28567  avglts1d  28622  avglts2d  28623  bdaypw2n0bndlem  28632  z12sge0  28652  dfz12s2  28657  elreno2  28664  tgjustr  28719  trgcgrg  28760  lnrot1  28872  islnopp  28995  elplng  29036  plngcplem  29041  ismidb  29061  islmib  29070  axsegconlem6  29238  axeuclidlem  29278  axcontlem2  29281  axcontlem4  29283  axcontlem12  29291  ausgrusgrb  29481  nb3grpr2  29699  cplgr2v  29748  umgr2v2enb1  29842  crctcsh  30139  clwwlknonwwlknonb  30423  eupth2lems  30555  nmoreltpnf  31087  isblo2  31101  nmlnogt0  31115  phoeqi  31175  ubthlem2  31189  hire  31412  normgt0  31445  ho01i  32146  ho02i  32147  hoeq1  32148  hoeq2  32149  nmopreltpnf  32187  adjeq  32253  leop  32441  leopmul2i  32453  pjnormssi  32486  pjimai  32494  jplem1  32586  mddmd2  32627  mdslmd1lem1  32643  mdslmd1lem2  32644  superpos  32672  atnssm0  32694  dmdbr5ati  32740  disjunsn  32905  fcoinvbr  32916  ofpreima  32976  funcnv5mpt  32978  suppiniseg  32997  isoun  33013  fpwrelmapffslem  33043  fpwrelmap  33044  iocinioc2  33090  xrdifh  33091  nndiffz1  33097  xdivmul  33210  cntzsnid  33366  cntrval2  33457  isarchi2  33471  isunitc  33527  erler  33551  rlocisunit  33562  elrsp  33652  lsmsnpridl  33675  lsmssass  33677  esplyind  33931  finexttrb  34021  algextdeglem6  34078  algextdeglem7  34079  smatrcl  34152  rhmpreimacnlem  34240  sqsscirc2  34265  xrmulc1cn  34286  esumfsup  34426  1stmbfm  34616  2ndmbfm  34617  mbfmcnt  34624  eulerpartlems  34716  eulerpartlemd  34722  ballotlemfc0  34849  ballotlemfcc  34850  ballotlemsima  34872  ballotlemfrcn0  34886  reprinfz1  34975  reprdifc  34980  bnj1173  35356  fineqvnttrclse  35491  kardcard2  35533  vonf1wev  35546  vonf1owevOLD  35548  zltp1ne  35555  lfuhgr2  35565  erdszelem7  35643  erdszelem9  35645  iscvm  35705  cvmlift3lem4  35768  rexxfr3dALT  36085  fscgr  36526  seglelin  36562  btwnoutside  36571  lineunray  36593  cldbnd  36781  isfne4  36795  fneval  36807  filnetlem4  36836  nndivsub  36912  bj-gabima  37520  dfgcd3  37912  fvineqsneu  38001  wl-sbhbt  38153  wl-sbcom2d  38160  wl-sbalnae  38161  sin2h  38205  cos2h  38206  matunitlindflem1  38211  matunitlindflem2  38212  matunitlindf  38213  ptrest  38214  poimirlem3  38218  poimirlem4  38219  poimirlem22  38237  poimirlem27  38242  mblfinlem3  38254  mblfinlem4  38255  ismblfin  38256  itg2addnclem  38266  itg2addnclem2  38267  itg2gt0cn  38270  iblabsnclem  38278  ftc1anclem6  38293  areacirclem2  38304  areacirclem5  38307  areacirc  38308  mettrifi  38352  drngoi  38546  eldm4  38876  exanres2  38898  disjecxrn  39007  exeupre  39086  brcoss2  39117  br1cossres2  39125  eldmcoss2  39144  eldm1cossres2  39146  brcosscnv2  39158  erimeq2  39358  disjqmap  39422  disjlem19  39499  prter3  39602  islshpat  39737  lsatnle  39764  ellkr2  39811  lshpkr  39837  lkr0f2  39881  lduallkr3  39882  lkreqN  39890  cvrval2  39994  isat3  40027  glbconN  40097  hlrelat5N  40121  cvrval4N  40134  atlt  40157  1cvrco  40192  pmaple  40481  isline2  40494  isline4N  40497  elpaddn0  40520  elpadd2at2  40527  cdlemkid4  41654  dia0  41772  cdlemm10N  41838  dibglbN  41886  dihmeetlem4preN  42026  dochkrshp3  42108  dvh4dimlem  42163  lcfl5  42216  mapdpglem3  42395  mapdheq  42448  hdmap1eq  42521  hdmapval2lem  42551  hdmapoc  42651  hlhillcs  42678  lcmineqlem18  42759  dvdsexpb  43042  renegadd  43079  resubadd  43086  redivmuld  43152  mulgt0b1d  43192  fsuppssind  43273  fz1eqin  43448  diophin  43451  jm2.19  43668  rmxdiophlem  43690  pw2f1ocnv  43712  wepwsolem  43717  gicabl  43774  idomodle  43866  onsupmaxb  43914  cantnf2  44000  tfsconcatb0  44019  tfsnfin  44027  ntrclsfveq2  44735  ntrclsss  44737  ntrclsk4  44746  extoimad  44838  radcnvrat  44972  bcc0  44998  hashomiso  45682  supxrre3rnmpt  46091  clim2f  46298  clim2f2  46332  liminfreuzlem  46464  liminfltlem  46466  xlimmnflimsup2  46514  xlimpnfliminf2  46523  xlimlimsupleliminf  46525  opprb  47713  funbrafv2b  47841  dfafn5a  47842  leaddsuble  47979  mod2addne  48052  iccpartgtprec  48114  flsqrt  48290  dfeven2  48359  dfodd3  48360  lindslinindimp2lem4  49186  snlindsntor  49196  regt1loggt0  49261  elbigo2  49277  elbigolo1  49282  fldivexpfllog2  49290  nnlog2ge0lt1  49291  blenpw2m1  49304  naryfvalelwrdf  49358  isprsd  49678  resccatlem  49796  functhinclem1  50167  thincciso  50176  thinciso  50193  isinito2lem  50221  fulltermc  50234  prstcprs  50283  oduoppcciso  50289  postc  50292  lmdran  50394  cmdlan  50395