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  548  mpbirand  715  sb3b  2497  sbcom3  2527  sbal1  2549  sbal2  2550  2reu4lem  4467  issn  4780  disjprg  5086  reuhypd  5366  snelpwg  5400  ordtri3  6367  ordsssuc  6422  iota1  6485  funbrfv2b  6909  dffn5  6910  feqmptdf  6922  unima  6927  dmfco  6948  fneqeql  7012  f1ompt  7077  dff13  7223  fliftcnv  7280  soisores  7296  isotr  7305  isoini  7307  caovord3  7594  releldm2  8009  fimaproj  8099  brtpos  8199  tpostpos  8210  oe1m  8498  oawordri  8503  oalimcl  8513  omlimcl  8531  omabs  8605  iserd  8689  qliftel  8766  qliftfun  8768  qliftf  8771  ecopovsym  8785  pw2f1olem  9038  mapen  9098  findcard3  9212  tfsnfin2  9292  suppeqfsuppbi  9311  mapfien  9340  supisolem  9406  cantnflem1  9630  wemapwe  9638  rankr1clem  9764  rankr1c  9765  ranklim  9788  r1pwALT  9790  r1pwcl  9791  isfin1-2  10328  isfin1-4  10330  fin71num  10340  axdc3lem2  10394  infinfg  10509  ltmnq  10916  prlem936  10991  ltsosr  11038  ltasr  11044  xrlenlt  11233  ltxrlt  11239  letri3  11254  ne0gt0  11274  subadd  11419  ltsubadd2  11644  lesubadd2  11646  suble  11651  ltsub23  11653  ltaddpos2  11664  ltsubpos  11665  subge02  11689  ltord2  11702  leord2  11703  ltaddsublt  11800  divmul  11834  divmul3  11836  rec11r  11876  ltdiv1  12042  ltdivmul2  12055  ledivmul2  12057  ltrec  12060  ltdiv2  12064  negfi  12127  negiso  12158  nnle1eq1  12229  avgle1  12447  avgle2  12448  avgle  12449  nn0le0eq0  12495  elz2  12572  znnnlt1  12584  zleltp1  12608  difrp  13019  xrltlen  13134  dfle2  13135  xrletri3  13142  xgepnf  13154  xlemnf  13156  qbtwnre  13188  xltnegi  13205  supxrre  13316  infxrre  13326  elioo5  13393  elfz5  13507  elfzm11  13586  predfz  13644  flbi  13812  flbi2  13813  fldiv4lem1div2uz2  13832  fznnfl  13858  zmodid2  13895  2submod  13931  lt2sq  14132  le2sq  14133  sqlecan  14208  bcval5  14317  pfxsuffeqwrdeq  14697  shftfib  15071  mulre  15120  cnpart  15239  01sqrexlem6  15246  sqrmo  15250  elicc4abs  15319  abs2difabs  15334  cau4  15356  limsupgre  15480  clim2  15503  ello1mpt2  15521  lo1resb  15563  o1resb  15565  climeq  15566  climmpt2  15572  isercoll  15667  caucvgb  15679  fsumabs  15801  isumshft  15841  geomulcvg  15878  absefib  16202  dvdsval3  16262  addmulmodb  16271  dvdsabseq  16319  dvdsflip  16323  dvdsssfz1  16324  mod2eq1n2dvds  16353  ndvdsadd  16416  bitscmp  16444  smupvallem  16489  dvdssq  16573  lcmdvds  16614  ncoprmgcdgt1b  16657  isprm3  16689  isprm5  16714  phiprmpw  16783  prmdiv  16792  pc11  16888  pcz  16889  pockthlem  16913  prmreclem2  16925  prmreclem4  16927  prmreclem6  16929  1arith  16935  vdwapun  16982  rami  17023  ramcl  17037  pwsle  17494  ercpbllem  17550  invsym  17767  funcres2c  17908  latnle  18477  grpinvcnv  19020  subgacs  19174  eqger  19191  ghmqusker  19299  gexdvds2  19597  pgpfi1  19607  pgpfi  19617  lsmass  19681  lssnle  19686  lsmdisj3b  19702  lsmhash  19717  ablsubadd  19821  gsumval3lem2  19918  subgdmdprd  20048  pgpfac1lem2  20089  dvdsr02  20389  issubrg3  20618  isdomn3  20733  drngid2  20770  sdrgunit  20814  sdrgacs  20819  lssacs  21003  prmirred  21495  chrdvds  21547  chrcong  21548  chrnzr  21551  znleval  21575  znleval2  21576  cygznlem3  21590  frlmbas  21776  elfilspd  21824  lindfmm  21848  islindf4  21859  islindf5  21860  psrbaglefi  21947  coe1mul2lem1  22299  mdetunilem9  22649  isneip  23134  neiptopnei  23161  lpdifsn  23172  restopnb  23204  restopn2  23206  restdis  23207  restperf  23213  lmbr2  23288  cncls2  23302  cnprest  23318  cnprest2  23319  iscnrm2  23367  ist0-2  23373  ist1-3  23378  ishaus2  23380  cmpfi  23437  dfconn2  23448  1stccnp  23491  subislly  23510  hausmapdom  23529  tx1cn  23638  tx2cn  23639  txcnmpt  23653  txrest  23660  hauseqlcld  23675  tgqtop  23741  qtopcld  23742  ordthmeolem  23830  trfil2  23916  trfil3  23917  trnei  23921  ufildr  23960  fmfg  23978  rnelfm  23982  fmfnfm  23987  elflim  24000  flimrest  24012  cnflf  24031  cnflf2  24032  ptcmplem2  24082  ghmcnp  24144  tsmssubm  24172  iscfilu  24316  xmetgt0  24387  prdsxmetlem  24397  blcomps  24422  blcom  24423  xblpnfps  24424  xblpnf  24425  blpnf  24426  xmeter  24462  setsxms  24508  imasf1obl  24517  stdbdbl  24546  metrest  24553  metuel2  24594  dscopn  24602  xrtgioo  24836  metdstri  24881  cnmpopc  24959  iihalf2  24964  icopnfhmeo  24974  evth2  24991  lmmbr3  25291  iscau3  25309  metcld  25337  cfilucfil3  25351  srabn  25391  rrxmet  25439  minveclem4  25463  evthicc2  25491  ovolgelb  25511  shft2rab  25539  ovolshftlem1  25540  sca2rab  25543  ovolscalem1  25544  ioombl1lem4  25592  mbfmulc2lem  25678  ismbf3d  25685  mbfsup  25695  mbfinf  25696  i1f1lem  25720  i1fmulclem  25733  mbfi1fseqlem4  25749  itg2seq  25773  ditgneg  25888  limcdif  25907  limcnlp  25909  cnplimc  25918  rolle  26021  mvth  26023  dvne0  26042  lhop1lem  26044  itgsubst  26080  mdegle0  26106  deg1leb  26124  deg1le0  26140  q1peqb  26185  coemulhi  26283  dgrlt  26295  plydivlem3  26325  vieta1lem2  26341  aannenlem1  26358  ulmres  26417  reefiso  26477  pilem3  26482  ellogdm  26670  root1eq1  26786  angpieqvdlem  26859  angpieqvdlem2  26860  quad2  26870  1cubr  26873  quart  26892  rlimcnp  26996  wilthlem2  27099  isppw  27144  dvdsflsumcom  27218  fsumvma  27243  logfac2  27247  chpchtsum  27249  dchrmulcl  27279  dchrresb  27289  bclbnd  27310  bposlem1  27314  bposlem5  27318  gausslemma2dlem0c  27388  lgsquadlem1  27410  m1lgs  27418  2lgsoddprmlem2  27439  dchrisumlem3  27521  dchrisum0lem1  27546  ltsval2  27686  noextenddif  27698  lesloe  27784  lestri3  27785  eqcuts  27844  elmade2  27917  ltadds1  28051  negsunif  28114  ltsubs1  28135  ltsubadds2d  28149  mulsproplem12  28186  ltmuls2  28230  ltmuls1d  28232  divmulsw  28252  ltdivmuls2wd  28259  oniso  28330  n0subs  28422  n0lesltp1  28425  elzn0s  28457  avglts1d  28512  avglts2d  28513  bdaypw2n0bndlem  28522  z12sge0  28542  dfz12s2  28547  elreno2  28554  tgjustr  28609  trgcgrg  28650  lnrot1  28758  islnopp  28874  ismidb  28913  islmib  28922  axsegconlem6  29058  axeuclidlem  29098  axcontlem2  29101  axcontlem4  29103  axcontlem12  29111  ausgrusgrb  29301  nb3grpr2  29519  cplgr2v  29568  umgr2v2enb1  29662  crctcsh  29959  clwwlknonwwlknonb  30243  eupth2lems  30375  nmoreltpnf  30907  isblo2  30921  nmlnogt0  30935  phoeqi  30995  ubthlem2  31009  hire  31232  normgt0  31265  ho01i  31966  ho02i  31967  hoeq1  31968  hoeq2  31969  nmopreltpnf  32007  adjeq  32073  leop  32261  leopmul2i  32273  pjnormssi  32306  pjimai  32314  jplem1  32406  mddmd2  32447  mdslmd1lem1  32463  mdslmd1lem2  32464  superpos  32492  atnssm0  32514  dmdbr5ati  32560  disjunsn  32732  fcoinvbr  32743  ofpreima  32806  funcnv5mpt  32808  suppiniseg  32827  isoun  32843  fpwrelmapffslem  32873  fpwrelmap  32874  iocinioc2  32920  xrdifh  32921  nndiffz1  32927  sgn3da  32975  xdivmul  33052  cntzsnid  33210  cntrval2  33301  isarchi2  33315  erler  33395  elrsp  33504  lsmsnpridl  33530  lsmssass  33534  r1pid2OLD  33749  esplyind  33816  finexttrb  33906  algextdeglem6  33963  algextdeglem7  33964  smatrcl  34037  rhmpreimacnlem  34125  sqsscirc2  34150  xrmulc1cn  34171  esumfsup  34311  1stmbfm  34501  2ndmbfm  34502  mbfmcnt  34509  eulerpartlems  34601  eulerpartlemd  34607  ballotlemfc0  34734  ballotlemfcc  34735  ballotlemsima  34757  ballotlemfrcn0  34771  reprinfz1  34863  reprdifc  34868  bnj1173  35244  fineqvnttrclse  35365  vonf1owev  35396  zltp1ne  35398  lfuhgr2  35407  erdszelem7  35485  erdszelem9  35487  iscvm  35547  cvmlift3lem4  35610  rexxfr3dALT  35927  fscgr  36368  seglelin  36404  btwnoutside  36413  lineunray  36435  cldbnd  36624  isfne4  36638  fneval  36650  filnetlem4  36679  nndivsub  36755  bj-gabima  37363  dfgcd3  37754  fvineqsneu  37843  wl-sbhbt  37995  wl-sbcom2d  38002  wl-sbalnae  38003  sin2h  38047  cos2h  38048  matunitlindflem1  38053  matunitlindflem2  38054  matunitlindf  38055  ptrest  38056  poimirlem3  38060  poimirlem4  38061  poimirlem22  38079  poimirlem27  38084  mblfinlem3  38096  mblfinlem4  38097  ismblfin  38098  itg2addnclem  38108  itg2addnclem2  38109  itg2gt0cn  38112  iblabsnclem  38120  ftc1anclem6  38135  areacirclem2  38146  areacirclem5  38149  areacirc  38150  mettrifi  38194  drngoi  38388  eldm4  38718  exanres2  38740  disjecxrn  38849  exeupre  38928  brcoss2  38959  br1cossres2  38967  eldmcoss2  38986  eldm1cossres2  38988  brcosscnv2  39000  erimeq2  39200  disjqmap  39264  disjlem19  39341  prter3  39444  islshpat  39579  lsatnle  39606  ellkr2  39653  lshpkr  39679  lkr0f2  39723  lduallkr3  39724  lkreqN  39732  cvrval2  39836  isat3  39869  glbconN  39939  hlrelat5N  39963  cvrval4N  39976  atlt  39999  1cvrco  40034  pmaple  40323  isline2  40336  isline4N  40339  elpaddn0  40362  elpadd2at2  40369  cdlemkid4  41496  dia0  41614  cdlemm10N  41680  dibglbN  41728  dihmeetlem4preN  41868  dochkrshp3  41950  dvh4dimlem  42005  lcfl5  42058  mapdpglem3  42237  mapdheq  42290  hdmap1eq  42363  hdmapval2lem  42393  hdmapoc  42493  hlhillcs  42520  lcmineqlem18  42601  dvdsexpb  42882  renegadd  42919  resubadd  42926  redivmuld  42992  mulgt0b1d  43032  fsuppssind  43113  fz1eqin  43288  diophin  43291  jm2.19  43508  rmxdiophlem  43530  pw2f1ocnv  43552  wepwsolem  43557  gicabl  43614  idomodle  43706  onsupmaxb  43754  cantnf2  43840  tfsconcatb0  43859  tfsnfin  43867  ntrclsfveq2  44575  ntrclsss  44577  ntrclsk4  44586  extoimad  44678  radcnvrat  44828  bcc0  44854  supxrre3rnmpt  45941  clim2f  46148  clim2f2  46182  liminfreuzlem  46314  liminfltlem  46316  xlimmnflimsup2  46364  xlimpnfliminf2  46373  xlimlimsupleliminf  46375  opprb  47563  funbrafv2b  47691  dfafn5a  47692  leaddsuble  47829  mod2addne  47902  iccpartgtprec  47964  flsqrt  48140  dfeven2  48209  dfodd3  48210  lindslinindimp2lem4  49021  snlindsntor  49031  regt1loggt0  49096  elbigo2  49112  elbigolo1  49117  fldivexpfllog2  49125  nnlog2ge0lt1  49126  blenpw2m1  49139  naryfvalelwrdf  49193  isprsd  49514  resccatlem  49632  functhinclem1  50003  thincciso  50012  thinciso  50029  isinito2lem  50057  fulltermc  50070  prstcprs  50119  oduoppcciso  50125  postc  50128  lmdran  50230  cmdlan  50231