Theorem bitr4di 289

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)

Hypotheses

Ref	Expression
bitr4di.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr4di.2	⊢ (𝜃 ↔ 𝜒)

Assertion

Ref	Expression
bitr4di	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4di

Step	Hyp	Ref	Expression
1		bitr4di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr4di.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	bicomi 224	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	bitrdi 287	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:  3bitr4g  314  bibi2i  337  mtt  364  nbn2  370  ifptru  1074  3bior1fd  1477  3biant1d  1480  clel4g  3617  eueq3  3669  sbceqal  3802  eqrrabd  4038  n0moeu  4311  sbcel12  4363  sbceqg  4364  sbcne12  4367  reldisj  4405  raldifeq  4446  r19.3rz  4454  eldifpr  4615  reusngf  4631  rexreusng  4636  eldiftp  4644  eqsndOLD  4787  reusv2lem5  5347  prelpw  5394  otthg  5433  2rbropap  5512  rabxp  5672  pwvrel  5674  ssrel3  5735  elrng  5840  iss  5994  idrefALT  6070  xpcan  6134  xpcan2  6135  dfpo2  6254  ordelpss  6345  fcnvres  6711  dffv3  6830  funimass4  6898  unima  6909  fndmdif  6987  fneqeql  6991  funimass3  6999  elrnrexdmb  7035  dff4  7046  fnsnbg  7110  fnsnbOLD  7112  fconst4  7160  elunirn  7197  f12dfv  7219  riota1  7336  riota2df  7338  f1ocnvfv3  7353  eqfnov  7487  elrnmpores  7496  caoftrn  7663  ordsucun  7767  dflim3  7789  dfom2  7810  peano5  7835  opiota  8003  frxp2  8086  xpord2pred  8087  xpord2indlem  8089  suppssr  8137  mpoxopovel  8162  brtpos  8177  rntpos  8181  ordgt0ge1  8420  ondif2  8429  oelim2  8523  omabs  8579  naddrid  8611  iiner  8726  erinxp  8728  qliftfun  8739  mapdm0  8779  ordunifi  9190  elfi2  9317  elfiun  9333  fifo  9335  noinfep  9569  cantnflem1  9598  cantnf  9602  rankonidlem  9740  r1pwALT  9758  cardalephex  10000  alephinit  10005  dfac5lem4OLD  10038  cflim2  10173  cfsmolem  10180  compssiso  10284  fin1a2lem11  10320  itunisuc  10329  axdclem  10429  brdom6disj  10442  alephreg  10493  fpwwe2lem8  10549  pwfseqlem3  10571  indpi  10818  nqereu  10840  ordpinq  10854  ltanq  10882  ltmnq  10883  suplem2pr  10964  map2psrpr  11021  ssxr  11202  leltne  11222  ltneg  11637  leneg  11640  suprnub  12107  negiso  12122  elnnnn0  12444  nn0sub  12451  fcdmnn0fsupp  12459  zrevaddcl  12536  znnsub  12537  znn0sub  12538  prime  12573  eluz2  12757  indstr  12829  eluz2b1  12832  qrevaddcl  12884  rpneg  12939  xrleltne  13059  dfle2  13061  dflt2  13062  supxrleub  13241  infxrgelb  13251  ixxin  13278  iccid  13306  elicopnf  13361  iccsplit  13401  fzsplit2  13465  fzsn  13482  fzpr  13495  uzsplit  13512  preduz  13566  fvinim0ffz  13705  injresinj  13707  om2uzf1oi  13876  lt2sqi  14112  le2sqi  14113  hashsdom  14304  hashf1lem1  14378  fz1isolem  14384  prprrab  14396  ccatlcan  14641  ccatrcan  14642  s3eq3seq  14862  2swrd2eqwrdeq  14876  trclfvcotr  14932  cnpart  15163  limsuplt  15402  rlimresb  15488  mertenslem2  15808  fprod2dlem  15903  sadadd2lem2  16377  saddisjlem  16391  bitsuz  16401  gcddiv  16478  algcvgblem  16504  isprm3  16610  isprm5  16634  prmreclem5  16848  vdwapun  16902  vdwmc2  16907  ramcl  16957  pwsle  17413  ismre  17509  mreacs  17581  acsfn  17582  iscatd2  17604  cidpropd  17633  dfiso2  17696  oppcsect2  17703  isfunc  17788  setcinv  18014  lubeldm  18274  lubval  18277  glbeldm  18287  glbval  18290  tosso  18340  ipodrsfi  18462  acsfiindd  18476  submgmacs  18642  imasmnd2  18699  ismhm0  18715  resmndismnd  18733  submacs  18752  imasgrp2  18985  issubg  19056  resgrpisgrp  19077  subgacs  19090  eqgval  19106  ghmqusnsglem1  19209  ghmquskerlem1  19212  gaorber  19237  symgfix2  19345  psgnran  19444  isslw  19537  sylow2alem2  19547  sylow2a  19548  sylow3lem6  19561  efgcpbllemb  19684  prmcyg  19823  gsum2d2lem  19902  gsumcom2  19904  subgdmdprd  19965  dprd2d2  19975  pgpfac1lem2  20006  pgpfac1lem4  20009  imasrng  20112  imasring  20266  isrnghmmul  20378  isnzr2  20451  isdomn3  20648  drngmulne0  20695  subrgacs  20733  sdrgacs  20734  lssle0  20901  lssacs  20918  lssats2  20951  lvecvsn0  21064  islpir  21283  zndvds  21504  znleval  21509  znleval2  21510  lindsmm  21783  islinds3  21789  islindf4  21793  ismhp3  22085  psdmul  22109  eltg2b  22903  discld  23033  opnssneib  23059  cldlp  23094  restbas  23102  leordtvallem1  23154  leordtvallem2  23155  ssidcn  23199  cnprest2  23234  lmss  23242  perfcls  23309  cmpfi  23352  1stccnp  23406  subislly  23425  hausmapdom  23444  locfindis  23474  iskgen3  23493  kgencn  23500  ptpjpre1  23515  xkoccn  23563  txrest  23575  txlm  23592  txkgen  23596  xkopt  23599  xkoinjcn  23631  imasnopn  23634  imasncld  23635  imasncls  23636  qtopcn  23658  kqfeq  23668  isr0  23681  fbfinnfr  23785  trfbas  23788  fbunfip  23813  ufileu  23863  cfinufil  23872  fmid  23904  txflf  23950  fclsrest  23968  alexsubALT  23995  tsmsres  24088  ucnima  24224  fmucndlem  24234  bldisj  24342  xmeter  24377  elbl4  24507  restmetu  24514  dscopn  24517  bl2ioo  24736  isphtpc  24949  tcphcph  25193  lmmbr2  25215  lmmbrf  25218  iscau2  25233  iscauf  25236  caucfil  25239  metcld  25262  metcld2  25263  bcthlem1  25280  bcthlem4  25283  cldcss2  25398  ovolgelb  25437  ovoliunlem1  25459  ismbfcn  25586  mbfmax  25606  mbfimaopnlem  25612  i1faddlem  25650  i1fmullem  25651  i1fres  25662  i1fpos  25663  itg1climres  25671  xrge0f  25688  itgresr  25736  iblcnlem1  25745  limcun  25852  dvres  25868  mdegmullem  26039  r1pid2  26123  ply1remlem  26126  plyremlem  26268  vieta1  26276  ulmcau  26360  sineq0  26489  coseq1  26490  ang180lem3  26777  cubic  26815  atandm  26842  atandm2  26843  atandm3  26844  rlimcnp  26931  rlimcnp2  26932  vmappw  27082  dchrelbas3  27205  dchrelbas4  27210  dchrsum2  27235  bposlem6  27256  2sqreuopltb  27432  2sqreuopnnltb  27434  dchrisumlem3  27458  pntleml  27578  noetasuplem4  27704  noetainflem4  27708  rightge0  27817  addsrid  27960  negleft  28054  negright  28055  mulsrid  28109  mulsne0bd  28182  oniso  28267  om2noseqf1o  28297  zn0subs  28399  avglts1d  28449  avglts2d  28450  istrkg3ld  28533  tgcgr4  28603  lnrot2  28696  islnopp  28811  islmib  28859  mptelee  28967  brbtwn2  28978  axsegconlem6  28995  axsegcon  29000  ax5seg  29011  axpasch  29014  axeuclid  29036  axcontlem4  29040  elntg2  29058  issubgr  29344  nb3gr2nb  29457  uhgrvd00  29608  isrusgr0  29640  wlkcpr  29702  wlkcomp  29704  upgr2wlk  29740  upgrf1istrl  29775  clwlkcomp  29852  clwlkcompbp  29855  iswwlksnx  29913  wspthsnwspthsnon  29989  wspniunwspnon  29996  2pthon3v  30016  usgr2wspthons3  30040  usgr2wspthon  30041  rusgrnumwwlks  30050  clwlkclwwlklem3  30076  clwlkclwwlk  30077  clwwlknonwwlknonb  30181  0pth  30200  eupth2lem2  30294  vdgn1frgrv2  30371  fusgreg2wsp  30411  clwwlknonclwlknonf1o  30437  dlwwlknondlwlknonf1o  30440  wlkl0  30442  nmoolb  30846  nmlno0lem  30868  ubthlem1  30945  ocsh  31358  shle0  31517  eigrei  31909  adjeu  31964  nmoplb  31982  nmfnlb  31999  eleigvec2  32033  nmlnop0iALT  32070  cnlnadjlem5  32146  adjbdln  32158  jplem2  32344  cvbr2  32358  mdsl2bi  32398  chrelat3  32446  eqelbid  32549  sq2reunnltb  32559  rmounid  32569  nelpr  32606  disjunsn  32669  ofpreima  32743  funcnvmpt  32745  funcnv5mpt  32746  dfcnv2  32754  suppiniseg  32765  gtiso  32780  fpwrelmap  32812  infxrge0glb  32845  xrdifh  32860  fzsplit3  32873  fzo0opth  32883  swrdrn3  33037  toslublem  33054  tosglblem  33056  mgcval  33069  mndlrinvb  33107  xrge0tsmsbi  33156  cntzun  33161  isarchi  33264  dvdsrspss  33468  rspsnasso  33469  lsmsnorb  33472  nsgqusf1olem2  33495  isprmidl  33519  ressply1mon1p  33649  r1pid2OLD  33690  constrfin  33903  smatrcl  33953  ist0cld  33990  rspectopn  34024  zarcls  34031  rhmpreimacnlem  34041  unitdivcld  34058  lmxrge0  34109  isrrext  34157  issibf  34490  eulerpartlemr  34531  eulerpartlemmf  34532  eulerpartlemn  34538  dstfrvunirn  34632  ballotlemfc0  34650  ballotlemfcc  34651  reprsuc  34772  reprpmtf1o  34783  reprdifc  34784  bnj919  34923  bnj976  34933  bnj1542  35013  bnj150  35032  bnj151  35033  bnj607  35072  bnj852  35077  bnj873  35080  bnj938  35093  bnj1171  35156  bnj1388  35189  bnj1489  35212  nummin  35249  usgrgt2cycl  35324  subfacp1lem3  35376  subfacp1lem5  35378  erdszelem9  35393  kur14  35410  iscvm  35453  satf0op  35571  mclsax  35763  rexxfr3dALT  35833  elintfv  35959  fundmpss  35961  opelco3  35969  dfon2  35984  dfbigcup2  36091  sscoid  36105  funpartfv  36139  dfrdg4  36145  cgr3permute3  36241  segletr  36308  segleantisym  36309  seglelin  36310  fneval  36546  neibastop3  36556  eltail  36568  filnetlem4  36575  bj-hbntbi  36905  bj-equsvt  36980  bj-sbceqgALT  37103  bj-clel3gALT  37249  bj-rest10  37289  bj-0int  37302  topdifinffinlem  37548  isbasisrelowllem1  37556  isbasisrelowllem2  37557  rdgeqoa  37571  finxpreclem4  37595  finxpsuclem  37598  wl-ifp4impr  37668  wl-1xor  37683  uncf  37796  phpreu  37801  cos2h  37808  tan2h  37809  matunitlindflem1  37813  poimirlem16  37833  poimirlem19  37836  poimirlem23  37840  poimirlem24  37841  poimirlem26  37843  poimirlem27  37844  mbfposadd  37864  cnambfre  37865  itg2addnclem  37868  itg2addnc  37871  iblabsnclem  37880  ftc1anclem1  37890  ftc1anclem5  37894  caures  37957  heiborlem3  38010  heiborlem10  38017  elghomOLD  38084  divrngidl  38225  eqrelf  38449  brvbrvvdif  38458  elrnres  38467  eldmres3  38472  eldmqsres2  38483  exanres  38490  relcnveq  38517  iss2  38533  ecinn0  38542  brxrn2  38565  ecxrn  38587  ecxrn2  38589  disjressuc2  38592  elrelsrel  38623  eldmcoss2  38718  eldm1cossres  38719  elrelscnveq  38797  elcoeleqvrelsrel  38849  brredundsredund  38880  brdmqssqs  38901  cnvepresdmqss  38907  eldmqs1cossres  38914  brerser  38932  erimeq2  38933  eleldisjseldisj  38984  prtlem10  39121  prtlem16  39125  prtlem19  39134  prtex  39136  prter3  39138  islshpat  39273  lcvbr2  39278  lcvbr3  39279  lshpsmreu  39365  isat3  39563  hlrelat5N  39657  islpln5  39791  cdlemblem  40049  paddvaln0N  40057  paddval0  40066  cdlemefrs29bpre1  40653  cdlemefrs29cpre1  40654  cdlemg27b  40952  cdlemg33c  40964  cdlemg33e  40966  diaglbN  41311  cdlemm10N  41374  dicopelval2  41437  dicelval2N  41438  dihopelvalcpre  41504  dihglbcpreN  41556  dih1dimatlem  41585  dihatexv  41594  dvh4dimlem  41699  mapdpglem3  41931  hdmap14lem13  42136  hdmapglem7a  42183  eluzp1  42558  fsuppind  42829  isnacs2  42944  rabrenfdioph  43052  expdiophlem1  43259  pw2f1ocnv  43275  pwfi2f1o  43334  numinfctb  43341  dfacbasgrp  43346  islnr3  43353  onsupneqmaxlim0  43462  onsupnmax  43466  onsupuni  43467  tfsconcatrnss  43588  safesnsupfilb  43655  dfhe3  44012  clsk3nimkb  44277  ntrneiiso  44328  ntrneikb  44331  scottabf  44477  mnuunid  44514  hashnzfzclim  44559  dvconstbi  44571  sbcoreleleqVD  45095  trfr  45199  permac8prim  45251  rfcnpre3  45274  rfcnpre4  45275  r19.3rzf  45398  cncfshift  46114  stoweidlem59  46299  chnsubseqwl  47119  dfafv23  47495  nelbrnel  47518  elsetpreimafvrab  47636  iccpartiun  47676  prproropf1olem0  47744  prprelb  47758  prprspr2  47760  reuprpr  47765  oddm1evenALTV  47917  oddp1evenALTV  47918  oddprmne2  47957  fpprel  47970  dfvopnbgr2  48095  uhgrimisgrgric  48173  isgrlim  48224  gpg5nbgrvtx03starlem1  48310  gpg5nbgrvtx03starlem3  48312  gpg5nbgrvtx13starlem1  48313  gpg5nbgrvtx13starlem3  48315  iscmgmALT  48466  iscsgrpALT  48468  mofeu  49089  iscnrm3  49193  joindm2  49209  meetdm2  49211  oppcendc  49259  0funcg  49326  0funcALT  49329  istermc  49715  functermc2  49750  fulltermc  49752  elpglem2  49953