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  3618  eueq3  3670  sbceqal  3803  eqrrabd  4039  n0moeu  4312  sbcel12  4364  sbceqg  4365  sbcne12  4368  reldisj  4406  raldifeq  4447  r19.3rz  4455  eldifpr  4616  reusngf  4632  rexreusng  4637  eldiftp  4645  eqsndOLD  4788  reusv2lem5  5348  prelpw  5395  otthg  5434  2rbropap  5513  rabxp  5673  pwvrel  5675  ssrel3  5736  elrng  5841  iss  5995  idrefALT  6071  xpcan  6135  xpcan2  6136  dfpo2  6255  ordelpss  6346  fcnvres  6712  dffv3  6831  funimass4  6899  unima  6910  funcnvmpt  6944  fndmdif  6989  fneqeql  6993  funimass3  7001  elrnrexdmb  7037  dff4  7048  fnsnbg  7112  fnsnbOLD  7114  fconst4  7162  elunirn  7199  f12dfv  7221  riota1  7338  riota2df  7340  f1ocnvfv3  7355  eqfnov  7489  elrnmpores  7498  caoftrn  7665  ordsucun  7769  dflim3  7791  dfom2  7812  peano5  7837  opiota  8005  frxp2  8088  xpord2pred  8089  xpord2indlem  8091  suppssr  8139  mpoxopovel  8164  brtpos  8179  rntpos  8183  ordgt0ge1  8422  ondif2  8431  oelim2  8525  omabs  8581  naddrid  8613  iiner  8730  erinxp  8732  qliftfun  8743  mapdm0  8783  ordunifi  9194  elfi2  9321  elfiun  9337  fifo  9339  noinfep  9573  cantnflem1  9602  cantnf  9606  rankonidlem  9744  r1pwALT  9762  cardalephex  10004  alephinit  10009  dfac5lem4OLD  10042  cflim2  10177  cfsmolem  10184  compssiso  10288  fin1a2lem11  10324  itunisuc  10333  axdclem  10433  brdom6disj  10446  alephreg  10497  fpwwe2lem8  10553  pwfseqlem3  10575  indpi  10822  nqereu  10844  ordpinq  10858  ltanq  10886  ltmnq  10887  suplem2pr  10968  map2psrpr  11025  ssxr  11206  leltne  11226  ltneg  11641  leneg  11644  suprnub  12111  negiso  12126  elnnnn0  12448  nn0sub  12455  fcdmnn0fsupp  12463  zrevaddcl  12540  znnsub  12541  znn0sub  12542  prime  12577  eluz2  12761  indstr  12833  eluz2b1  12836  qrevaddcl  12888  rpneg  12943  xrleltne  13063  dfle2  13065  dflt2  13066  supxrleub  13245  infxrgelb  13255  ixxin  13282  iccid  13310  elicopnf  13365  iccsplit  13405  fzsplit2  13469  fzsn  13486  fzpr  13499  uzsplit  13516  preduz  13570  fvinim0ffz  13709  injresinj  13711  om2uzf1oi  13880  lt2sqi  14116  le2sqi  14117  hashsdom  14308  hashf1lem1  14382  fz1isolem  14388  prprrab  14400  ccatlcan  14645  ccatrcan  14646  s3eq3seq  14866  2swrd2eqwrdeq  14880  trclfvcotr  14936  cnpart  15167  limsuplt  15406  rlimresb  15492  mertenslem2  15812  fprod2dlem  15907  sadadd2lem2  16381  saddisjlem  16395  bitsuz  16405  gcddiv  16482  algcvgblem  16508  isprm3  16614  isprm5  16638  prmreclem5  16852  vdwapun  16906  vdwmc2  16911  ramcl  16961  pwsle  17417  ismre  17513  mreacs  17585  acsfn  17586  iscatd2  17608  cidpropd  17637  dfiso2  17700  oppcsect2  17707  isfunc  17792  setcinv  18018  lubeldm  18278  lubval  18281  glbeldm  18291  glbval  18294  tosso  18344  ipodrsfi  18466  acsfiindd  18480  submgmacs  18646  imasmnd2  18703  ismhm0  18719  resmndismnd  18737  submacs  18756  imasgrp2  18989  issubg  19060  resgrpisgrp  19081  subgacs  19094  eqgval  19110  ghmqusnsglem1  19213  ghmquskerlem1  19216  gaorber  19241  symgfix2  19349  psgnran  19448  isslw  19541  sylow2alem2  19551  sylow2a  19552  sylow3lem6  19565  efgcpbllemb  19688  prmcyg  19827  gsum2d2lem  19906  gsumcom2  19908  subgdmdprd  19969  dprd2d2  19979  pgpfac1lem2  20010  pgpfac1lem4  20013  imasrng  20116  imasring  20270  isrnghmmul  20382  isnzr2  20455  isdomn3  20652  drngmulne0  20699  subrgacs  20737  sdrgacs  20738  lssle0  20905  lssacs  20922  lssats2  20955  lvecvsn0  21068  islpir  21287  zndvds  21508  znleval  21513  znleval2  21514  lindsmm  21787  islinds3  21793  islindf4  21797  ismhp3  22089  psdmul  22113  eltg2b  22907  discld  23037  opnssneib  23063  cldlp  23098  restbas  23106  leordtvallem1  23158  leordtvallem2  23159  ssidcn  23203  cnprest2  23238  lmss  23246  perfcls  23313  cmpfi  23356  1stccnp  23410  subislly  23429  hausmapdom  23448  locfindis  23478  iskgen3  23497  kgencn  23504  ptpjpre1  23519  xkoccn  23567  txrest  23579  txlm  23596  txkgen  23600  xkopt  23603  xkoinjcn  23635  imasnopn  23638  imasncld  23639  imasncls  23640  qtopcn  23662  kqfeq  23672  isr0  23685  fbfinnfr  23789  trfbas  23792  fbunfip  23817  ufileu  23867  cfinufil  23876  fmid  23908  txflf  23954  fclsrest  23972  alexsubALT  23999  tsmsres  24092  ucnima  24228  fmucndlem  24238  bldisj  24346  xmeter  24381  elbl4  24511  restmetu  24518  dscopn  24521  bl2ioo  24740  isphtpc  24953  tcphcph  25197  lmmbr2  25219  lmmbrf  25222  iscau2  25237  iscauf  25240  caucfil  25243  metcld  25266  metcld2  25267  bcthlem1  25284  bcthlem4  25287  cldcss2  25402  ovolgelb  25441  ovoliunlem1  25463  ismbfcn  25590  mbfmax  25610  mbfimaopnlem  25616  i1faddlem  25654  i1fmullem  25655  i1fres  25666  i1fpos  25667  itg1climres  25675  xrge0f  25692  itgresr  25740  iblcnlem1  25749  limcun  25856  dvres  25872  mdegmullem  26043  r1pid2  26127  ply1remlem  26130  plyremlem  26272  vieta1  26280  ulmcau  26364  sineq0  26493  coseq1  26494  ang180lem3  26781  cubic  26819  atandm  26846  atandm2  26847  atandm3  26848  rlimcnp  26935  rlimcnp2  26936  vmappw  27086  dchrelbas3  27209  dchrelbas4  27214  dchrsum2  27239  bposlem6  27260  2sqreuopltb  27436  2sqreuopnnltb  27438  dchrisumlem3  27462  pntleml  27582  noetasuplem4  27708  noetainflem4  27712  rightpos  27819  addsrid  27946  negsleft  28040  negsright  28041  mulsrid  28095  mulsne0bd  28168  onsiso  28252  om2noseqf1o  28282  zn0subs  28382  avgslt1d  28432  avgslt2d  28433  istrkg3ld  28516  tgcgr4  28586  lnrot2  28679  islnopp  28794  islmib  28842  mptelee  28950  brbtwn2  28961  axsegconlem6  28978  axsegcon  28983  ax5seg  28994  axpasch  28997  axeuclid  29019  axcontlem4  29023  elntg2  29041  issubgr  29327  nb3gr2nb  29440  uhgrvd00  29591  isrusgr0  29623  wlkcpr  29685  wlkcomp  29687  upgr2wlk  29723  upgrf1istrl  29758  clwlkcomp  29835  clwlkcompbp  29838  iswwlksnx  29896  wspthsnwspthsnon  29972  wspniunwspnon  29979  2pthon3v  29999  usgr2wspthons3  30023  usgr2wspthon  30024  rusgrnumwwlks  30033  clwlkclwwlklem3  30059  clwlkclwwlk  30060  clwwlknonwwlknonb  30164  0pth  30183  eupth2lem2  30277  vdgn1frgrv2  30354  fusgreg2wsp  30394  clwwlknonclwlknonf1o  30420  dlwwlknondlwlknonf1o  30423  wlkl0  30425  nmoolb  30829  nmlno0lem  30851  ubthlem1  30928  ocsh  31341  shle0  31500  eigrei  31892  adjeu  31947  nmoplb  31965  nmfnlb  31982  eleigvec2  32016  nmlnop0iALT  32053  cnlnadjlem5  32129  adjbdln  32141  jplem2  32327  cvbr2  32341  mdsl2bi  32381  chrelat3  32429  eqelbid  32531  sq2reunnltb  32541  rmounid  32551  nelpr  32588  disjunsn  32651  ofpreima  32725  funcnv5mpt  32727  dfcnv2  32735  suppiniseg  32746  gtiso  32761  fpwrelmap  32793  infxrge0glb  32826  xrdifh  32841  fzsplit3  32854  fzo0opth  32864  swrdrn3  33018  toslublem  33035  tosglblem  33037  mgcval  33050  mndlrinvb  33088  xrge0tsmsbi  33137  cntzun  33142  isarchi  33245  dvdsrspss  33449  rspsnasso  33450  lsmsnorb  33453  nsgqusf1olem2  33476  isprmidl  33500  ressply1mon1p  33630  r1pid2OLD  33671  constrfin  33884  smatrcl  33934  ist0cld  33971  rspectopn  34005  zarcls  34012  rhmpreimacnlem  34022  unitdivcld  34039  lmxrge0  34090  isrrext  34138  issibf  34471  eulerpartlemr  34512  eulerpartlemmf  34513  eulerpartlemn  34519  dstfrvunirn  34613  ballotlemfc0  34631  ballotlemfcc  34632  reprsuc  34753  reprpmtf1o  34764  reprdifc  34765  bnj919  34904  bnj976  34914  bnj1542  34994  bnj150  35013  bnj151  35014  bnj607  35053  bnj852  35058  bnj873  35061  bnj938  35074  bnj1171  35137  bnj1388  35170  bnj1489  35193  nummin  35230  usgrgt2cycl  35305  subfacp1lem3  35357  subfacp1lem5  35359  erdszelem9  35374  kur14  35391  iscvm  35434  satf0op  35552  mclsax  35744  rexxfr3dALT  35814  elintfv  35940  fundmpss  35942  opelco3  35950  dfon2  35965  dfbigcup2  36072  sscoid  36086  funpartfv  36120  dfrdg4  36126  cgr3permute3  36222  segletr  36289  segleantisym  36290  seglelin  36291  fneval  36527  neibastop3  36537  eltail  36549  filnetlem4  36556  bj-hbntbi  36880  bj-equsvt  36955  bj-sbceqgALT  37078  bj-clel3gALT  37224  bj-rest10  37264  bj-0int  37277  topdifinffinlem  37523  isbasisrelowllem1  37531  isbasisrelowllem2  37532  rdgeqoa  37546  finxpreclem4  37570  finxpsuclem  37573  wl-ifp4impr  37643  wl-1xor  37658  uncf  37771  phpreu  37776  cos2h  37783  tan2h  37784  matunitlindflem1  37788  poimirlem16  37808  poimirlem19  37811  poimirlem23  37815  poimirlem24  37816  poimirlem26  37818  poimirlem27  37819  mbfposadd  37839  cnambfre  37840  itg2addnclem  37843  itg2addnc  37846  iblabsnclem  37855  ftc1anclem1  37865  ftc1anclem5  37869  caures  37932  heiborlem3  37985  heiborlem10  37992  elghomOLD  38059  divrngidl  38200  eqrelf  38430  brvbrvvdif  38441  elrnres  38450  eldmres3  38455  eldmqsres2  38466  exanres  38473  relcnveq  38500  iss2  38516  ecinn0  38525  raldmqsmo  38535  brxrn2  38556  ecxrn  38578  ecxrn2  38580  disjressuc2  38583  elrelsrel  38614  eldmcoss2  38721  eldm1cossres  38722  elrelscnveq  38800  elcoeleqvrelsrel  38852  brredundsredund  38883  brdmqssqs  38903  cnvepresdmqss  38909  eldmqs1cossres  38916  brerser  38934  erimeq2  38935  eleldisjseldisj  39001  prtlem10  39162  prtlem16  39166  prtlem19  39175  prtex  39177  prter3  39179  islshpat  39314  lcvbr2  39319  lcvbr3  39320  lshpsmreu  39406  isat3  39604  hlrelat5N  39698  islpln5  39832  cdlemblem  40090  paddvaln0N  40098  paddval0  40107  cdlemefrs29bpre1  40694  cdlemefrs29cpre1  40695  cdlemg27b  40993  cdlemg33c  41005  cdlemg33e  41007  diaglbN  41352  cdlemm10N  41415  dicopelval2  41478  dicelval2N  41479  dihopelvalcpre  41545  dihglbcpreN  41597  dih1dimatlem  41626  dihatexv  41635  dvh4dimlem  41740  mapdpglem3  41972  hdmap14lem13  42177  hdmapglem7a  42224  eluzp1  42598  fsuppind  42869  isnacs2  42984  rabrenfdioph  43092  expdiophlem1  43299  pw2f1ocnv  43315  pwfi2f1o  43374  numinfctb  43381  dfacbasgrp  43386  islnr3  43393  onsupneqmaxlim0  43502  onsupnmax  43506  onsupuni  43507  tfsconcatrnss  43628  safesnsupfilb  43695  dfhe3  44052  clsk3nimkb  44317  ntrneiiso  44368  ntrneikb  44371  scottabf  44517  mnuunid  44554  hashnzfzclim  44599  dvconstbi  44611  sbcoreleleqVD  45135  trfr  45239  permac8prim  45291  rfcnpre3  45314  rfcnpre4  45315  r19.3rzf  45438  cncfshift  46154  stoweidlem59  46339  chnsubseqwl  47159  dfafv23  47535  nelbrnel  47558  elsetpreimafvrab  47676  iccpartiun  47716  prproropf1olem0  47784  prprelb  47798  prprspr2  47800  reuprpr  47805  oddm1evenALTV  47957  oddp1evenALTV  47958  oddprmne2  47997  fpprel  48010  dfvopnbgr2  48135  uhgrimisgrgric  48213  isgrlim  48264  gpg5nbgrvtx03starlem1  48350  gpg5nbgrvtx03starlem3  48352  gpg5nbgrvtx13starlem1  48353  gpg5nbgrvtx13starlem3  48355  iscmgmALT  48506  iscsgrpALT  48508  mofeu  49129  iscnrm3  49233  joindm2  49249  meetdm2  49251  oppcendc  49299  0funcg  49366  0funcALT  49369  istermc  49755  functermc2  49790  fulltermc  49792  elpglem2  49993