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  1075  3bior1fd  1478  3biant1d  1481  clel4g  3606  eueq3  3658  sbceqal  3791  eqrrabd  4027  n0moeu  4300  sbcel12  4352  sbceqg  4353  sbcne12  4356  reldisj  4394  raldifeq  4434  r19.3rz  4442  eldifpr  4603  reusngf  4619  rexreusng  4624  eldiftp  4632  eqsndOLD  4775  reusv2lem5  5345  prelpw  5399  otthg  5439  2rbropap  5519  rabxp  5679  pwvrel  5681  ssrel3  5742  elrng  5847  iss  6001  idrefALT  6077  xpcan  6141  xpcan2  6142  dfpo2  6261  ordelpss  6352  fcnvres  6718  dffv3  6837  funimass4  6905  unima  6916  funcnvmpt  6950  fndmdif  6995  fneqeql  6999  funimass3  7007  elrnrexdmb  7043  dff4  7054  fnsnbg  7119  fnsnbOLD  7121  fconst4  7169  elunirn  7206  f12dfv  7228  riota1  7345  riota2df  7347  f1ocnvfv3  7362  eqfnov  7496  elrnmpores  7505  caoftrn  7672  ordsucun  7776  dflim3  7798  dfom2  7819  peano5  7844  opiota  8012  frxp2  8094  xpord2pred  8095  xpord2indlem  8097  suppssr  8145  mpoxopovel  8170  brtpos  8185  rntpos  8189  ordgt0ge1  8428  ondif2  8437  oelim2  8531  omabs  8587  naddrid  8619  iiner  8736  erinxp  8738  qliftfun  8749  mapdm0  8789  ordunifi  9200  elfi2  9327  elfiun  9343  fifo  9345  noinfep  9581  cantnflem1  9610  cantnf  9614  rankonidlem  9752  r1pwALT  9770  cardalephex  10012  alephinit  10017  dfac5lem4OLD  10050  cflim2  10185  cfsmolem  10192  compssiso  10296  fin1a2lem11  10332  itunisuc  10341  axdclem  10441  brdom6disj  10454  alephreg  10505  fpwwe2lem8  10561  pwfseqlem3  10583  indpi  10830  nqereu  10852  ordpinq  10866  ltanq  10894  ltmnq  10895  suplem2pr  10976  map2psrpr  11033  ssxr  11215  leltne  11235  ltneg  11650  leneg  11653  suprnub  12121  negiso  12136  elnnnn0  12480  nn0sub  12487  fcdmnn0fsupp  12495  zrevaddcl  12572  znnsub  12573  znn0sub  12574  prime  12610  eluz2  12794  indstr  12866  eluz2b1  12869  qrevaddcl  12921  rpneg  12976  xrleltne  13096  dfle2  13098  dflt2  13099  supxrleub  13278  infxrgelb  13288  ixxin  13315  iccid  13343  elicopnf  13398  iccsplit  13438  fzsplit2  13503  fzsn  13520  fzpr  13533  uzsplit  13550  preduz  13604  fvinim0ffz  13744  injresinj  13746  om2uzf1oi  13915  lt2sqi  14151  le2sqi  14152  hashsdom  14343  hashf1lem1  14417  fz1isolem  14423  prprrab  14435  ccatlcan  14680  ccatrcan  14681  s3eq3seq  14901  2swrd2eqwrdeq  14915  trclfvcotr  14971  cnpart  15202  limsuplt  15441  rlimresb  15527  mertenslem2  15850  fprod2dlem  15945  sadadd2lem2  16419  saddisjlem  16433  bitsuz  16443  gcddiv  16520  algcvgblem  16546  isprm3  16652  isprm5  16677  prmreclem5  16891  vdwapun  16945  vdwmc2  16950  ramcl  17000  pwsle  17456  ismre  17552  mreacs  17624  acsfn  17625  iscatd2  17647  cidpropd  17676  dfiso2  17739  oppcsect2  17746  isfunc  17831  setcinv  18057  lubeldm  18317  lubval  18320  glbeldm  18330  glbval  18333  tosso  18383  ipodrsfi  18505  acsfiindd  18519  submgmacs  18685  imasmnd2  18742  ismhm0  18758  resmndismnd  18776  submacs  18795  imasgrp2  19031  issubg  19102  resgrpisgrp  19123  subgacs  19136  eqgval  19152  ghmqusnsglem1  19255  ghmquskerlem1  19258  gaorber  19283  symgfix2  19391  psgnran  19490  isslw  19583  sylow2alem2  19593  sylow2a  19594  sylow3lem6  19607  efgcpbllemb  19730  prmcyg  19869  gsum2d2lem  19948  gsumcom2  19950  subgdmdprd  20011  dprd2d2  20021  pgpfac1lem2  20052  pgpfac1lem4  20055  imasrng  20158  imasring  20310  isrnghmmul  20422  isnzr2  20495  isdomn3  20692  drngmulne0  20739  subrgacs  20777  sdrgacs  20778  lssle0  20945  lssacs  20962  lssats2  20995  lvecvsn0  21107  islpir  21326  zndvds  21529  znleval  21534  znleval2  21535  lindsmm  21808  islinds3  21814  islindf4  21818  ismhp3  22108  psdmul  22132  eltg2b  22924  discld  23054  opnssneib  23080  cldlp  23115  restbas  23123  leordtvallem1  23175  leordtvallem2  23176  ssidcn  23220  cnprest2  23255  lmss  23263  perfcls  23330  cmpfi  23373  1stccnp  23427  subislly  23446  hausmapdom  23465  locfindis  23495  iskgen3  23514  kgencn  23521  ptpjpre1  23536  xkoccn  23584  txrest  23596  txlm  23613  txkgen  23617  xkopt  23620  xkoinjcn  23652  imasnopn  23655  imasncld  23656  imasncls  23657  qtopcn  23679  kqfeq  23689  isr0  23702  fbfinnfr  23806  trfbas  23809  fbunfip  23834  ufileu  23884  cfinufil  23893  fmid  23925  txflf  23971  fclsrest  23989  alexsubALT  24016  tsmsres  24109  ucnima  24245  fmucndlem  24255  bldisj  24363  xmeter  24398  elbl4  24528  restmetu  24535  dscopn  24538  bl2ioo  24757  isphtpc  24961  tcphcph  25204  lmmbr2  25226  lmmbrf  25229  iscau2  25244  iscauf  25247  caucfil  25250  metcld  25273  metcld2  25274  bcthlem1  25291  bcthlem4  25294  cldcss2  25409  ovolgelb  25447  ovoliunlem1  25469  ismbfcn  25596  mbfmax  25616  mbfimaopnlem  25622  i1faddlem  25660  i1fmullem  25661  i1fres  25672  i1fpos  25673  itg1climres  25681  xrge0f  25698  itgresr  25746  iblcnlem1  25755  limcun  25862  dvres  25878  mdegmullem  26043  r1pid2  26127  ply1remlem  26130  plyremlem  26270  vieta1  26278  ulmcau  26360  sineq0  26488  coseq1  26489  ang180lem3  26775  cubic  26813  atandm  26840  atandm2  26841  atandm3  26842  rlimcnp  26929  rlimcnp2  26930  vmappw  27079  dchrelbas3  27201  dchrelbas4  27206  dchrsum2  27231  bposlem6  27252  2sqreuopltb  27428  2sqreuopnnltb  27430  dchrisumlem3  27454  pntleml  27574  noetasuplem4  27700  noetainflem4  27704  rightge0  27813  addsrid  27956  negleft  28050  negright  28051  mulsrid  28105  mulsne0bd  28178  oniso  28263  om2noseqf1o  28293  zn0subs  28395  avglts1d  28445  avglts2d  28446  istrkg3ld  28529  tgcgr4  28599  lnrot2  28692  islnopp  28807  islmib  28855  mptelee  28963  brbtwn2  28974  axsegconlem6  28991  axsegcon  28996  ax5seg  29007  axpasch  29010  axeuclid  29032  axcontlem4  29036  elntg2  29054  issubgr  29340  nb3gr2nb  29453  uhgrvd00  29603  isrusgr0  29635  wlkcpr  29697  wlkcomp  29699  upgr2wlk  29735  upgrf1istrl  29770  clwlkcomp  29847  clwlkcompbp  29850  iswwlksnx  29908  wspthsnwspthsnon  29984  wspniunwspnon  29991  2pthon3v  30011  usgr2wspthons3  30035  usgr2wspthon  30036  rusgrnumwwlks  30045  clwlkclwwlklem3  30071  clwlkclwwlk  30072  clwwlknonwwlknonb  30176  0pth  30195  eupth2lem2  30289  vdgn1frgrv2  30366  fusgreg2wsp  30406  clwwlknonclwlknonf1o  30432  dlwwlknondlwlknonf1o  30435  wlkl0  30437  nmoolb  30842  nmlno0lem  30864  ubthlem1  30941  ocsh  31354  shle0  31513  eigrei  31905  adjeu  31960  nmoplb  31978  nmfnlb  31995  eleigvec2  32029  nmlnop0iALT  32066  cnlnadjlem5  32142  adjbdln  32154  jplem2  32340  cvbr2  32354  mdsl2bi  32394  chrelat3  32442  eqelbid  32544  sq2reunnltb  32554  rmounid  32564  nelpr  32601  disjunsn  32664  ofpreima  32738  funcnv5mpt  32740  dfcnv2  32748  suppiniseg  32759  gtiso  32774  fpwrelmap  32806  infxrge0glb  32838  xrdifh  32853  fzsplit3  32866  fzo0opth  32876  swrdrn3  33015  toslublem  33032  tosglblem  33034  mgcval  33047  mndlrinvb  33085  xrge0tsmsbi  33135  cntzun  33140  isarchi  33243  dvdsrspss  33447  rspsnasso  33448  lsmsnorb  33451  nsgqusf1olem2  33474  isprmidl  33498  ressply1mon1p  33628  r1pid2OLD  33669  constrfin  33890  smatrcl  33940  ist0cld  33977  rspectopn  34011  zarcls  34018  rhmpreimacnlem  34028  unitdivcld  34045  lmxrge0  34096  isrrext  34144  issibf  34477  eulerpartlemr  34518  eulerpartlemmf  34519  eulerpartlemn  34525  dstfrvunirn  34619  ballotlemfc0  34637  ballotlemfcc  34638  reprsuc  34759  reprpmtf1o  34770  reprdifc  34771  bnj919  34910  bnj976  34920  bnj1542  34999  bnj150  35018  bnj151  35019  bnj607  35058  bnj852  35063  bnj873  35066  bnj938  35079  bnj1171  35142  bnj1388  35175  bnj1489  35198  nummin  35236  usgrgt2cycl  35312  subfacp1lem3  35364  subfacp1lem5  35366  erdszelem9  35381  kur14  35398  iscvm  35441  satf0op  35559  mclsax  35751  rexxfr3dALT  35821  elintfv  35947  fundmpss  35949  opelco3  35957  dfon2  35972  dfbigcup2  36079  sscoid  36093  funpartfv  36127  dfrdg4  36133  cgr3permute3  36229  segletr  36296  segleantisym  36297  seglelin  36298  fneval  36534  neibastop3  36544  eltail  36556  filnetlem4  36563  mh-infprim2bi  36729  bj-hbntbi  37001  bj-equsvt  37068  bj-sbceqgALT  37209  bj-clel3gALT  37355  bj-rest10  37400  bj-0int  37413  qdiffALT  37642  topdifinffinlem  37663  isbasisrelowllem1  37671  isbasisrelowllem2  37672  rdgeqoa  37686  finxpreclem4  37710  finxpsuclem  37713  wl-ifp4impr  37783  wl-1xor  37798  uncf  37920  phpreu  37925  cos2h  37932  tan2h  37933  matunitlindflem1  37937  poimirlem16  37957  poimirlem19  37960  poimirlem23  37964  poimirlem24  37965  poimirlem26  37967  poimirlem27  37968  mbfposadd  37988  cnambfre  37989  itg2addnclem  37992  itg2addnc  37995  iblabsnclem  38004  ftc1anclem1  38014  ftc1anclem5  38018  caures  38081  heiborlem3  38134  heiborlem10  38141  elghomOLD  38208  divrngidl  38349  eqrelf  38579  brvbrvvdif  38590  elrnres  38599  eldmres3  38604  eldmqsres2  38615  exanres  38622  relcnveq  38649  iss2  38665  ecinn0  38674  raldmqsmo  38684  brxrn2  38705  ecxrn  38727  ecxrn2  38729  disjressuc2  38732  elrelsrel  38763  eldmcoss2  38870  eldm1cossres  38871  elrelscnveq  38949  elcoeleqvrelsrel  39001  brredundsredund  39032  brdmqssqs  39052  cnvepresdmqss  39058  eldmqs1cossres  39065  brerser  39083  erimeq2  39084  eleldisjseldisj  39150  prtlem10  39311  prtlem16  39315  prtlem19  39324  prtex  39326  prter3  39328  islshpat  39463  lcvbr2  39468  lcvbr3  39469  lshpsmreu  39555  isat3  39753  hlrelat5N  39847  islpln5  39981  cdlemblem  40239  paddvaln0N  40247  paddval0  40256  cdlemefrs29bpre1  40843  cdlemefrs29cpre1  40844  cdlemg27b  41142  cdlemg33c  41154  cdlemg33e  41156  diaglbN  41501  cdlemm10N  41564  dicopelval2  41627  dicelval2N  41628  dihopelvalcpre  41694  dihglbcpreN  41746  dih1dimatlem  41775  dihatexv  41784  dvh4dimlem  41889  mapdpglem3  42121  hdmap14lem13  42326  hdmapglem7a  42373  eluzp1  42739  fsuppind  43023  isnacs2  43138  rabrenfdioph  43242  expdiophlem1  43449  pw2f1ocnv  43465  pwfi2f1o  43524  numinfctb  43531  dfacbasgrp  43536  islnr3  43543  onsupneqmaxlim0  43652  onsupnmax  43656  onsupuni  43657  tfsconcatrnss  43778  safesnsupfilb  43845  dfhe3  44202  clsk3nimkb  44467  ntrneiiso  44518  ntrneikb  44521  scottabf  44667  mnuunid  44704  hashnzfzclim  44749  dvconstbi  44761  sbcoreleleqVD  45285  trfr  45389  permac8prim  45441  rfcnpre3  45464  rfcnpre4  45465  r19.3rzf  45588  cncfshift  46302  stoweidlem59  46487  chnsubseqwl  47307  dfafv23  47695  nelbrnel  47718  elsetpreimafvrab  47848  iccpartiun  47888  prproropf1olem0  47956  prprelb  47970  prprspr2  47972  reuprpr  47977  oddm1evenALTV  48145  oddp1evenALTV  48146  oddprmne2  48185  fpprel  48198  dfvopnbgr2  48323  uhgrimisgrgric  48401  isgrlim  48452  gpg5nbgrvtx03starlem1  48538  gpg5nbgrvtx03starlem3  48540  gpg5nbgrvtx13starlem1  48541  gpg5nbgrvtx13starlem3  48543  iscmgmALT  48694  iscsgrpALT  48696  mofeu  49317  iscnrm3  49421  joindm2  49437  meetdm2  49439  oppcendc  49487  0funcg  49554  0funcALT  49557  istermc  49943  functermc2  49978  fulltermc  49980  elpglem2  50181