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  2476  sbcom3  2506  sbal1  2528  sbal2  2529  2reu4lem  4469  issn  4781  disjprg  5085  reuhypd  5355  snelpwg  5382  ordtri3  6342  ordsssuc  6397  iota1  6460  funbrfv2b  6879  dffn5  6880  feqmptdf  6892  unima  6897  dmfco  6918  fneqeql  6979  f1ompt  7044  dff13  7188  fliftcnv  7245  soisores  7261  isotr  7270  isoini  7272  caovord3  7559  releldm2  7975  fimaproj  8065  brtpos  8165  tpostpos  8176  oe1m  8460  oawordri  8465  oalimcl  8475  omlimcl  8493  omabs  8566  iserd  8648  qliftel  8724  qliftfun  8726  qliftf  8729  ecopovsym  8743  pw2f1olem  8994  mapen  9054  findcard3  9167  suppeqfsuppbi  9263  mapfien  9292  supisolem  9358  cantnflem1  9579  wemapwe  9587  rankr1clem  9713  rankr1c  9714  ranklim  9737  r1pwALT  9739  r1pwcl  9740  isfin1-2  10276  isfin1-4  10278  fin71num  10288  axdc3lem2  10342  ltmnq  10863  prlem936  10938  ltsosr  10985  ltasr  10991  xrlenlt  11177  ltxrlt  11183  letri3  11198  ne0gt0  11218  subadd  11363  ltsubadd2  11588  lesubadd2  11590  suble  11595  ltsub23  11597  ltaddpos2  11608  ltsubpos  11609  subge02  11633  ltord2  11646  leord2  11647  ltaddsublt  11744  divmul  11779  divmul3  11781  rec11r  11820  ltdiv1  11986  ltdivmul2  11999  ledivmul2  12001  ltrec  12004  ltdiv2  12008  negfi  12071  negiso  12102  nnle1eq1  12155  avgle1  12361  avgle2  12362  avgle  12363  nn0le0eq0  12409  elz2  12486  znnnlt1  12499  zleltp1  12523  difrp  12930  xrltlen  13045  dfle2  13046  xrletri3  13053  xgepnf  13064  xlemnf  13066  qbtwnre  13098  xltnegi  13115  supxrre  13226  infxrre  13236  elioo5  13303  elfz5  13416  elfzm11  13495  predfz  13553  flbi  13720  flbi2  13721  fldiv4lem1div2uz2  13740  fznnfl  13766  zmodid2  13803  2submod  13839  lt2sq  14040  le2sq  14041  sqlecan  14116  bcval5  14225  pfxsuffeqwrdeq  14605  shftfib  14979  mulre  15028  cnpart  15147  01sqrexlem6  15154  sqrmo  15158  elicc4abs  15227  abs2difabs  15242  cau4  15264  limsupgre  15388  clim2  15411  ello1mpt2  15429  lo1resb  15471  o1resb  15473  climeq  15474  climmpt2  15480  isercoll  15575  caucvgb  15587  fsumabs  15708  isumshft  15746  geomulcvg  15783  absefib  16107  dvdsval3  16167  addmulmodb  16176  dvdsabseq  16224  dvdsflip  16228  dvdsssfz1  16229  mod2eq1n2dvds  16258  ndvdsadd  16321  bitscmp  16349  smupvallem  16394  dvdssq  16478  lcmdvds  16519  ncoprmgcdgt1b  16562  isprm3  16594  isprm5  16618  phiprmpw  16687  prmdiv  16696  pc11  16792  pcz  16793  pockthlem  16817  prmreclem2  16829  prmreclem4  16831  prmreclem6  16833  1arith  16839  vdwapun  16886  rami  16927  ramcl  16941  pwsle  17396  ercpbllem  17452  invsym  17669  funcres2c  17810  latnle  18379  grpinvcnv  18919  subgacs  19073  eqger  19090  ghmqusker  19199  gexdvds2  19497  pgpfi1  19507  pgpfi  19517  lsmass  19581  lssnle  19586  lsmdisj3b  19602  lsmhash  19617  ablsubadd  19721  gsumval3lem2  19818  subgdmdprd  19948  pgpfac1lem2  19989  dvdsr02  20290  issubrg3  20515  isdomn3  20630  drngid2  20667  sdrgunit  20711  sdrgacs  20716  lssacs  20900  prmirred  21411  chrdvds  21463  chrcong  21464  chrnzr  21467  znleval  21491  znleval2  21492  cygznlem3  21506  frlmbas  21692  elfilspd  21740  lindfmm  21764  islindf4  21775  islindf5  21776  psrbaglefi  21863  coe1mul2lem1  22181  mdetunilem9  22535  isneip  23020  neiptopnei  23047  lpdifsn  23058  restopnb  23090  restopn2  23092  restdis  23093  restperf  23099  lmbr2  23174  cncls2  23188  cnprest  23204  cnprest2  23205  iscnrm2  23253  ist0-2  23259  ist1-3  23264  ishaus2  23266  cmpfi  23323  dfconn2  23334  1stccnp  23377  subislly  23396  hausmapdom  23415  tx1cn  23524  tx2cn  23525  txcnmpt  23539  txrest  23546  hauseqlcld  23561  tgqtop  23627  qtopcld  23628  ordthmeolem  23716  trfil2  23802  trfil3  23803  trnei  23807  ufildr  23846  fmfg  23864  rnelfm  23868  fmfnfm  23873  elflim  23886  flimrest  23898  cnflf  23917  cnflf2  23918  ptcmplem2  23968  ghmcnp  24030  tsmssubm  24058  iscfilu  24202  xmetgt0  24273  prdsxmetlem  24283  blcomps  24308  blcom  24309  xblpnfps  24310  xblpnf  24311  blpnf  24312  xmeter  24348  setsxms  24394  imasf1obl  24403  stdbdbl  24432  metrest  24439  metuel2  24480  dscopn  24488  xrtgioo  24722  metdstri  24767  cnmpopc  24849  iihalf2  24855  icopnfhmeo  24868  evth2  24886  lmmbr3  25187  iscau3  25205  metcld  25233  cfilucfil3  25247  srabn  25287  rrxmet  25335  minveclem4  25359  evthicc2  25388  ovolgelb  25408  shft2rab  25436  ovolshftlem1  25437  sca2rab  25440  ovolscalem1  25441  ioombl1lem4  25489  mbfmulc2lem  25575  ismbf3d  25582  mbfsup  25592  mbfinf  25593  i1f1lem  25617  i1fmulclem  25630  mbfi1fseqlem4  25646  itg2seq  25670  ditgneg  25785  limcdif  25804  limcnlp  25806  cnplimc  25815  rolle  25921  mvth  25924  dvne0  25943  lhop1lem  25945  itgsubst  25983  mdegle0  26009  deg1leb  26027  deg1le0  26043  q1peqb  26088  coemulhi  26186  dgrlt  26199  plydivlem3  26230  vieta1lem2  26246  aannenlem1  26263  ulmres  26324  reefiso  26385  pilem3  26390  ellogdm  26575  root1eq1  26692  angpieqvdlem  26765  angpieqvdlem2  26766  quad2  26776  1cubr  26779  quart  26798  rlimcnp  26902  wilthlem2  27006  isppw  27051  dvdsflsumcom  27125  fsumvma  27151  logfac2  27155  chpchtsum  27157  dchrmulcl  27187  dchrresb  27197  bclbnd  27218  bposlem1  27222  bposlem5  27226  gausslemma2dlem0c  27296  lgsquadlem1  27318  m1lgs  27326  2lgsoddprmlem2  27347  dchrisumlem3  27429  dchrisum0lem1  27454  sltval2  27595  noextenddif  27607  sleloe  27693  sletri3  27694  eqscut  27746  elmade2  27813  sltadd1  27935  negsunif  27997  sltsub1  28016  sltsubadd2d  28030  mulsproplem12  28066  sltmul2  28110  sltmul1d  28112  divsmulw  28132  sltdivmul2wd  28139  onsiso  28205  n0subs  28289  n0sleltp1  28292  elzn0s  28322  avgslt1d  28376  avgslt2d  28377  zs12ge0  28393  tgjustr  28452  trgcgrg  28493  lnrot1  28601  islnopp  28717  ismidb  28756  islmib  28765  axsegconlem6  28900  axeuclidlem  28940  axcontlem2  28943  axcontlem4  28945  axcontlem12  28953  ausgrusgrb  29143  nb3grpr2  29361  cplgr2v  29410  umgr2v2enb1  29505  crctcsh  29802  clwwlknonwwlknonb  30086  eupth2lems  30218  nmoreltpnf  30749  isblo2  30763  nmlnogt0  30777  phoeqi  30837  ubthlem2  30851  hire  31074  normgt0  31107  ho01i  31808  ho02i  31809  hoeq1  31810  hoeq2  31811  nmopreltpnf  31849  adjeq  31915  leop  32103  leopmul2i  32115  pjnormssi  32148  pjimai  32156  jplem1  32248  mddmd2  32289  mdslmd1lem1  32305  mdslmd1lem2  32306  superpos  32334  atnssm0  32356  dmdbr5ati  32402  disjunsn  32574  fcoinvbr  32585  ofpreima  32647  funcnv5mpt  32650  suppiniseg  32667  isoun  32683  fpwrelmapffslem  32715  fpwrelmap  32716  iocinioc2  32762  xrdifh  32763  nndiffz1  32769  sgn3da  32817  xdivmul  32905  cntzsnid  33049  cntrval2  33140  isarchi2  33154  erler  33232  elrsp  33337  lsmsnpridl  33363  lsmssass  33367  r1pid2OLD  33569  finexttrb  33678  algextdeglem6  33735  algextdeglem7  33736  smatrcl  33809  rhmpreimacnlem  33897  sqsscirc2  33922  xrmulc1cn  33943  esumfsup  34083  1stmbfm  34273  2ndmbfm  34274  mbfmcnt  34281  eulerpartlems  34373  eulerpartlemd  34379  ballotlemfc0  34506  ballotlemfcc  34507  ballotlemsima  34529  ballotlemfrcn0  34543  reprinfz1  34635  reprdifc  34640  bnj1173  35014  fineqvnttrclse  35144  vonf1owev  35152  zltp1ne  35154  lfuhgr2  35163  erdszelem7  35241  erdszelem9  35243  iscvm  35303  cvmlift3lem4  35366  rexxfr3dALT  35683  fscgr  36124  seglelin  36160  btwnoutside  36169  lineunray  36191  cldbnd  36370  isfne4  36384  fneval  36396  filnetlem4  36425  nndivsub  36501  bj-gabima  36984  dfgcd3  37368  fvineqsneu  37455  wl-sbhbt  37598  wl-sbcom2d  37605  wl-sbalnae  37606  sin2h  37649  cos2h  37650  matunitlindflem1  37655  matunitlindflem2  37656  matunitlindf  37657  ptrest  37658  poimirlem3  37662  poimirlem4  37663  poimirlem22  37681  poimirlem27  37686  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  itg2addnclem  37710  itg2addnclem2  37711  itg2gt0cn  37714  iblabsnclem  37722  ftc1anclem6  37737  areacirclem2  37748  areacirclem5  37751  areacirc  37752  mettrifi  37796  drngoi  37990  eldm4  38312  exanres2  38334  disjecxrn  38435  exeupre  38502  brcoss2  38533  br1cossres2  38541  eldmcoss2  38560  eldm1cossres2  38562  brcosscnv2  38574  erimeq2  38775  disjlem19  38898  prter3  38980  islshpat  39115  lsatnle  39142  ellkr2  39189  lshpkr  39215  lkr0f2  39259  lduallkr3  39260  lkreqN  39268  cvrval2  39372  isat3  39405  glbconN  39475  hlrelat5N  39499  cvrval4N  39512  atlt  39535  1cvrco  39570  pmaple  39859  isline2  39872  isline4N  39875  elpaddn0  39898  elpadd2at2  39905  cdlemkid4  41032  dia0  41150  cdlemm10N  41216  dibglbN  41264  dihmeetlem4preN  41404  dochkrshp3  41486  dvh4dimlem  41541  lcfl5  41594  mapdpglem3  41773  mapdheq  41826  hdmap1eq  41899  hdmapval2lem  41929  hdmapoc  42029  hlhillcs  42056  lcmineqlem18  42138  dvdsexpb  42427  renegadd  42464  resubadd  42471  redivmuld  42537  mulgt0b1d  42564  fsuppssind  42685  fz1eqin  42861  diophin  42864  jm2.19  43085  rmxdiophlem  43107  pw2f1ocnv  43129  wepwsolem  43134  gicabl  43191  idomodle  43283  onsupmaxb  43331  cantnf2  43417  tfsconcatb0  43436  tfsnfin  43444  ntrclsfveq2  44153  ntrclsss  44155  ntrclsk4  44164  extoimad  44256  radcnvrat  44406  bcc0  44432  supxrre3rnmpt  45526  clim2f  45733  clim2f2  45767  liminfreuzlem  45899  liminfltlem  45901  xlimmnflimsup2  45949  xlimpnfliminf2  45958  xlimlimsupleliminf  45960  opprb  47130  funbrafv2b  47258  dfafn5a  47259  leaddsuble  47396  mod2addne  47463  iccpartgtprec  47519  flsqrt  47692  dfeven2  47748  dfodd3  47749  lindslinindimp2lem4  48561  snlindsntor  48571  regt1loggt0  48636  elbigo2  48652  elbigolo1  48657  fldivexpfllog2  48665  nnlog2ge0lt1  48666  blenpw2m1  48679  naryfvalelwrdf  48733  isprsd  49054  resccatlem  49173  functhinclem1  49544  thincciso  49553  thinciso  49570  isinito2lem  49598  fulltermc  49611  prstcprs  49660  oduoppcciso  49666  postc  49669  lmdran  49771  cmdlan  49772