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  2480  sbcom3  2510  sbal1  2532  sbal2  2533  2reu4lem  4497  issn  4808  disjprg  5115  reuhypd  5389  snelpwg  5417  ordtri3  6388  ordsssuc  6442  iota1  6507  funbrfv2b  6935  dffn5  6936  feqmptdf  6948  unima  6953  dmfco  6974  fneqeql  7035  f1ompt  7100  dff13  7246  fliftcnv  7303  soisores  7319  isotr  7328  isoini  7330  caovord3  7618  releldm2  8040  fimaproj  8132  brtpos  8232  tpostpos  8243  oe1m  8555  oawordri  8560  oalimcl  8570  omlimcl  8588  omabs  8661  iserd  8743  qliftel  8812  qliftfun  8814  qliftf  8817  ecopovsym  8831  pw2f1olem  9088  mapen  9153  findcard3  9288  suppeqfsuppbi  9389  mapfien  9418  supisolem  9484  cantnflem1  9701  wemapwe  9709  rankr1clem  9832  rankr1c  9833  ranklim  9856  r1pwALT  9858  r1pwcl  9859  isfin1-2  10397  isfin1-4  10399  fin71num  10409  axdc3lem2  10463  ltmnq  10984  prlem936  11059  ltsosr  11106  ltasr  11112  xrlenlt  11298  ltxrlt  11303  letri3  11318  ne0gt0  11338  subadd  11483  ltsubadd2  11706  lesubadd2  11708  suble  11713  ltsub23  11715  ltaddpos2  11726  ltsubpos  11727  subge02  11751  ltord2  11764  leord2  11765  ltaddsublt  11862  divmul  11897  divmul3  11899  rec11r  11938  ltdiv1  12104  ltdivmul2  12117  ledivmul2  12119  ltrec  12122  ltdiv2  12126  negfi  12189  negiso  12220  nnle1eq1  12268  avgle1  12479  avgle2  12480  avgle  12481  nn0le0eq0  12527  elz2  12604  znnnlt1  12617  zleltp1  12641  difrp  13045  xrltlen  13160  dfle2  13161  xrletri3  13168  xgepnf  13179  xlemnf  13181  qbtwnre  13213  xltnegi  13230  supxrre  13341  infxrre  13351  elioo5  13418  elfz5  13531  elfzm11  13610  predfz  13668  flbi  13831  flbi2  13832  fldiv4lem1div2uz2  13851  fznnfl  13877  zmodid2  13914  2submod  13948  lt2sq  14149  le2sq  14150  sqlecan  14225  bcval5  14334  pfxsuffeqwrdeq  14714  shftfib  15089  mulre  15138  cnpart  15257  01sqrexlem6  15264  sqrmo  15268  elicc4abs  15336  abs2difabs  15351  cau4  15373  limsupgre  15495  clim2  15518  ello1mpt2  15536  lo1resb  15578  o1resb  15580  climeq  15581  climmpt2  15587  isercoll  15682  caucvgb  15694  fsumabs  15815  isumshft  15853  geomulcvg  15890  absefib  16214  dvdsval3  16274  addmulmodb  16283  dvdsabseq  16330  dvdsflip  16334  dvdsssfz1  16335  mod2eq1n2dvds  16364  ndvdsadd  16427  bitscmp  16455  smupvallem  16500  dvdssq  16584  lcmdvds  16625  ncoprmgcdgt1b  16668  isprm3  16700  isprm5  16724  phiprmpw  16793  prmdiv  16802  pc11  16898  pcz  16899  pockthlem  16923  prmreclem2  16935  prmreclem4  16937  prmreclem6  16939  1arith  16945  vdwapun  16992  rami  17033  ramcl  17047  pwsle  17504  ercpbllem  17560  invsym  17773  funcres2c  17914  latnle  18481  grpinvcnv  18987  subgacs  19142  eqger  19159  ghmqusker  19268  gexdvds2  19564  pgpfi1  19574  pgpfi  19584  lsmass  19648  lssnle  19653  lsmdisj3b  19669  lsmhash  19684  ablsubadd  19788  gsumval3lem2  19885  subgdmdprd  20015  pgpfac1lem2  20056  dvdsr02  20330  issubrg3  20558  isdomn3  20673  drngid2  20710  sdrgunit  20754  sdrgacs  20759  lssacs  20922  prmirred  21433  chrdvds  21485  chrcong  21486  chrnzr  21489  znleval  21513  znleval2  21514  cygznlem3  21528  frlmbas  21713  elfilspd  21761  lindfmm  21785  islindf4  21796  islindf5  21797  psrbaglefi  21884  coe1mul2lem1  22202  mdetunilem9  22556  isneip  23041  neiptopnei  23068  lpdifsn  23079  restopnb  23111  restopn2  23113  restdis  23114  restperf  23120  lmbr2  23195  cncls2  23209  cnprest  23225  cnprest2  23226  iscnrm2  23274  ist0-2  23280  ist1-3  23285  ishaus2  23287  cmpfi  23344  dfconn2  23355  1stccnp  23398  subislly  23417  hausmapdom  23436  tx1cn  23545  tx2cn  23546  txcnmpt  23560  txrest  23567  hauseqlcld  23582  tgqtop  23648  qtopcld  23649  ordthmeolem  23737  trfil2  23823  trfil3  23824  trnei  23828  ufildr  23867  fmfg  23885  rnelfm  23889  fmfnfm  23894  elflim  23907  flimrest  23919  cnflf  23938  cnflf2  23939  ptcmplem2  23989  ghmcnp  24051  tsmssubm  24079  iscfilu  24224  xmetgt0  24295  prdsxmetlem  24305  blcomps  24330  blcom  24331  xblpnfps  24332  xblpnf  24333  blpnf  24334  xmeter  24370  setsxms  24416  imasf1obl  24425  stdbdbl  24454  metrest  24461  metuel2  24502  dscopn  24510  xrtgioo  24744  metdstri  24789  cnmpopc  24871  iihalf2  24877  icopnfhmeo  24890  evth2  24908  lmmbr3  25210  iscau3  25228  metcld  25256  cfilucfil3  25270  srabn  25310  rrxmet  25358  minveclem4  25382  evthicc2  25411  ovolgelb  25431  shft2rab  25459  ovolshftlem1  25460  sca2rab  25463  ovolscalem1  25464  ioombl1lem4  25512  mbfmulc2lem  25598  ismbf3d  25605  mbfsup  25615  mbfinf  25616  i1f1lem  25640  i1fmulclem  25653  mbfi1fseqlem4  25669  itg2seq  25693  ditgneg  25808  limcdif  25827  limcnlp  25829  cnplimc  25838  rolle  25944  mvth  25947  dvne0  25966  lhop1lem  25968  itgsubst  26006  mdegle0  26032  deg1leb  26050  deg1le0  26066  q1peqb  26111  coemulhi  26209  dgrlt  26222  plydivlem3  26253  vieta1lem2  26269  aannenlem1  26286  ulmres  26347  reefiso  26408  pilem3  26413  ellogdm  26598  root1eq1  26715  angpieqvdlem  26788  angpieqvdlem2  26789  quad2  26799  1cubr  26802  quart  26821  rlimcnp  26925  wilthlem2  27029  isppw  27074  dvdsflsumcom  27148  fsumvma  27174  logfac2  27178  chpchtsum  27180  dchrmulcl  27210  dchrresb  27220  bclbnd  27241  bposlem1  27245  bposlem5  27249  gausslemma2dlem0c  27319  lgsquadlem1  27341  m1lgs  27349  2lgsoddprmlem2  27370  dchrisumlem3  27452  dchrisum0lem1  27477  sltval2  27618  noextenddif  27630  sleloe  27716  sletri3  27717  eqscut  27767  elmade2  27824  sltadd1  27942  negsunif  28004  sltsub1  28023  sltsubadd2d  28037  mulsproplem12  28070  sltmul2  28114  sltmul1d  28116  divsmulw  28135  sltdivmul2wd  28142  n0subs  28277  elzn0s  28301  tgjustr  28399  trgcgrg  28440  lnrot1  28548  islnopp  28664  ismidb  28703  islmib  28712  axsegconlem6  28847  axeuclidlem  28887  axcontlem2  28890  axcontlem4  28892  axcontlem12  28900  ausgrusgrb  29090  nb3grpr2  29308  cplgr2v  29357  umgr2v2enb1  29452  crctcsh  29752  clwwlknonwwlknonb  30033  eupth2lems  30165  nmoreltpnf  30696  isblo2  30710  nmlnogt0  30724  phoeqi  30784  ubthlem2  30798  hire  31021  normgt0  31054  ho01i  31755  ho02i  31756  hoeq1  31757  hoeq2  31758  nmopreltpnf  31796  adjeq  31862  leop  32050  leopmul2i  32062  pjnormssi  32095  pjimai  32103  jplem1  32195  mddmd2  32236  mdslmd1lem1  32252  mdslmd1lem2  32253  superpos  32281  atnssm0  32303  dmdbr5ati  32349  disjunsn  32521  fcoinvbr  32532  ofpreima  32589  funcnv5mpt  32592  suppiniseg  32609  isoun  32625  fpwrelmapffslem  32655  fpwrelmap  32656  iocinioc2  32702  xrdifh  32703  nndiffz1  32709  sgn3da  32759  xdivmul  32845  cntzsnid  33009  isarchi2  33129  erler  33206  elrsp  33333  lsmsnpridl  33359  lsmssass  33363  r1pid2OLD  33564  finexttrb  33652  algextdeglem6  33702  algextdeglem7  33703  smatrcl  33773  rhmpreimacnlem  33861  sqsscirc2  33886  xrmulc1cn  33907  esumfsup  34047  1stmbfm  34238  2ndmbfm  34239  mbfmcnt  34246  eulerpartlems  34338  eulerpartlemd  34344  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemsima  34494  ballotlemfrcn0  34508  reprinfz1  34600  reprdifc  34605  bnj1173  34979  zltp1ne  35078  lfuhgr2  35087  erdszelem7  35165  erdszelem9  35167  iscvm  35227  cvmlift3lem4  35290  rexxfr3dALT  35607  fscgr  36044  seglelin  36080  btwnoutside  36089  lineunray  36111  cldbnd  36290  isfne4  36304  fneval  36316  filnetlem4  36345  nndivsub  36421  bj-gabima  36904  dfgcd3  37288  fvineqsneu  37375  wl-sbhbt  37518  wl-sbcom2d  37525  wl-sbalnae  37526  wl-ax11-lem8  37556  sin2h  37580  cos2h  37581  matunitlindflem1  37586  matunitlindflem2  37587  matunitlindf  37588  ptrest  37589  poimirlem3  37593  poimirlem4  37594  poimirlem22  37612  poimirlem27  37617  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  itg2addnclem  37641  itg2addnclem2  37642  itg2gt0cn  37645  iblabsnclem  37653  ftc1anclem6  37668  areacirclem2  37679  areacirclem5  37682  areacirc  37683  mettrifi  37727  drngoi  37921  eldm4  38238  exanres2  38261  disjecxrn  38353  brcoss2  38396  br1cossres2  38404  eldmcoss2  38423  eldm1cossres2  38425  brcosscnv2  38437  erimeq2  38642  disjlem19  38765  prter3  38846  islshpat  38981  lsatnle  39008  ellkr2  39055  lshpkr  39081  lkr0f2  39125  lduallkr3  39126  lkreqN  39134  cvrval2  39238  isat3  39271  glbconN  39341  glbconNOLD  39342  hlrelat5N  39366  cvrval4N  39379  atlt  39402  1cvrco  39437  pmaple  39726  isline2  39739  isline4N  39742  elpaddn0  39765  elpadd2at2  39772  cdlemkid4  40899  dia0  41017  cdlemm10N  41083  dibglbN  41131  dihmeetlem4preN  41271  dochkrshp3  41353  dvh4dimlem  41408  lcfl5  41461  mapdpglem3  41640  mapdheq  41693  hdmap1eq  41766  hdmapval2lem  41796  hdmapoc  41896  hlhillcs  41923  lcmineqlem18  42005  dvdsexpb  42331  renegadd  42362  resubadd  42369  mulgt0b2d  42450  fsuppssind  42563  fz1eqin  42739  diophin  42742  jm2.19  42964  rmxdiophlem  42986  pw2f1ocnv  43008  wepwsolem  43013  gicabl  43070  idomodle  43162  onsupmaxb  43210  cantnf2  43296  tfsconcatb0  43315  tfsnfin  43323  ntrclsfveq2  44032  ntrclsss  44034  ntrclsk4  44043  extoimad  44135  radcnvrat  44286  bcc0  44312  supxrre3rnmpt  45404  clim2f  45613  clim2f2  45647  liminfreuzlem  45779  liminfltlem  45781  xlimmnflimsup2  45829  xlimpnfliminf2  45838  xlimlimsupleliminf  45840  opprb  47008  funbrafv2b  47136  dfafn5a  47137  leaddsuble  47274  iccpartgtprec  47382  flsqrt  47555  dfeven2  47611  dfodd3  47612  lindslinindimp2lem4  48385  snlindsntor  48395  regt1loggt0  48464  elbigo2  48480  elbigolo1  48485  fldivexpfllog2  48493  nnlog2ge0lt1  48494  blenpw2m1  48507  naryfvalelwrdf  48561  isprsd  48877  resccatlem  48988  functhinclem1  49278  thincciso  49287  thinciso  49304  isinito2lem  49331  fulltermc  49344  prstcprs  49385  oduoppcciso  49391  postc  49394