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  541  mpbirand  703  sb3b  2478  sbcom3  2511  sbal1  2534  sbal2  2535  2reu4lem  4461  issn  4768  disjprgw  5073  disjprg  5074  reuhypd  5345  ordtri3  6299  ordsssuc  6349  iota1  6407  funbrfv2b  6821  dffn5  6822  feqmptdf  6833  unima  6837  dmfco  6858  fneqeql  6917  f1ompt  6979  dff13  7122  fliftcnv  7175  soisores  7191  isotr  7200  isoini  7202  caovord3  7476  releldm2  7870  fimaproj  7960  brtpos  8035  tpostpos  8046  oe1m  8352  oawordri  8357  oalimcl  8367  omlimcl  8385  omabs  8455  iserd  8498  qliftel  8563  qliftfun  8565  qliftf  8568  ecopovsym  8582  pw2f1olem  8832  mapen  8893  suppeqfsuppbi  9103  mapfien  9128  supisolem  9193  cantnflem1  9408  wemapwe  9416  rankr1clem  9562  rankr1c  9563  ranklim  9586  r1pwALT  9588  r1pwcl  9589  isfin1-2  10125  isfin1-4  10127  fin71num  10137  axdc3lem2  10191  ltmnq  10712  prlem936  10787  ltsosr  10834  ltasr  10840  xrlenlt  11024  ltxrlt  11029  letri3  11044  ne0gt0  11063  subadd  11207  ltsubadd2  11429  lesubadd2  11431  suble  11436  ltsub23  11438  ltaddpos2  11449  ltsubpos  11450  subge02  11474  ltord2  11487  leord2  11488  ltaddsublt  11585  divmul  11619  divmul3  11621  rec11r  11657  ltdiv1  11822  ltdivmul2  11835  ledivmul2  11837  ltrec  11840  ltdiv2  11844  negfi  11907  negiso  11938  nnle1eq1  11986  avgle1  12196  avgle2  12197  avgle  12198  nn0le0eq0  12244  elz2  12320  znnnlt1  12330  zleltp1  12354  difrp  12750  xrltlen  12862  dfle2  12863  xrletri3  12870  xgepnf  12881  xlemnf  12883  qbtwnre  12915  xltnegi  12932  supxrre  13043  infxrre  13052  elioo5  13118  elfz5  13230  elfzm11  13309  predfz  13363  flbi  13517  flbi2  13518  fldiv4lem1div2uz2  13537  fznnfl  13563  zmodid2  13600  2submod  13633  lt2sq  13833  le2sq  13834  sqlecan  13906  bcval5  14013  pfxsuffeqwrdeq  14392  shftfib  14764  mulre  14813  cnpart  14932  sqrlem6  14940  sqrmo  14944  elicc4abs  15012  abs2difabs  15027  cau4  15049  limsupgre  15171  clim2  15194  ello1mpt2  15212  lo1resb  15254  o1resb  15256  climeq  15257  climmpt2  15263  isercoll  15360  caucvgb  15372  fsumabs  15494  isumshft  15532  geomulcvg  15569  absefib  15888  dvdsval3  15948  dvdsabseq  16003  dvdsflip  16007  dvdsssfz1  16008  mod2eq1n2dvds  16037  ndvdsadd  16100  bitscmp  16126  smupvallem  16171  dvdssq  16253  lcmdvds  16294  ncoprmgcdgt1b  16337  isprm3  16369  isprm5  16393  phiprmpw  16458  prmdiv  16467  pc11  16562  pcz  16563  pockthlem  16587  prmreclem2  16599  prmreclem4  16601  prmreclem6  16603  1arith  16609  vdwapun  16656  rami  16697  ramcl  16711  pwsle  17184  ercpbllem  17240  invsym  17455  funcres2c  17598  latnle  18172  grpinvcnv  18624  subgacs  18770  eqger  18787  gexdvds2  19171  pgpfi1  19181  pgpfi  19191  lsmass  19256  lssnle  19261  lsmdisj3b  19277  lsmhash  19292  ablsubadd  19394  gsumval3lem2  19488  subgdmdprd  19618  pgpfac1lem2  19659  dvdsr02  19879  drngid2  19988  issubrg3  20033  sdrgacs  20050  lssacs  20210  prmirred  20677  chrdvds  20713  chrcong  20714  chrnzr  20715  znleval  20743  znleval2  20744  cygznlem3  20758  frlmbas  20943  elfilspd  20991  lindfmm  21015  islindf4  21026  islindf5  21027  psrbaglefi  21116  psrbaglefiOLD  21117  coe1mul2lem1  21419  mdetunilem9  21750  isneip  22237  neiptopnei  22264  lpdifsn  22275  restopnb  22307  restopn2  22309  restdis  22310  restperf  22316  lmbr2  22391  cncls2  22405  cnprest  22421  cnprest2  22422  iscnrm2  22470  ist0-2  22476  ist1-3  22481  ishaus2  22483  cmpfi  22540  dfconn2  22551  1stccnp  22594  subislly  22613  hausmapdom  22632  tx1cn  22741  tx2cn  22742  txcnmpt  22756  txrest  22763  hauseqlcld  22778  tgqtop  22844  qtopcld  22845  ordthmeolem  22933  trfil2  23019  trfil3  23020  trnei  23024  ufildr  23063  fmfg  23081  rnelfm  23085  fmfnfm  23090  elflim  23103  flimrest  23115  cnflf  23134  cnflf2  23135  ptcmplem2  23185  ghmcnp  23247  tsmssubm  23275  iscfilu  23421  xmetgt0  23492  prdsxmetlem  23502  blcomps  23527  blcom  23528  xblpnfps  23529  xblpnf  23530  blpnf  23531  xmeter  23567  setsxms  23615  imasf1obl  23625  stdbdbl  23654  metrest  23661  metuel2  23702  dscopn  23710  xrtgioo  23950  metdstri  23995  cnmpopc  24072  iihalf2  24077  icopnfhmeo  24087  evth2  24104  lmmbr3  24405  iscau3  24423  metcld  24451  cfilucfil3  24465  srabn  24505  rrxmet  24553  minveclem4  24577  evthicc2  24605  ovolgelb  24625  shft2rab  24653  ovolshftlem1  24654  sca2rab  24657  ovolscalem1  24658  ioombl1lem4  24706  mbfmulc2lem  24792  ismbf3d  24799  mbfsup  24809  mbfinf  24810  i1f1lem  24834  i1fmulclem  24848  mbfi1fseqlem4  24864  itg2seq  24888  ditgneg  25002  limcdif  25021  limcnlp  25023  cnplimc  25032  rolle  25135  mvth  25137  dvne0  25156  lhop1lem  25158  itgsubst  25194  mdegle0  25223  deg1leb  25241  deg1le0  25257  q1peqb  25300  coemulhi  25396  dgrlt  25408  plydivlem3  25436  vieta1lem2  25452  aannenlem1  25469  ulmres  25528  reefiso  25588  pilem3  25593  ellogdm  25775  root1eq1  25889  angpieqvdlem  25959  angpieqvdlem2  25960  quad2  25970  1cubr  25973  quart  25992  rlimcnp  26096  wilthlem2  26199  isppw  26244  dvdsflsumcom  26318  fsumvma  26342  logfac2  26346  chpchtsum  26348  dchrmulcl  26378  dchrresb  26388  bclbnd  26409  bposlem1  26413  bposlem5  26417  gausslemma2dlem0c  26487  lgsquadlem1  26509  m1lgs  26517  2lgsoddprmlem2  26538  dchrisumlem3  26620  dchrisum0lem1  26645  tgjustr  26816  trgcgrg  26857  lnrot1  26965  islnopp  27081  ismidb  27120  islmib  27129  axsegconlem6  27271  axeuclidlem  27311  axcontlem2  27314  axcontlem4  27316  axcontlem12  27324  ausgrusgrb  27516  nb3grpr2  27731  cplgr2v  27780  umgr2v2enb1  27874  crctcsh  28168  clwwlknonwwlknonb  28449  eupth2lems  28581  nmoreltpnf  29110  isblo2  29124  nmlnogt0  29138  phoeqi  29198  ubthlem2  29212  hire  29435  normgt0  29468  ho01i  30169  ho02i  30170  hoeq1  30171  hoeq2  30172  nmopreltpnf  30210  adjeq  30276  leop  30464  leopmul2i  30476  pjnormssi  30509  pjimai  30517  jplem1  30609  mddmd2  30650  mdslmd1lem1  30666  mdslmd1lem2  30667  superpos  30695  atnssm0  30717  dmdbr5ati  30763  disjunsn  30912  fcoinvbr  30926  ofpreima  30981  funcnv5mpt  30984  suppiniseg  30999  isoun  31013  fpwrelmapffslem  31046  fpwrelmap  31047  iocinioc2  31079  xrdifh  31080  nndiffz1  31086  xdivmul  31178  cntzsnid  31300  isarchi2  31418  elrsp  31548  lsmsnpridl  31565  lsmssass  31569  finexttrb  31716  smatrcl  31725  rhmpreimacnlem  31813  sqsscirc2  31838  xrmulc1cn  31859  esumfsup  32017  1stmbfm  32206  2ndmbfm  32207  mbfmcnt  32214  eulerpartlems  32306  eulerpartlemd  32312  ballotlemfc0  32438  ballotlemfcc  32439  ballotlemsima  32461  ballotlemfrcn0  32475  sgn3da  32487  reprinfz1  32581  reprdifc  32586  bnj1173  32961  zltp1ne  33047  lfuhgr2  33059  erdszelem7  33138  erdszelem9  33140  iscvm  33200  cvmlift3lem4  33263  sltval2  33838  noextenddif  33850  sleloe  33936  sletri3  33937  eqscut  33978  elmade2  34031  fscgr  34361  seglelin  34397  btwnoutside  34406  lineunray  34428  cldbnd  34494  isfne4  34508  fneval  34520  filnetlem4  34549  nndivsub  34625  bj-gabima  35107  dfgcd3  35474  fvineqsneu  35561  wl-sbhbt  35688  wl-sbcom2d  35695  wl-sbalnae  35696  wl-ax11-lem8  35722  sin2h  35746  cos2h  35747  matunitlindflem1  35752  matunitlindflem2  35753  matunitlindf  35754  ptrest  35755  poimirlem3  35759  poimirlem4  35760  poimirlem22  35778  poimirlem27  35783  mblfinlem3  35795  mblfinlem4  35796  ismblfin  35797  itg2addnclem  35807  itg2addnclem2  35808  itg2gt0cn  35811  iblabsnclem  35819  ftc1anclem6  35834  areacirclem2  35845  areacirclem5  35848  areacirc  35849  mettrifi  35894  drngoi  36088  eldm4  36388  exanres2  36411  brcoss2  36534  br1cossres2  36542  eldmcoss2  36556  eldm1cossres2  36558  brcosscnv2  36570  erim2  36768  prter3  36875  islshpat  37010  lsatnle  37037  ellkr2  37084  lshpkr  37110  lkr0f2  37154  lduallkr3  37155  lkreqN  37163  cvrval2  37267  isat3  37300  glbconN  37370  hlrelat5N  37394  cvrval4N  37407  atlt  37430  1cvrco  37465  pmaple  37754  isline2  37767  isline4N  37770  elpaddn0  37793  elpadd2at2  37800  cdlemkid4  38927  dia0  39045  cdlemm10N  39111  dibglbN  39159  dihmeetlem4preN  39299  dochkrshp3  39381  dvh4dimlem  39436  lcfl5  39489  mapdpglem3  39668  mapdheq  39721  hdmap1eq  39794  hdmapval2lem  39824  hdmapoc  39924  hlhillcs  39955  lcmineqlem18  40034  fsuppssind  40262  dvdsexpb  40322  renegadd  40335  resubadd  40342  mulgt0b2d  40410  fz1eqin  40571  diophin  40574  jm2.19  40795  rmxdiophlem  40817  pw2f1ocnv  40839  wepwsolem  40847  gicabl  40904  idomodle  41001  isdomn3  41009  ntrclsfveq2  41624  ntrclsss  41626  ntrclsk4  41635  extoimad  41728  radcnvrat  41885  bcc0  41911  supxrre3rnmpt  42923  clim2f  43131  clim2f2  43165  liminfreuzlem  43297  liminfltlem  43299  xlimmnflimsup2  43347  xlimpnfliminf2  43356  xlimlimsupleliminf  43358  opprb  44476  funbrafv2b  44602  dfafn5a  44603  leaddsuble  44741  iccpartgtprec  44824  flsqrt  44997  dfeven2  45053  dfodd3  45054  lindslinindimp2lem4  45754  snlindsntor  45764  regt1loggt0  45834  elbigo2  45850  elbigolo1  45855  fldivexpfllog2  45863  nnlog2ge0lt1  45864  blenpw2m1  45877  naryfvalelwrdf  45931  isprsd  46201  functhinclem1  46274  thincciso  46282  thinciso  46293  prstcprs  46308  postc  46315