Theorem bitr4di 292

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 227	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	bitrdi 290	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr4g  317  bibi2i  340  mtt  367  nbn2  373  ifptru  1091  3bior1fd  1506  3biant1d  1509  clel4g  3616  eueq3  3668  sbceqal  3799  eqrrabd  4011  n0moeu  4306  sbcel12  4368  sbceqg  4369  sbcne12  4372  reldisj  4405  raldifeq  4448  r19.3rz  4456  eldifpr  4618  reusngf  4634  rexreusng  4639  eldiftp  4647  reusv2lem5  5363  prelpw  5413  otthg  5453  2rbropap  5538  rabxp  5698  pwvrel  5700  ssrel3  5761  elrng  5872  iss  6026  idrefALT  6106  xpcan  6167  xpcan2  6168  dfpo2  6299  ordelpss  6390  fcnvres  6759  dffv3  6881  funimass4  6949  unima  6960  funcnvmpt  6995  fndmdif  7041  fneqeql  7045  funimass3  7053  elrnrexdmb  7090  dff4  7101  fnsnbg  7169  fnsnbOLD  7171  fconst4  7220  elunirn  7255  f12dfv  7281  riota1  7398  riota2df  7400  f1ocnvfv3  7415  eqfnov  7549  elrnmpores  7558  caoftrn  7734  ordsucun  7836  dflim3  7858  dfom2  7879  peano5  7905  opiota  8070  frxp2  8161  xpord2pred  8162  xpord2indlem  8164  suppssr  8212  mpoxopovel  8237  brtpos  8252  rntpos  8256  ordgt0ge1  8501  ondif2  8510  oelim2  8604  omabs  8660  naddrid  8693  iiner  8810  erinxp  8812  qliftfun  8823  mapdm0  8862  uncf  8891  ordunifi  9281  elfi2  9406  elfiun  9422  fifo  9424  noinfep  9661  cantnflem1  9690  cantnf  9694  rankonidlem  9838  r1pwALT  9860  scottabf  9939  cardalephex  10169  alephinit  10174  cflim2  10341  cfsmolem  10348  compssiso  10452  fin1a2lem11  10488  itunisuc  10497  axdclem  10597  brdom6disj  10611  alephreg  10667  fpwwe2lem8  10723  pwfseqlem3  10745  indpi  10992  nqereu  11014  ordpinq  11028  ltanq  11056  ltmnq  11057  suplem2pr  11138  map2psrpr  11195  ssxr  11379  leltne  11399  ltneg  11816  leneg  11819  suprnub  12282  negiso  12297  elnnnn0  12649  nn0sub  12656  fcdmnn0fsupp  12664  zrevaddcl  12741  znnsub  12742  znn0sub  12743  prime  12780  eluz2  12971  indstr  13043  eluz2b1  13046  qrevaddcl  13099  rpneg  13154  xrleltne  13274  dfle2  13276  dflt2  13277  supxrleub  13456  infxrgelb  13466  ixxin  13493  iccid  13521  elicopnf  13576  iccsplit  13616  fzsplit2  13683  fzsn  13700  fzpr  13713  uzsplit  13730  preduz  13784  fvinim0ffz  13924  injresinj  13926  om2uzf1oi  14096  lt2sqi  14332  le2sqi  14333  hashsdom  14525  hashf1lem1  14600  fz1isolem  14606  prprrab  14618  swrdrn3  14802  ccatlcan  14867  ccatrcan  14868  s3eq3seq  15090  2swrd2eqwrdeq  15106  trclfvcotr  15162  cnpart  15407  limsuplt  15646  rlimresb  15732  mertenslem2  16054  fprod2dlem  16147  sadadd2lem2  16620  saddisjlem  16634  bitsuz  16644  gcddiv  16724  algcvgblem  16752  isprm3  16858  isprm5  16883  prmreclem5  17098  vdwapun  17152  vdwmc2  17157  ramcl  17207  pwsle  17664  ismre  17760  mreacs  17832  acsfn  17833  iscatd2  17855  cidpropd  17884  dfiso2  17947  oppcsect2  17954  isfunc  18039  setcinv  18265  lubeldm  18525  lubval  18528  glbeldm  18538  glbval  18541  tosso  18591  ipodrsfi  18713  acsfiindd  18727  submgmacs  18906  imasmnd2  18968  ismhm0  18985  resmndismnd  19003  submacs  19023  imasgrp2  19265  issubg  19336  resgrpisgrp  19358  subgacs  19371  eqgval  19389  ghmqusnsglem1  19494  ghmquskerlem1  19497  gaorber  19522  symgfix2  19630  psgnran  19729  isslw  19822  sylow2alem2  19832  sylow2a  19833  sylow3lem6  19846  efgcpbllemb  19969  prmcyg  20108  gsum2d2lem  20187  gsumcom2  20189  subgdmdprd  20250  dprd2d2  20260  pgpfac1lem2  20291  pgpfac1lem4  20294  imasrng  20399  imasring  20560  isrnghmmul  20672  isnzr2  20768  isdomn3  20966  drngmulne0  21019  subrgacs  21057  sdrgacs  21058  lssle0  21225  lssacs  21242  lssats2  21275  lvecvsn0  21387  rspsn0  21526  isprmidl  21619  islpir  21652  zndvds  21855  znleval  21860  znleval2  21861  lindsmm  22134  islinds3  22140  islindf4  22144  ismhp3  22463  psdmul  22487  matunitlindflem1  22994  eltg2b  23277  discld  23407  opnssneib  23433  cldlp  23468  restbas  23476  leordtvallem1  23528  leordtvallem2  23529  ssidcn  23573  cnprest2  23608  lmss  23616  perfcls  23683  cmpfi  23726  1stccnp  23781  subislly  23800  hausmapdom  23819  locfindis  23849  iskgen3  23868  kgencn  23875  ptpjpre1  23890  xkoccn  23938  txrest  23950  txlm  23967  txkgen  23971  xkopt  23974  xkoinjcn  24006  imasnopn  24009  imasncld  24010  imasncls  24011  qtopcn  24033  kqfeq  24043  isr0  24056  fbfinnfr  24160  trfbas  24163  fbunfip  24188  ufileu  24238  cfinufil  24247  fmid  24279  txflf  24325  fclsrest  24343  alexsubALT  24370  tsmsres  24463  ucnima  24599  fmucndlem  24609  bldisj  24717  xmeter  24752  elbl4  24882  restmetu  24889  dscopn  24892  bl2ioo  25111  isphtpc  25315  tcphcph  25558  lmmbr2  25580  lmmbrf  25583  iscau2  25598  iscauf  25601  caucfil  25604  metcld  25627  metcld2  25628  bcthlem1  25645  bcthlem4  25648  cldcss2  25763  ovolgelb  25801  ovoliunlem1  25823  ismbfcn  25950  mbfmax  25970  mbfimaopnlem  25976  i1faddlem  26014  i1fmullem  26015  i1fres  26026  i1fpos  26027  itg1climres  26035  xrge0f  26052  itgresr  26099  iblcnlem1  26108  limcun  26215  dvres  26231  mdegmullem  26396  r1pid2  26480  ply1remlem  26483  plyremlem  26625  vieta1  26635  ulmcau  26722  sineq0  26852  coseq1  26853  ang180lem3  27139  cubic  27177  atandm  27204  atandm2  27205  atandm3  27206  rlimcnp  27293  rlimcnp2  27294  vmappw  27443  dchrelbas3  27565  dchrelbas4  27570  dchrsum2  27595  bposlem6  27616  2sqreuopltb  27792  2sqreuopnnltb  27794  dchrisumlem3  27818  pntleml  27938  noetasuplem4  28093  noetainflem4  28097  rightge0  28207  addsrid  28350  negleft  28444  negright  28445  mulsrid  28499  mulsne0bd  28572  oniso  28657  om2noseqf1o  28687  zn0subs  28789  avglts1d  28839  avglts2d  28840  istrkg3ld  28923  tgcgr4  28994  lnrot2  29092  islnopp  29215  islmib  29292  mptelee  29472  brbtwn2  29483  axsegconlem6  29500  axsegcon  29505  ax5seg  29516  axpasch  29519  axeuclid  29541  axcontlem4  29545  elntg2  29563  issubgr  29852  nb3gr2nb  29965  uhgrvd00  30115  isrusgr0  30147  wlkcpr  30209  wlkcomp  30211  upgr2wlk  30247  upgrf1istrl  30286  clwlkcomp  30366  clwlkcompbp  30369  iswwlksnx  30429  wspthsnwspthsnon  30505  wspniunwspnon  30512  2pthon3v  30532  usgr2wspthons3  30556  usgr2wspthon  30557  rusgrnumwwlks  30566  clwlkclwwlklem3  30592  clwlkclwwlk  30593  clwwlknonwwlknonb  30697  0pth  30716  eupth2lem2  30820  vdgn1frgrv2  30897  fusgreg2wsp  30937  clwwlknonclwlknonf1o  30963  dlwwlknondlwlknonf1o  30966  wlkl0  30968  nmoolb  31373  nmlno0lem  31395  ubthlem1  31472  ocsh  31885  shle0  32044  eigrei  32436  adjeu  32491  nmoplb  32509  nmfnlb  32526  eleigvec2  32560  nmlnop0iALT  32597  cnlnadjlem5  32673  adjbdln  32685  jplem2  32871  cvbr2  32885  mdsl2bi  32925  chrelat3  32973  eqelbid  33071  sq2reunnltb  33081  rmounid  33091  nelpr  33127  disjunsn  33188  ofpreima  33259  funcnv5mpt  33261  dfcnv2  33269  suppiniseg  33279  gtiso  33294  fpwrelmap  33325  infxrge0glb  33357  xrdifh  33372  fzsplit3  33385  fzo0opth  33395  toslublem  33533  tosglblem  33535  mgcval  33548  mndlrinvb  33586  xrge0tsmsbi  33635  cntzun  33640  isarchi  33743  dvdsrspss  33942  rspsnasso  33943  lsmsnorb  33946  nsgqusf1olem2  33965  ressply1mon1p  34100  constrfin  34378  smatrcl  34428  ist0cld  34465  rspectopn  34499  zarcls  34506  rhmpreimacnlem  34516  unitdivcld  34533  lmxrge0  34584  isrrext  34632  issibf  34965  eulerpartlemr  35006  eulerpartlemmf  35007  eulerpartlemn  35013  dstfrvunirn  35107  ballotlemfc0  35125  ballotlemfcc  35126  reprsuc  35244  reprpmtf1o  35255  reprdifc  35256  bnj919  35398  bnj976  35408  bnj1542  35487  bnj150  35506  bnj151  35507  bnj607  35546  bnj852  35551  bnj873  35554  bnj938  35567  bnj1171  35630  bnj1388  35663  bnj1489  35686  nummin  35722  dfscott3  35743  usgrgt2cycl  35909  subfacp1lem3  35947  subfacp1lem5  35949  erdszelem9  35964  kur14  35981  iscvm  36024  satf0op  36142  mclsax  36334  rexxfr3dALT  36404  elintfv  36530  fundmpss  36532  opelco3  36539  dfon2  36554  dfbigcup2  36661  sscoid  36675  funpartfv  36709  dfrdg4  36715  cgr3permute3  36812  segletr  36879  segleantisym  36880  seglelin  36881  nmulrid  36946  fneval  37140  neibastop3  37150  eltail  37162  filnetlem4  37169  mh-infprim2bi  37335  bj-hbntbi  37606  bj-equsvt  37673  bj-sbceqgALT  37814  bj-clel3gALT  37963  bj-rest10  38009  bj-0int  38022  qdiffALT  38250  topdifinffinlem  38271  isbasisrelowllem1  38279  isbasisrelowllem2  38280  rdgeqoa  38294  finxpreclem4  38318  finxpsuclem  38321  wl-ifp4impr  38391  wl-1xor  38406  phpreu  38528  cos2h  38535  tan2h  38536  poimirlem16  38555  poimirlem19  38558  poimirlem23  38562  poimirlem24  38563  poimirlem26  38565  poimirlem27  38566  mbfposadd  38586  cnambfre  38587  itg2addnclem  38590  itg2addnc  38593  iblabsnclem  38602  ftc1anclem1  38612  ftc1anclem5  38616  findcard4  38633  caures  38695  heiborlem3  38748  heiborlem10  38755  elghomOLD  38822  divrngidl  38963  eqrelf  39191  brvbrvvdif  39202  elrnres  39211  eldmres3  39216  eldmqsres2  39227  exanres  39234  relcnveq  39261  iss2  39277  ecinn0  39286  raldmqsmo  39296  brxrn2  39317  ecxrn  39339  ecxrn2  39341  disjressuc2  39344  elrelsrel  39375  eldmcoss2  39482  eldm1cossres  39483  elrelscnveq  39561  elcoeleqvrelsrel  39613  brredundsredund  39644  brdmqssqs  39664  cnvepresdmqss  39670  eldmqs1cossres  39677  brerser  39695  erimeq2  39696  eleldisjseldisj  39762  prtlem10  39923  prtlem16  39927  prtlem19  39936  prtex  39938  prter3  39940  islshpat  40075  lcvbr2  40080  lcvbr3  40081  lshpsmreu  40167  isat3  40365  hlrelat5N  40459  islpln5  40593  cdlemblem  40851  paddvaln0N  40859  paddval0  40868  cdlemefrs29bpre1  41455  cdlemefrs29cpre1  41456  cdlemg27b  41754  cdlemg33c  41766  cdlemg33e  41768  diaglbN  42113  cdlemm10N  42176  dicopelval2  42239  dicelval2N  42240  dihopelvalcpre  42306  dihglbcpreN  42358  dih1dimatlem  42387  dihatexv  42396  dvh4dimlem  42501  mapdpglem3  42733  hdmap14lem13  42938  hdmapglem7a  42985  eluzp1  43365  fsuppind  43619  isnacs2  43717  rabrenfdioph  43821  expdiophlem1  44028  pw2f1ocnv  44044  pwfi2f1o  44098  numinfctb  44105  dfacbasgrp  44110  islnr3  44117  onsupneqmaxlim0  44226  onsupnmax  44230  onsupuni  44231  tfsconcatrnss  44352  safesnsupfilb  44419  dfhe3  44775  clsk3nimkb  45040  ntrneiiso  45091  ntrneikb  45094  mnuunid  45261  hashnzfzclim  45306  dvconstbi  45318  sbcoreleleqVD  45841  trfr  45952  permac8prim  46004  rfcnpre3  46050  rfcnpre4  46051  r19.3rzf  46173  cncfshift  46884  stoweidlem59  47069  chnsubseqwl  47889  dfafv23  48323  nelbrnel  48346  elsetpreimafvrab  48476  iccpartiun  48516  prproropf1olem0  48584  prprelb  48598  prprspr2  48600  reuprpr  48605  oddm1evenALTV  48773  oddp1evenALTV  48774  oddprmne2  48813  fpprel  48826  dfvopnbgr2  48951  uhgrimisgrgric  49029  isgrlim  49080  gpg5nbgrvtx03starlem1  49166  gpg5nbgrvtx03starlem3  49168  gpg5nbgrvtx13starlem1  49169  gpg5nbgrvtx13starlem3  49171  iscmgmALT  49321  iscsgrpALT  49323  mofeu  49958  iscnrm3  50060  joindm2  50076  meetdm2  50078  oppcendc  50126  0funcg  50193  0funcALT  50196  istermc  50582  functermc2  50617  fulltermc  50619  elpglem2  50805