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  3638  eueq3  3690  sbceqal  3823  eqrrabd  4057  n0moeu  4330  sbcel12  4382  sbceqg  4383  sbcne12  4386  reldisj  4424  raldifeq  4465  r19.3rz  4468  ralf0  4485  eldifpr  4630  reusngf  4646  rexreusng  4651  eldiftp  4659  eqsndOLD  4803  reusv2lem5  5365  prelpw  5414  otthg  5453  2rbropap  5534  rabxp  5694  pwvrel  5696  ssrel3  5757  elrng  5863  iss  6014  idrefALT  6092  xpcan  6157  xpcan2  6158  dfpo2  6277  ordelpss  6368  fcnvres  6744  dffv3  6861  funimass4  6932  unima  6943  fndmdif  7021  fneqeql  7025  funimass3  7033  elrnrexdmb  7069  dff4  7080  fnsnbg  7145  fnsnbOLD  7147  fconst4  7195  elunirn  7232  f12dfv  7255  riota1  7372  riota2df  7374  f1ocnvfv3  7389  eqfnov  7525  elrnmpores  7534  caoftrn  7701  ordsucun  7808  dflim3  7831  dfom2  7852  peano5  7878  opiota  8047  frxp2  8132  xpord2pred  8133  xpord2indlem  8135  suppssr  8183  mpoxopovel  8208  brtpos  8223  rntpos  8227  ordgt0ge1  8468  ondif2  8477  oelim2  8570  omabs  8626  naddrid  8658  iiner  8766  erinxp  8768  qliftfun  8779  mapdm0  8819  ordunifi  9255  elfi2  9383  elfiun  9399  fifo  9401  noinfep  9631  cantnflem1  9660  cantnf  9664  rankonidlem  9799  r1pwALT  9817  pr2nelemOLD  9974  cardalephex  10061  alephinit  10066  dfac5lem4OLD  10099  cflim2  10234  cfsmolem  10241  compssiso  10345  fin1a2lem11  10381  itunisuc  10390  axdclem  10490  brdom6disj  10503  alephreg  10553  fpwwe2lem8  10609  pwfseqlem3  10631  indpi  10878  nqereu  10900  ordpinq  10914  ltanq  10942  ltmnq  10943  suplem2pr  11024  map2psrpr  11081  ssxr  11261  leltne  11281  ltneg  11694  leneg  11697  suprnub  12164  negiso  12179  elnnnn0  12501  nn0sub  12508  fcdmnn0fsupp  12516  zrevaddcl  12594  znnsub  12595  znn0sub  12596  prime  12631  eluz2  12815  indstr  12889  eluz2b1  12892  qrevaddcl  12944  rpneg  12998  xrleltne  13118  dfle2  13120  dflt2  13121  supxrleub  13299  infxrgelb  13309  ixxin  13336  iccid  13364  elicopnf  13419  iccsplit  13459  fzsplit2  13523  fzsn  13540  fzpr  13553  uzsplit  13570  preduz  13624  fvinim0ffz  13759  injresinj  13761  om2uzf1oi  13928  lt2sqi  14164  le2sqi  14165  hashsdom  14356  hashf1lem1  14430  fz1isolem  14436  prprrab  14448  ccatlcan  14693  ccatrcan  14694  s3eq3seq  14915  2swrd2eqwrdeq  14929  trclfvcotr  14985  cnpart  15216  limsuplt  15452  rlimresb  15538  mertenslem2  15858  fprod2dlem  15953  sadadd2lem2  16426  saddisjlem  16440  bitsuz  16450  gcddiv  16527  algcvgblem  16553  isprm3  16659  isprm5  16683  prmreclem5  16897  vdwapun  16951  vdwmc2  16956  ramcl  17006  pwsle  17461  ismre  17557  mreacs  17625  acsfn  17626  iscatd2  17648  cidpropd  17677  dfiso2  17740  oppcsect2  17747  isfunc  17832  setcinv  18058  lubeldm  18318  lubval  18321  glbeldm  18331  glbval  18334  tosso  18384  ipodrsfi  18504  acsfiindd  18518  submgmacs  18650  imasmnd2  18707  ismhm0  18723  resmndismnd  18741  submacs  18760  imasgrp2  18993  issubg  19064  resgrpisgrp  19085  subgacs  19099  eqgval  19115  ghmqusnsglem1  19218  ghmquskerlem1  19221  gaorber  19246  symgfix2  19352  psgnran  19451  isslw  19544  sylow2alem2  19554  sylow2a  19555  sylow3lem6  19568  efgcpbllemb  19691  prmcyg  19830  gsum2d2lem  19909  gsumcom2  19911  subgdmdprd  19972  dprd2d2  19982  pgpfac1lem2  20013  pgpfac1lem4  20016  imasrng  20092  imasring  20245  isrnghmmul  20357  isnzr2  20433  isdomn3  20630  drngmulne0  20677  subrgacs  20715  sdrgacs  20716  lssle0  20862  lssacs  20879  lssats2  20912  lvecvsn0  21025  islpir  21244  zndvds  21465  znleval  21470  znleval2  21471  lindsmm  21743  islinds3  21749  islindf4  21753  ismhp3  22035  psdmul  22059  eltg2b  22852  discld  22982  opnssneib  23008  cldlp  23043  restbas  23051  leordtvallem1  23103  leordtvallem2  23104  ssidcn  23148  cnprest2  23183  lmss  23191  perfcls  23258  cmpfi  23301  1stccnp  23355  subislly  23374  hausmapdom  23393  locfindis  23423  iskgen3  23442  kgencn  23449  ptpjpre1  23464  xkoccn  23512  txrest  23524  txlm  23541  txkgen  23545  xkopt  23548  xkoinjcn  23580  imasnopn  23583  imasncld  23584  imasncls  23585  qtopcn  23607  kqfeq  23617  isr0  23630  fbfinnfr  23734  trfbas  23737  fbunfip  23762  ufileu  23812  cfinufil  23821  fmid  23853  txflf  23899  fclsrest  23917  alexsubALT  23944  tsmsres  24037  ucnima  24174  fmucndlem  24184  bldisj  24292  xmeter  24327  elbl4  24457  restmetu  24464  dscopn  24467  bl2ioo  24686  isphtpc  24899  tcphcph  25144  lmmbr2  25166  lmmbrf  25169  iscau2  25184  iscauf  25187  caucfil  25190  metcld  25213  metcld2  25214  bcthlem1  25231  bcthlem4  25234  cldcss2  25349  ovolgelb  25388  ovoliunlem1  25410  ismbfcn  25537  mbfmax  25557  mbfimaopnlem  25563  i1faddlem  25601  i1fmullem  25602  i1fres  25613  i1fpos  25614  itg1climres  25622  xrge0f  25639  itgresr  25687  iblcnlem1  25696  limcun  25803  dvres  25819  mdegmullem  25990  r1pid2  26074  ply1remlem  26077  plyremlem  26219  vieta1  26227  ulmcau  26311  sineq0  26440  coseq1  26441  ang180lem3  26728  cubic  26766  atandm  26793  atandm2  26794  atandm3  26795  rlimcnp  26882  rlimcnp2  26883  vmappw  27033  dchrelbas3  27156  dchrelbas4  27161  dchrsum2  27186  bposlem6  27207  2sqreuopltb  27383  2sqreuopnnltb  27385  dchrisumlem3  27409  pntleml  27529  noetasuplem4  27655  noetainflem4  27659  addsrid  27878  mulsrid  28023  mulsne0bd  28096  onsiso  28176  om2noseqf1o  28202  zn0subs  28298  istrkg3ld  28395  tgcgr4  28465  lnrot2  28558  islnopp  28673  islmib  28721  brbtwn2  28839  axsegconlem6  28856  axsegcon  28861  ax5seg  28872  axpasch  28875  axeuclid  28897  axcontlem4  28901  elntg2  28919  issubgr  29205  nb3gr2nb  29318  uhgrvd00  29469  isrusgr0  29501  wlkcpr  29564  wlkcomp  29566  upgr2wlk  29603  upgrf1istrl  29638  clwlkcomp  29716  clwlkcompbp  29719  iswwlksnx  29777  wspthsnwspthsnon  29853  wspniunwspnon  29860  2pthon3v  29880  usgr2wspthons3  29901  usgr2wspthon  29902  rusgrnumwwlks  29911  clwlkclwwlklem3  29937  clwlkclwwlk  29938  clwwlknonwwlknonb  30042  0pth  30061  eupth2lem2  30155  vdgn1frgrv2  30232  fusgreg2wsp  30272  clwwlknonclwlknonf1o  30298  dlwwlknondlwlknonf1o  30301  wlkl0  30303  nmoolb  30707  nmlno0lem  30729  ubthlem1  30806  ocsh  31219  shle0  31378  eigrei  31770  adjeu  31825  nmoplb  31843  nmfnlb  31860  eleigvec2  31894  nmlnop0iALT  31931  cnlnadjlem5  32007  adjbdln  32019  jplem2  32205  cvbr2  32219  mdsl2bi  32259  chrelat3  32307  eqelbid  32411  sq2reunnltb  32421  rmounid  32431  nelpr  32467  disjunsn  32530  ofpreima  32597  funcnvmpt  32599  funcnv5mpt  32600  dfcnv2  32608  suppiniseg  32617  gtiso  32632  fpwrelmap  32664  infxrge0glb  32696  xrdifh  32711  fzsplit3  32724  fzo0opth  32736  swrdrn3  32885  toslublem  32906  tosglblem  32908  mgcval  32921  mndlrinvb  32974  xrge0tsmsbi  33011  cntzun  33016  isarchi  33144  dvdsrspss  33366  rspsnasso  33367  lsmsnorb  33370  nsgqusf1olem2  33393  isprmidl  33417  ressply1mon1p  33545  r1pid2OLD  33582  constrfin  33744  smatrcl  33794  ist0cld  33831  rspectopn  33865  zarcls  33872  rhmpreimacnlem  33882  unitdivcld  33899  lmxrge0  33950  isrrext  33998  issibf  34332  eulerpartlemr  34373  eulerpartlemmf  34374  eulerpartlemn  34380  dstfrvunirn  34474  ballotlemfc0  34492  ballotlemfcc  34493  reprsuc  34614  reprpmtf1o  34625  reprdifc  34626  bnj919  34765  bnj976  34775  bnj1542  34855  bnj150  34874  bnj151  34875  bnj607  34914  bnj852  34919  bnj873  34922  bnj938  34935  bnj1171  34998  bnj1388  35031  bnj1489  35054  nummin  35089  usgrgt2cycl  35119  subfacp1lem3  35171  subfacp1lem5  35173  erdszelem9  35188  kur14  35205  iscvm  35248  satf0op  35366  mclsax  35558  rexxfr3dALT  35628  elintfv  35749  fundmpss  35751  opelco3  35759  dfon2  35777  dfbigcup2  35884  sscoid  35898  funpartfv  35930  dfrdg4  35936  cgr3permute3  36032  segletr  36099  segleantisym  36100  seglelin  36101  fneval  36337  neibastop3  36347  eltail  36359  filnetlem4  36366  bj-hbntbi  36689  bj-equsvt  36764  bj-sbceqgALT  36887  bj-clel3gALT  37033  bj-rest10  37073  bj-0int  37086  topdifinffinlem  37332  isbasisrelowllem1  37340  isbasisrelowllem2  37341  rdgeqoa  37355  finxpreclem4  37379  finxpsuclem  37382  wl-ifp4impr  37452  wl-1xor  37467  uncf  37590  phpreu  37595  cos2h  37602  tan2h  37603  matunitlindflem1  37607  poimirlem16  37627  poimirlem19  37630  poimirlem23  37634  poimirlem24  37635  poimirlem26  37637  poimirlem27  37638  mbfposadd  37658  cnambfre  37659  itg2addnclem  37662  itg2addnc  37665  iblabsnclem  37674  ftc1anclem1  37684  ftc1anclem5  37688  caures  37751  heiborlem3  37804  heiborlem10  37811  elghomOLD  37878  divrngidl  38019  eqrelf  38240  brvbrvvdif  38249  elrnres  38256  eldmqsres2  38273  exanres  38280  relcnveq  38307  iss2  38329  ecinn0  38338  brxrn2  38360  ecxrn  38372  disjressuc2  38373  eldmcoss2  38444  eldm1cossres  38445  elrelsrel  38472  elrelscnveq  38477  elcoeleqvrelsrel  38581  brredundsredund  38612  brdmqssqs  38632  cnvepresdmqss  38637  eldmqs1cossres  38644  brerser  38662  erimeq2  38663  eleldisjseldisj  38714  prtlem10  38850  prtlem16  38854  prtlem19  38863  prtex  38865  prter3  38867  islshpat  39002  lcvbr2  39007  lcvbr3  39008  lshpsmreu  39094  isat3  39292  hlrelat5N  39387  islpln5  39521  cdlemblem  39779  paddvaln0N  39787  paddval0  39796  cdlemefrs29bpre1  40383  cdlemefrs29cpre1  40384  cdlemg27b  40682  cdlemg33c  40694  cdlemg33e  40696  diaglbN  41041  cdlemm10N  41104  dicopelval2  41167  dicelval2N  41168  dihopelvalcpre  41234  dihglbcpreN  41286  dih1dimatlem  41315  dihatexv  41324  dvh4dimlem  41429  mapdpglem3  41661  hdmap14lem13  41866  hdmapglem7a  41913  eluzp1  42287  fsuppind  42550  isnacs2  42666  rabrenfdioph  42774  expdiophlem1  42982  pw2f1ocnv  42998  pwfi2f1o  43057  numinfctb  43064  dfacbasgrp  43069  islnr3  43076  onsupneqmaxlim0  43185  onsupnmax  43189  onsupuni  43190  tfsconcatrnss  43311  safesnsupfilb  43379  dfhe3  43736  clsk3nimkb  44001  ntrneiiso  44052  ntrneikb  44055  scottabf  44201  mnuunid  44238  hashnzfzclim  44283  dvconstbi  44295  sbcoreleleqVD  44820  trfr  44924  permac8prim  44976  rfcnpre3  44999  rfcnpre4  45000  r19.3rzf  45124  cncfshift  45845  stoweidlem59  46030  dfafv23  47224  nelbrnel  47247  elsetpreimafvrab  47350  iccpartiun  47390  prproropf1olem0  47458  prprelb  47472  prprspr2  47474  reuprpr  47479  oddm1evenALTV  47631  oddp1evenALTV  47632  oddprmne2  47671  fpprel  47684  dfvopnbgr2  47808  uhgrimisgrgric  47886  isgrlim  47936  gpg5nbgrvtx03starlem1  48012  gpg5nbgrvtx03starlem3  48014  gpg5nbgrvtx13starlem1  48015  gpg5nbgrvtx13starlem3  48017  iscmgmALT  48141  iscsgrpALT  48143  mofeu  48768  iscnrm3  48868  joindm2  48884  meetdm2  48886  oppcendc  48935  0funcg  49002  0funcALT  49005  istermc  49352  functermc2  49387  fulltermc  49389  elpglem2  49578