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  3616  eueq3  3668  sbceqal  3801  eqrrabd  4034  n0moeu  4307  sbcel12  4359  sbceqg  4360  sbcne12  4363  reldisj  4401  raldifeq  4442  r19.3rz  4445  ralf0  4462  eldifpr  4609  reusngf  4625  rexreusng  4630  eldiftp  4638  eqsndOLD  4781  reusv2lem5  5338  prelpw  5385  otthg  5423  2rbropap  5502  rabxp  5662  pwvrel  5664  ssrel3  5724  elrng  5829  iss  5981  idrefALT  6057  xpcan  6120  xpcan2  6121  dfpo2  6239  ordelpss  6330  fcnvres  6696  dffv3  6813  funimass4  6881  unima  6892  fndmdif  6970  fneqeql  6974  funimass3  6982  elrnrexdmb  7018  dff4  7029  fnsnbg  7093  fnsnbOLD  7095  fconst4  7143  elunirn  7180  f12dfv  7202  riota1  7319  riota2df  7321  f1ocnvfv3  7336  eqfnov  7470  elrnmpores  7479  caoftrn  7646  ordsucun  7750  dflim3  7772  dfom2  7793  peano5  7818  opiota  7986  frxp2  8069  xpord2pred  8070  xpord2indlem  8072  suppssr  8120  mpoxopovel  8145  brtpos  8160  rntpos  8164  ordgt0ge1  8403  ondif2  8412  oelim2  8505  omabs  8561  naddrid  8593  iiner  8708  erinxp  8710  qliftfun  8721  mapdm0  8761  ordunifi  9169  elfi2  9293  elfiun  9309  fifo  9311  noinfep  9545  cantnflem1  9574  cantnf  9578  rankonidlem  9713  r1pwALT  9731  cardalephex  9973  alephinit  9978  dfac5lem4OLD  10011  cflim2  10146  cfsmolem  10153  compssiso  10257  fin1a2lem11  10293  itunisuc  10302  axdclem  10402  brdom6disj  10415  alephreg  10465  fpwwe2lem8  10521  pwfseqlem3  10543  indpi  10790  nqereu  10812  ordpinq  10826  ltanq  10854  ltmnq  10855  suplem2pr  10936  map2psrpr  10993  ssxr  11174  leltne  11194  ltneg  11609  leneg  11612  suprnub  12079  negiso  12094  elnnnn0  12416  nn0sub  12423  fcdmnn0fsupp  12431  zrevaddcl  12509  znnsub  12510  znn0sub  12511  prime  12546  eluz2  12730  indstr  12806  eluz2b1  12809  qrevaddcl  12861  rpneg  12916  xrleltne  13036  dfle2  13038  dflt2  13039  supxrleub  13217  infxrgelb  13227  ixxin  13254  iccid  13282  elicopnf  13337  iccsplit  13377  fzsplit2  13441  fzsn  13458  fzpr  13471  uzsplit  13488  preduz  13542  fvinim0ffz  13681  injresinj  13683  om2uzf1oi  13852  lt2sqi  14088  le2sqi  14089  hashsdom  14280  hashf1lem1  14354  fz1isolem  14360  prprrab  14372  ccatlcan  14617  ccatrcan  14618  s3eq3seq  14838  2swrd2eqwrdeq  14852  trclfvcotr  14908  cnpart  15139  limsuplt  15378  rlimresb  15464  mertenslem2  15784  fprod2dlem  15879  sadadd2lem2  16353  saddisjlem  16367  bitsuz  16377  gcddiv  16454  algcvgblem  16480  isprm3  16586  isprm5  16610  prmreclem5  16824  vdwapun  16878  vdwmc2  16883  ramcl  16933  pwsle  17388  ismre  17484  mreacs  17556  acsfn  17557  iscatd2  17579  cidpropd  17608  dfiso2  17671  oppcsect2  17678  isfunc  17763  setcinv  17989  lubeldm  18249  lubval  18252  glbeldm  18262  glbval  18265  tosso  18315  ipodrsfi  18437  acsfiindd  18451  submgmacs  18617  imasmnd2  18674  ismhm0  18690  resmndismnd  18708  submacs  18727  imasgrp2  18960  issubg  19031  resgrpisgrp  19052  subgacs  19066  eqgval  19082  ghmqusnsglem1  19185  ghmquskerlem1  19188  gaorber  19213  symgfix2  19321  psgnran  19420  isslw  19513  sylow2alem2  19523  sylow2a  19524  sylow3lem6  19537  efgcpbllemb  19660  prmcyg  19799  gsum2d2lem  19878  gsumcom2  19880  subgdmdprd  19941  dprd2d2  19951  pgpfac1lem2  19982  pgpfac1lem4  19985  imasrng  20088  imasring  20241  isrnghmmul  20353  isnzr2  20426  isdomn3  20623  drngmulne0  20670  subrgacs  20708  sdrgacs  20709  lssle0  20876  lssacs  20893  lssats2  20926  lvecvsn0  21039  islpir  21258  zndvds  21479  znleval  21484  znleval2  21485  lindsmm  21758  islinds3  21764  islindf4  21768  ismhp3  22050  psdmul  22074  eltg2b  22867  discld  22997  opnssneib  23023  cldlp  23058  restbas  23066  leordtvallem1  23118  leordtvallem2  23119  ssidcn  23163  cnprest2  23198  lmss  23206  perfcls  23273  cmpfi  23316  1stccnp  23370  subislly  23389  hausmapdom  23408  locfindis  23438  iskgen3  23457  kgencn  23464  ptpjpre1  23479  xkoccn  23527  txrest  23539  txlm  23556  txkgen  23560  xkopt  23563  xkoinjcn  23595  imasnopn  23598  imasncld  23599  imasncls  23600  qtopcn  23622  kqfeq  23632  isr0  23645  fbfinnfr  23749  trfbas  23752  fbunfip  23777  ufileu  23827  cfinufil  23836  fmid  23868  txflf  23914  fclsrest  23932  alexsubALT  23959  tsmsres  24052  ucnima  24188  fmucndlem  24198  bldisj  24306  xmeter  24341  elbl4  24471  restmetu  24478  dscopn  24481  bl2ioo  24700  isphtpc  24913  tcphcph  25157  lmmbr2  25179  lmmbrf  25182  iscau2  25197  iscauf  25200  caucfil  25203  metcld  25226  metcld2  25227  bcthlem1  25244  bcthlem4  25247  cldcss2  25362  ovolgelb  25401  ovoliunlem1  25423  ismbfcn  25550  mbfmax  25570  mbfimaopnlem  25576  i1faddlem  25614  i1fmullem  25615  i1fres  25626  i1fpos  25627  itg1climres  25635  xrge0f  25652  itgresr  25700  iblcnlem1  25709  limcun  25816  dvres  25832  mdegmullem  26003  r1pid2  26087  ply1remlem  26090  plyremlem  26232  vieta1  26240  ulmcau  26324  sineq0  26453  coseq1  26454  ang180lem3  26741  cubic  26779  atandm  26806  atandm2  26807  atandm3  26808  rlimcnp  26895  rlimcnp2  26896  vmappw  27046  dchrelbas3  27169  dchrelbas4  27174  dchrsum2  27199  bposlem6  27220  2sqreuopltb  27396  2sqreuopnnltb  27398  dchrisumlem3  27422  pntleml  27542  noetasuplem4  27668  noetainflem4  27672  rightpos  27775  addsrid  27900  mulsrid  28045  mulsne0bd  28118  onsiso  28198  om2noseqf1o  28224  zn0subs  28320  avgslt1d  28369  avgslt2d  28370  istrkg3ld  28432  tgcgr4  28502  lnrot2  28595  islnopp  28710  islmib  28758  brbtwn2  28876  axsegconlem6  28893  axsegcon  28898  ax5seg  28909  axpasch  28912  axeuclid  28934  axcontlem4  28938  elntg2  28956  issubgr  29242  nb3gr2nb  29355  uhgrvd00  29506  isrusgr0  29538  wlkcpr  29600  wlkcomp  29602  upgr2wlk  29638  upgrf1istrl  29673  clwlkcomp  29750  clwlkcompbp  29753  iswwlksnx  29811  wspthsnwspthsnon  29887  wspniunwspnon  29894  2pthon3v  29914  usgr2wspthons3  29935  usgr2wspthon  29936  rusgrnumwwlks  29945  clwlkclwwlklem3  29971  clwlkclwwlk  29972  clwwlknonwwlknonb  30076  0pth  30095  eupth2lem2  30189  vdgn1frgrv2  30266  fusgreg2wsp  30306  clwwlknonclwlknonf1o  30332  dlwwlknondlwlknonf1o  30335  wlkl0  30337  nmoolb  30741  nmlno0lem  30763  ubthlem1  30840  ocsh  31253  shle0  31412  eigrei  31804  adjeu  31859  nmoplb  31877  nmfnlb  31894  eleigvec2  31928  nmlnop0iALT  31965  cnlnadjlem5  32041  adjbdln  32053  jplem2  32239  cvbr2  32253  mdsl2bi  32293  chrelat3  32341  eqelbid  32444  sq2reunnltb  32454  rmounid  32464  nelpr  32501  disjunsn  32564  ofpreima  32637  funcnvmpt  32639  funcnv5mpt  32640  dfcnv2  32648  suppiniseg  32657  gtiso  32672  fpwrelmap  32706  infxrge0glb  32738  xrdifh  32753  fzsplit3  32766  fzo0opth  32775  swrdrn3  32926  toslublem  32943  tosglblem  32945  mgcval  32958  mndlrinvb  32996  xrge0tsmsbi  33033  cntzun  33038  isarchi  33141  dvdsrspss  33342  rspsnasso  33343  lsmsnorb  33346  nsgqusf1olem2  33369  isprmidl  33393  ressply1mon1p  33521  r1pid2OLD  33559  constrfin  33749  smatrcl  33799  ist0cld  33836  rspectopn  33870  zarcls  33877  rhmpreimacnlem  33887  unitdivcld  33904  lmxrge0  33955  isrrext  34003  issibf  34336  eulerpartlemr  34377  eulerpartlemmf  34378  eulerpartlemn  34384  dstfrvunirn  34478  ballotlemfc0  34496  ballotlemfcc  34497  reprsuc  34618  reprpmtf1o  34629  reprdifc  34630  bnj919  34769  bnj976  34779  bnj1542  34859  bnj150  34878  bnj151  34879  bnj607  34918  bnj852  34923  bnj873  34926  bnj938  34939  bnj1171  35002  bnj1388  35035  bnj1489  35058  nummin  35093  usgrgt2cycl  35142  subfacp1lem3  35194  subfacp1lem5  35196  erdszelem9  35211  kur14  35228  iscvm  35271  satf0op  35389  mclsax  35581  rexxfr3dALT  35651  elintfv  35777  fundmpss  35779  opelco3  35787  dfon2  35805  dfbigcup2  35912  sscoid  35926  funpartfv  35958  dfrdg4  35964  cgr3permute3  36060  segletr  36127  segleantisym  36128  seglelin  36129  fneval  36365  neibastop3  36375  eltail  36387  filnetlem4  36394  bj-hbntbi  36717  bj-equsvt  36792  bj-sbceqgALT  36915  bj-clel3gALT  37061  bj-rest10  37101  bj-0int  37114  topdifinffinlem  37360  isbasisrelowllem1  37368  isbasisrelowllem2  37369  rdgeqoa  37383  finxpreclem4  37407  finxpsuclem  37410  wl-ifp4impr  37480  wl-1xor  37495  uncf  37618  phpreu  37623  cos2h  37630  tan2h  37631  matunitlindflem1  37635  poimirlem16  37655  poimirlem19  37658  poimirlem23  37662  poimirlem24  37663  poimirlem26  37665  poimirlem27  37666  mbfposadd  37686  cnambfre  37687  itg2addnclem  37690  itg2addnc  37693  iblabsnclem  37702  ftc1anclem1  37712  ftc1anclem5  37716  caures  37779  heiborlem3  37832  heiborlem10  37839  elghomOLD  37906  divrngidl  38047  eqrelf  38269  brvbrvvdif  38278  elrnres  38285  eldmres3  38290  eldmqsres2  38301  exanres  38308  relcnveq  38335  iss2  38351  ecinn0  38360  brxrn2  38382  ecxrn  38398  disjressuc2  38399  eldmcoss2  38475  eldm1cossres  38476  elrelsrel  38503  elrelscnveq  38508  elcoeleqvrelsrel  38612  brredundsredund  38643  brdmqssqs  38663  cnvepresdmqss  38669  eldmqs1cossres  38676  brerser  38694  erimeq2  38695  eleldisjseldisj  38746  prtlem10  38883  prtlem16  38887  prtlem19  38896  prtex  38898  prter3  38900  islshpat  39035  lcvbr2  39040  lcvbr3  39041  lshpsmreu  39127  isat3  39325  hlrelat5N  39419  islpln5  39553  cdlemblem  39811  paddvaln0N  39819  paddval0  39828  cdlemefrs29bpre1  40415  cdlemefrs29cpre1  40416  cdlemg27b  40714  cdlemg33c  40726  cdlemg33e  40728  diaglbN  41073  cdlemm10N  41136  dicopelval2  41199  dicelval2N  41200  dihopelvalcpre  41266  dihglbcpreN  41318  dih1dimatlem  41347  dihatexv  41356  dvh4dimlem  41461  mapdpglem3  41693  hdmap14lem13  41898  hdmapglem7a  41945  eluzp1  42319  fsuppind  42602  isnacs2  42718  rabrenfdioph  42826  expdiophlem1  43033  pw2f1ocnv  43049  pwfi2f1o  43108  numinfctb  43115  dfacbasgrp  43120  islnr3  43127  onsupneqmaxlim0  43236  onsupnmax  43240  onsupuni  43241  tfsconcatrnss  43362  safesnsupfilb  43430  dfhe3  43787  clsk3nimkb  44052  ntrneiiso  44103  ntrneikb  44106  scottabf  44252  mnuunid  44289  hashnzfzclim  44334  dvconstbi  44346  sbcoreleleqVD  44870  trfr  44974  permac8prim  45026  rfcnpre3  45049  rfcnpre4  45050  r19.3rzf  45174  cncfshift  45891  stoweidlem59  46076  dfafv23  47263  nelbrnel  47286  elsetpreimafvrab  47404  iccpartiun  47444  prproropf1olem0  47512  prprelb  47526  prprspr2  47528  reuprpr  47533  oddm1evenALTV  47685  oddp1evenALTV  47686  oddprmne2  47725  fpprel  47738  dfvopnbgr2  47863  uhgrimisgrgric  47941  isgrlim  47992  gpg5nbgrvtx03starlem1  48078  gpg5nbgrvtx03starlem3  48080  gpg5nbgrvtx13starlem1  48081  gpg5nbgrvtx13starlem3  48083  iscmgmALT  48234  iscsgrpALT  48236  mofeu  48858  iscnrm3  48962  joindm2  48978  meetdm2  48980  oppcendc  49029  0funcg  49096  0funcALT  49099  istermc  49485  functermc2  49520  fulltermc  49522  elpglem2  49723