Theorem bitr4d 270

Description: Deduction form of bitr4i 266. (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 212	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 267	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  3bitr2d  295  3bitr2rd  296  3bitr4d  299  3bitr4rd  300  mpbirand  529  bianabs  920  sbcom3  2399  sbal1  2448  sbal2  2449  issn  4303  disjprg  4578  reuhypd  4821  ordtri3  5676  ordsssuc  5729  iota1  5782  funbrfv2b  6150  dffn5  6151  feqmptdf  6161  dmfco  6182  fneqeql  6233  f1ompt  6290  dff13  6416  fliftcnv  6461  soisores  6477  isotr  6486  isoini  6488  caovord3  6745  releldm2  7109  brtpos  7248  tpostpos  7259  oe1m  7512  oawordri  7517  oalimcl  7527  omlimcl  7545  omabs  7614  iserd  7655  qliftel  7717  qliftfun  7719  qliftf  7722  ecopovsym  7736  pw2f1olem  7949  mapen  8009  suppeqfsuppbi  8172  funsnfsupp  8182  mapfien  8196  supisolem  8262  cantnflem1  8469  wemapwe  8477  rankr1clem  8566  rankr1c  8567  ranklim  8590  r1pwALT  8592  r1pwcl  8593  isfin1-2  9090  isfin1-4  9092  fin71num  9102  axdc3lem2  9156  ltmnq  9673  prlem936  9748  ltsosr  9794  ltasr  9800  xrlenlt  9982  ltxrlt  9987  letri3  10002  ne0gt0  10021  subadd  10163  ltsubadd2  10378  lesubadd2  10380  suble  10385  ltsub23  10387  ltaddpos2  10398  ltsubpos  10399  subge02  10423  ltord2  10436  leord2  10437  ltaddsublt  10533  divmul  10567  divmul3  10569  rec11r  10603  ltdiv1  10766  ltdivmul2  10779  ledivmul2  10781  ltrec  10784  ltdiv2  10788  negfi  10850  negiso  10880  nnle1eq1  10925  avgle1  11149  avgle2  11150  avgle  11151  nn0le0eq0  11198  elz2  11271  znnnlt1  11281  zleltp1  11305  uzin  11596  difrp  11744  xrltlen  11855  dfle2  11856  xrletri3  11861  qbtwnre  11904  xltnegi  11921  supxrre  12029  supxrre1  12032  infxrre  12038  ixxun  12062  elioo5  12102  elfz5  12205  elfzm11  12280  uzsplit  12281  predfz  12333  flbi  12479  flbi2  12480  fldiv4lem1div2uz2  12499  fznnfl  12523  zmodid2  12560  2submod  12593  lt2sq  12799  le2sq  12800  sqlecan  12833  bcval5  12967  shftfib  13660  mulre  13709  cnpart  13828  sqrlem6  13836  sqrmo  13840  elicc4abs  13907  abs2difabs  13922  cau4  13944  limsupgre  14060  clim2  14083  ello12  14095  ello1mpt2  14101  elo12  14106  lo1resb  14143  o1resb  14145  climeq  14146  climmpt2  14152  isercoll  14246  caucvgb  14258  fsumss  14303  fsumabs  14374  isumshft  14410  geomulcvg  14446  fprodss  14517  absefib  14767  dvdsval3  14825  dvdsabseq  14873  dvdsflip  14877  dvdsssfz1  14878  mod2eq1n2dvds  14909  ndvdsadd  14972  bitscmp  14998  smupvallem  15043  dvdssq  15118  lcmdvds  15159  ncoprmgcdgt1b  15202  coprmdvdsOLD  15205  isprm3  15234  isprm5  15257  phiprmpw  15319  prmdiv  15328  pc11  15422  pcz  15423  pockthlem  15447  prmreclem2  15459  prmreclem4  15461  prmreclem6  15463  1arith  15469  vdwapun  15516  ramval  15550  rami  15557  ramcl  15571  pwsle  15975  ercpbllem  16031  invsym  16245  funcres2c  16384  latnle  16908  grpinvcnv  17306  subgacs  17452  eqger  17467  gexdvds2  17823  pgpfi1  17833  pgpfi  17843  lsmass  17906  lssnle  17910  lsmdisj3b  17926  lsmhash  17941  ablsubadd  18040  gsumval3lem2  18130  subgdmdprd  18256  pgpfac1lem2  18297  dvdsr02  18479  drngid2  18586  issubrg3  18631  lssacs  18788  lspsnel5  18816  psrbaglefi  19193  coe1mul2lem1  19458  prmirred  19662  chrdvds  19695  chrcong  19696  chrnzr  19697  znleval  19722  znleval2  19723  cygznlem3  19737  frlmbas  19918  elfilspd  19961  lindfmm  19985  islindf4  19996  islindf5  19997  mdetunilem9  20245  discld  20703  isneip  20719  neiptopnei  20746  lpdifsn  20757  restopnb  20789  restopn2  20791  restdis  20792  restperf  20798  lmbr2  20873  cncls2  20887  cnprest  20903  cnprest2  20904  iscnrm2  20952  ist0-2  20958  cnt0  20960  ist1-3  20963  ishaus2  20965  cmpfi  21021  dfcon2  21032  1stccnp  21075  1stccn  21076  subislly  21094  hausmapdom  21113  kgencn  21169  tx1cn  21222  tx2cn  21223  txcnmpt  21237  txrest  21244  hauseqlcld  21259  tgqtop  21325  qtopcld  21326  qtopcn  21327  ordthmeolem  21414  trfil2  21501  trfil3  21502  trnei  21506  ufildr  21545  fmfg  21563  rnelfm  21567  fmfnfm  21572  elflim  21585  fbflim  21590  flimrest  21597  isflf  21607  cnflf  21616  cnflf2  21617  fclscf  21639  cnfcf  21656  ptcmplem2  21667  ghmcnp  21728  tsmssubm  21756  iscfilu  21902  xmetgt0  21973  prdsxmetlem  21983  elbl2ps  22004  elbl2  22005  blcomps  22008  blcom  22009  xblpnfps  22010  xblpnf  22011  blpnf  22012  xmeter  22048  setsxms  22094  imasf1obl  22103  stdbdbl  22132  metrest  22139  metcn  22158  txmetcn  22163  metuel2  22180  dscopn  22188  xrtgioo  22417  metdstri  22462  cncffvrn  22509  cnmpt2pc  22535  iihalf2  22540  icopnfhmeo  22550  evth2  22567  lmmbr3  22866  iscau3  22884  lmclimf  22910  metcld  22912  cfilucfil3  22925  srabn  22964  rrxmet  22999  minveclem4  23011  evthicc2  23036  ovolfioo  23043  ovolficc  23044  ovolgelb  23055  ovoliun  23080  shft2rab  23083  ovolshftlem1  23084  sca2rab  23087  ovolscalem1  23088  ismbl2  23102  ioombl1lem4  23136  mbfmulc2lem  23220  mbfmax  23222  mbfposr  23225  ismbf3d  23227  mbfaddlem  23233  mbfsup  23237  mbfinf  23238  i1f1lem  23262  i1fmulclem  23275  mbfi1fseqlem4  23291  itg2seq  23315  itg2monolem1  23323  itg2cnlem1  23334  itgfsum  23399  ditgneg  23427  limcdif  23446  limcnlp  23448  cnplimc  23457  rolle  23557  mvth  23559  dvne0  23578  lhop1lem  23580  itgsubst  23616  mdegle0  23641  deg1leb  23659  deg1le0  23675  q1peqb  23718  coemulhi  23814  dgrlt  23826  plydivlem3  23854  vieta1lem2  23870  aannenlem1  23887  ulmres  23946  reefiso  24006  pilem3  24011  ellogdm  24185  root1eq1  24296  angpieqvdlem  24355  angpieqvdlem2  24356  quad2  24366  1cubr  24369  quart  24388  rlimcnp  24492  wilthlem2  24595  isppw  24640  dvdsflsumcom  24714  fsumvma  24738  logfac2  24742  chpchtsum  24744  dchrmulcl  24774  dchreq  24783  dchrresb  24784  bclbnd  24805  bposlem1  24809  bposlem5  24813  lgsneg  24846  gausslemma2dlem0c  24883  lgsquadlem1  24905  lgsquadlem2  24906  m1lgs  24913  2lgsoddprmlem2  24934  dchrisumlem3  24980  dchrisum0lem1  25005  trgcgrg  25210  tgellng  25248  lnrot1  25318  islnopp  25431  ismidb  25470  islmib  25479  isleag  25533  ttgelitv  25563  axsegconlem6  25602  axeuclidlem  25642  axcontlem2  25645  axcontlem4  25647  axcontlem12  25655  dfconngra1  26199  clwwlkn2  26303  eupath2  26507  frgra3v  26529  nmoreltpnf  27008  isblo2  27022  nmlnogt0  27036  phoeqi  27097  ubthlem2  27111  hire  27335  normgt0  27368  ho01i  28071  ho02i  28072  hoeq1  28073  hoeq2  28074  nmopreltpnf  28112  adjeq  28178  leop  28366  leopmul2i  28378  pjnormssi  28411  pjimai  28419  jplem1  28511  mddmd2  28552  mdslmd1lem1  28568  mdslmd1lem2  28569  superpos  28597  atnssm0  28619  dmdbr5ati  28665  disjunsn  28789  fcoinvbr  28799  ofpreima  28848  funcnv5mpt  28852  isoun  28862  fpwrelmapffslem  28895  fpwrelmap  28896  xgepnf  28904  xlemnf  28905  iocinioc2  28931  xrdifh  28932  nndiffz1  28936  xdivmul  28964  isarchi2  29070  smatrcl  29190  fimaproj  29228  sqsscirc2  29283  xrmulc1cn  29304  ismntoplly  29397  esumfsup  29459  1stmbfm  29649  2ndmbfm  29650  mbfmcnt  29657  eulerpartlems  29749  eulerpartlemd  29755  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemsima  29904  ballotlemfrcn0  29918  sgn3da  29930  bnj1173  30324  erdszelem7  30433  erdszelem9  30435  iscvm  30495  cvmlift3lem4  30558  sltval2  31053  fscgr  31357  seglelin  31393  btwnoutside  31402  lineunray  31424  cldbnd  31491  isfne4  31505  fneval  31517  filnetlem4  31546  nndivsub  31626  wl-sbhbt  32514  wl-sbcom2d  32523  wl-sbalnae  32524  wl-ax11-lem8  32548  sin2h  32569  cos2h  32570  matunitlindflem1  32575  matunitlindflem2  32576  matunitlindf  32577  ptrest  32578  poimirlem3  32582  poimirlem4  32583  poimirlem22  32601  poimirlem27  32606  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  itg2addnclem  32631  itg2addnclem2  32632  itg2gt0cn  32635  iblabsnclem  32643  ftc1anclem6  32660  areacirclem2  32671  areacirclem5  32674  areacirc  32675  cover2  32678  mettrifi  32723  drngoi  32920  prter3  33185  islshpat  33322  lsatnle  33349  ellkr2  33396  lshpkr  33422  lkr0f2  33466  lduallkr3  33467  lkreqN  33475  cvrval2  33579  isat3  33612  glbconN  33681  hlrelat5N  33705  cvrval4N  33718  atlt  33741  1cvrco  33776  pmaple  34065  isline2  34078  isline4N  34081  elpaddn0  34104  elpadd2at2  34111  cdlemkid4  35240  dia0  35359  cdlemm10N  35425  dibglbN  35473  dihmeetlem4preN  35613  dochkrshp3  35695  dvh4dimlem  35750  lcfl5  35803  mapdpglem3  35982  mapdheq  36035  hdmap1eq  36109  hdmapval2lem  36141  hdmapoc  36241  hlhillcs  36268  fz1eqin  36350  diophin  36354  jm2.19  36578  rmxdiophlem  36600  pw2f1ocnv  36622  wepwsolem  36630  gicabl  36687  sdrgacs  36790  idomodle  36793  isdomn3  36801  ntrclsfveq2  37379  ntrclsss  37381  ntrclsk4  37390  extoimad  37486  radcnvrat  37535  bcc0  37561  unima  38340  clim2f  38703  clim2f2  38737  2reu4a  39838  dfdfat2  39860  funbrafv2b  39888  dfafn5a  39889  iccpartgtprec  39958  flsqrt  40046  dfeven2  40100  dfodd3  40101  pfxsuffeqwrdeq  40269  leaddsuble  40343  ausgrusgrb  40395  usgredgffibi  40543  nb3grpr2  40611  cplgr2v  40654  umgr2v2enb1  40742  upgrspths1wlk  40944  crctcsh  41027  wspthsnwspthsnon  41122  dfconngr1  41355  eupth2lems  41406  lindslinindimp2lem4  42044  snlindsntor  42054  regt1loggt0  42128  elbigo2  42144  elbigolo1  42149  fldivexpfllog2  42157  nnlog2ge0lt1  42158  blenpw2m1  42171