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  3629  eueq3  3682  sbceqal  3815  eqrrabd  4049  n0moeu  4322  sbcel12  4374  sbceqg  4375  sbcne12  4378  reldisj  4416  raldifeq  4457  r19.3rz  4460  ralf0  4477  eldifpr  4622  reusngf  4638  rexreusng  4643  eldiftp  4651  eqsndOLD  4795  reusv2lem5  5357  prelpw  5406  otthg  5445  2rbropap  5526  rabxp  5686  pwvrel  5688  ssrel3  5749  elrng  5855  iss  6006  idrefALT  6084  xpcan  6149  xpcan2  6150  dfpo2  6269  ordelpss  6360  fcnvres  6737  dffv3  6854  funimass4  6925  unima  6936  fndmdif  7014  fneqeql  7018  funimass3  7026  elrnrexdmb  7062  dff4  7073  fnsnbg  7138  fnsnbOLD  7140  fconst4  7188  elunirn  7225  f12dfv  7248  riota1  7365  riota2df  7367  f1ocnvfv3  7382  eqfnov  7518  elrnmpores  7527  caoftrn  7694  ordsucun  7800  dflim3  7823  dfom2  7844  peano5  7869  opiota  8038  frxp2  8123  xpord2pred  8124  xpord2indlem  8126  suppssr  8174  mpoxopovel  8199  brtpos  8214  rntpos  8218  ordgt0ge1  8457  ondif2  8466  oelim2  8559  omabs  8615  naddrid  8647  iiner  8762  erinxp  8764  qliftfun  8775  mapdm0  8815  ordunifi  9237  elfi2  9365  elfiun  9381  fifo  9383  noinfep  9613  cantnflem1  9642  cantnf  9646  rankonidlem  9781  r1pwALT  9799  pr2nelemOLD  9956  cardalephex  10043  alephinit  10048  dfac5lem4OLD  10081  cflim2  10216  cfsmolem  10223  compssiso  10327  fin1a2lem11  10363  itunisuc  10372  axdclem  10472  brdom6disj  10485  alephreg  10535  fpwwe2lem8  10591  pwfseqlem3  10613  indpi  10860  nqereu  10882  ordpinq  10896  ltanq  10924  ltmnq  10925  suplem2pr  11006  map2psrpr  11063  ssxr  11243  leltne  11263  ltneg  11678  leneg  11681  suprnub  12148  negiso  12163  elnnnn0  12485  nn0sub  12492  fcdmnn0fsupp  12500  zrevaddcl  12578  znnsub  12579  znn0sub  12580  prime  12615  eluz2  12799  indstr  12875  eluz2b1  12878  qrevaddcl  12930  rpneg  12985  xrleltne  13105  dfle2  13107  dflt2  13108  supxrleub  13286  infxrgelb  13296  ixxin  13323  iccid  13351  elicopnf  13406  iccsplit  13446  fzsplit2  13510  fzsn  13527  fzpr  13540  uzsplit  13557  preduz  13611  fvinim0ffz  13747  injresinj  13749  om2uzf1oi  13918  lt2sqi  14154  le2sqi  14155  hashsdom  14346  hashf1lem1  14420  fz1isolem  14426  prprrab  14438  ccatlcan  14683  ccatrcan  14684  s3eq3seq  14905  2swrd2eqwrdeq  14919  trclfvcotr  14975  cnpart  15206  limsuplt  15445  rlimresb  15531  mertenslem2  15851  fprod2dlem  15946  sadadd2lem2  16420  saddisjlem  16434  bitsuz  16444  gcddiv  16521  algcvgblem  16547  isprm3  16653  isprm5  16677  prmreclem5  16891  vdwapun  16945  vdwmc2  16950  ramcl  17000  pwsle  17455  ismre  17551  mreacs  17619  acsfn  17620  iscatd2  17642  cidpropd  17671  dfiso2  17734  oppcsect2  17741  isfunc  17826  setcinv  18052  lubeldm  18312  lubval  18315  glbeldm  18325  glbval  18328  tosso  18378  ipodrsfi  18498  acsfiindd  18512  submgmacs  18644  imasmnd2  18701  ismhm0  18717  resmndismnd  18735  submacs  18754  imasgrp2  18987  issubg  19058  resgrpisgrp  19079  subgacs  19093  eqgval  19109  ghmqusnsglem1  19212  ghmquskerlem1  19215  gaorber  19240  symgfix2  19346  psgnran  19445  isslw  19538  sylow2alem2  19548  sylow2a  19549  sylow3lem6  19562  efgcpbllemb  19685  prmcyg  19824  gsum2d2lem  19903  gsumcom2  19905  subgdmdprd  19966  dprd2d2  19976  pgpfac1lem2  20007  pgpfac1lem4  20010  imasrng  20086  imasring  20239  isrnghmmul  20351  isnzr2  20427  isdomn3  20624  drngmulne0  20671  subrgacs  20709  sdrgacs  20710  lssle0  20856  lssacs  20873  lssats2  20906  lvecvsn0  21019  islpir  21238  zndvds  21459  znleval  21464  znleval2  21465  lindsmm  21737  islinds3  21743  islindf4  21747  ismhp3  22029  psdmul  22053  eltg2b  22846  discld  22976  opnssneib  23002  cldlp  23037  restbas  23045  leordtvallem1  23097  leordtvallem2  23098  ssidcn  23142  cnprest2  23177  lmss  23185  perfcls  23252  cmpfi  23295  1stccnp  23349  subislly  23368  hausmapdom  23387  locfindis  23417  iskgen3  23436  kgencn  23443  ptpjpre1  23458  xkoccn  23506  txrest  23518  txlm  23535  txkgen  23539  xkopt  23542  xkoinjcn  23574  imasnopn  23577  imasncld  23578  imasncls  23579  qtopcn  23601  kqfeq  23611  isr0  23624  fbfinnfr  23728  trfbas  23731  fbunfip  23756  ufileu  23806  cfinufil  23815  fmid  23847  txflf  23893  fclsrest  23911  alexsubALT  23938  tsmsres  24031  ucnima  24168  fmucndlem  24178  bldisj  24286  xmeter  24321  elbl4  24451  restmetu  24458  dscopn  24461  bl2ioo  24680  isphtpc  24893  tcphcph  25137  lmmbr2  25159  lmmbrf  25162  iscau2  25177  iscauf  25180  caucfil  25183  metcld  25206  metcld2  25207  bcthlem1  25224  bcthlem4  25227  cldcss2  25342  ovolgelb  25381  ovoliunlem1  25403  ismbfcn  25530  mbfmax  25550  mbfimaopnlem  25556  i1faddlem  25594  i1fmullem  25595  i1fres  25606  i1fpos  25607  itg1climres  25615  xrge0f  25632  itgresr  25680  iblcnlem1  25689  limcun  25796  dvres  25812  mdegmullem  25983  r1pid2  26067  ply1remlem  26070  plyremlem  26212  vieta1  26220  ulmcau  26304  sineq0  26433  coseq1  26434  ang180lem3  26721  cubic  26759  atandm  26786  atandm2  26787  atandm3  26788  rlimcnp  26875  rlimcnp2  26876  vmappw  27026  dchrelbas3  27149  dchrelbas4  27154  dchrsum2  27179  bposlem6  27200  2sqreuopltb  27376  2sqreuopnnltb  27378  dchrisumlem3  27402  pntleml  27522  noetasuplem4  27648  noetainflem4  27652  addsrid  27871  mulsrid  28016  mulsne0bd  28089  onsiso  28169  om2noseqf1o  28195  zn0subs  28291  istrkg3ld  28388  tgcgr4  28458  lnrot2  28551  islnopp  28666  islmib  28714  brbtwn2  28832  axsegconlem6  28849  axsegcon  28854  ax5seg  28865  axpasch  28868  axeuclid  28890  axcontlem4  28894  elntg2  28912  issubgr  29198  nb3gr2nb  29311  uhgrvd00  29462  isrusgr0  29494  wlkcpr  29557  wlkcomp  29559  upgr2wlk  29596  upgrf1istrl  29631  clwlkcomp  29709  clwlkcompbp  29712  iswwlksnx  29770  wspthsnwspthsnon  29846  wspniunwspnon  29853  2pthon3v  29873  usgr2wspthons3  29894  usgr2wspthon  29895  rusgrnumwwlks  29904  clwlkclwwlklem3  29930  clwlkclwwlk  29931  clwwlknonwwlknonb  30035  0pth  30054  eupth2lem2  30148  vdgn1frgrv2  30225  fusgreg2wsp  30265  clwwlknonclwlknonf1o  30291  dlwwlknondlwlknonf1o  30294  wlkl0  30296  nmoolb  30700  nmlno0lem  30722  ubthlem1  30799  ocsh  31212  shle0  31371  eigrei  31763  adjeu  31818  nmoplb  31836  nmfnlb  31853  eleigvec2  31887  nmlnop0iALT  31924  cnlnadjlem5  32000  adjbdln  32012  jplem2  32198  cvbr2  32212  mdsl2bi  32252  chrelat3  32300  eqelbid  32404  sq2reunnltb  32414  rmounid  32424  nelpr  32460  disjunsn  32523  ofpreima  32589  funcnvmpt  32591  funcnv5mpt  32592  dfcnv2  32600  suppiniseg  32609  gtiso  32624  fpwrelmap  32656  infxrge0glb  32688  xrdifh  32703  fzsplit3  32716  fzo0opth  32728  swrdrn3  32877  toslublem  32898  tosglblem  32900  mgcval  32913  mndlrinvb  32966  xrge0tsmsbi  33003  cntzun  33008  isarchi  33136  dvdsrspss  33358  rspsnasso  33359  lsmsnorb  33362  nsgqusf1olem2  33385  isprmidl  33409  ressply1mon1p  33537  r1pid2OLD  33574  constrfin  33736  smatrcl  33786  ist0cld  33823  rspectopn  33857  zarcls  33864  rhmpreimacnlem  33874  unitdivcld  33891  lmxrge0  33942  isrrext  33990  issibf  34324  eulerpartlemr  34365  eulerpartlemmf  34366  eulerpartlemn  34372  dstfrvunirn  34466  ballotlemfc0  34484  ballotlemfcc  34485  reprsuc  34606  reprpmtf1o  34617  reprdifc  34618  bnj919  34757  bnj976  34767  bnj1542  34847  bnj150  34866  bnj151  34867  bnj607  34906  bnj852  34911  bnj873  34914  bnj938  34927  bnj1171  34990  bnj1388  35023  bnj1489  35046  nummin  35081  usgrgt2cycl  35117  subfacp1lem3  35169  subfacp1lem5  35171  erdszelem9  35186  kur14  35203  iscvm  35246  satf0op  35364  mclsax  35556  rexxfr3dALT  35626  elintfv  35752  fundmpss  35754  opelco3  35762  dfon2  35780  dfbigcup2  35887  sscoid  35901  funpartfv  35933  dfrdg4  35939  cgr3permute3  36035  segletr  36102  segleantisym  36103  seglelin  36104  fneval  36340  neibastop3  36350  eltail  36362  filnetlem4  36369  bj-hbntbi  36692  bj-equsvt  36767  bj-sbceqgALT  36890  bj-clel3gALT  37036  bj-rest10  37076  bj-0int  37089  topdifinffinlem  37335  isbasisrelowllem1  37343  isbasisrelowllem2  37344  rdgeqoa  37358  finxpreclem4  37382  finxpsuclem  37385  wl-ifp4impr  37455  wl-1xor  37470  uncf  37593  phpreu  37598  cos2h  37605  tan2h  37606  matunitlindflem1  37610  poimirlem16  37630  poimirlem19  37633  poimirlem23  37637  poimirlem24  37638  poimirlem26  37640  poimirlem27  37641  mbfposadd  37661  cnambfre  37662  itg2addnclem  37665  itg2addnc  37668  iblabsnclem  37677  ftc1anclem1  37687  ftc1anclem5  37691  caures  37754  heiborlem3  37807  heiborlem10  37814  elghomOLD  37881  divrngidl  38022  eqrelf  38244  brvbrvvdif  38253  elrnres  38260  eldmres3  38265  eldmqsres2  38276  exanres  38283  relcnveq  38310  iss2  38326  ecinn0  38335  brxrn2  38357  ecxrn  38373  disjressuc2  38374  eldmcoss2  38450  eldm1cossres  38451  elrelsrel  38478  elrelscnveq  38483  elcoeleqvrelsrel  38587  brredundsredund  38618  brdmqssqs  38638  cnvepresdmqss  38644  eldmqs1cossres  38651  brerser  38669  erimeq2  38670  eleldisjseldisj  38721  prtlem10  38858  prtlem16  38862  prtlem19  38871  prtex  38873  prter3  38875  islshpat  39010  lcvbr2  39015  lcvbr3  39016  lshpsmreu  39102  isat3  39300  hlrelat5N  39395  islpln5  39529  cdlemblem  39787  paddvaln0N  39795  paddval0  39804  cdlemefrs29bpre1  40391  cdlemefrs29cpre1  40392  cdlemg27b  40690  cdlemg33c  40702  cdlemg33e  40704  diaglbN  41049  cdlemm10N  41112  dicopelval2  41175  dicelval2N  41176  dihopelvalcpre  41242  dihglbcpreN  41294  dih1dimatlem  41323  dihatexv  41332  dvh4dimlem  41437  mapdpglem3  41669  hdmap14lem13  41874  hdmapglem7a  41921  eluzp1  42295  fsuppind  42578  isnacs2  42694  rabrenfdioph  42802  expdiophlem1  43010  pw2f1ocnv  43026  pwfi2f1o  43085  numinfctb  43092  dfacbasgrp  43097  islnr3  43104  onsupneqmaxlim0  43213  onsupnmax  43217  onsupuni  43218  tfsconcatrnss  43339  safesnsupfilb  43407  dfhe3  43764  clsk3nimkb  44029  ntrneiiso  44080  ntrneikb  44083  scottabf  44229  mnuunid  44266  hashnzfzclim  44311  dvconstbi  44323  sbcoreleleqVD  44848  trfr  44952  permac8prim  45004  rfcnpre3  45027  rfcnpre4  45028  r19.3rzf  45152  cncfshift  45872  stoweidlem59  46057  dfafv23  47254  nelbrnel  47277  elsetpreimafvrab  47395  iccpartiun  47435  prproropf1olem0  47503  prprelb  47517  prprspr2  47519  reuprpr  47524  oddm1evenALTV  47676  oddp1evenALTV  47677  oddprmne2  47716  fpprel  47729  dfvopnbgr2  47853  uhgrimisgrgric  47931  isgrlim  47981  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem3  48064  iscmgmALT  48212  iscsgrpALT  48214  mofeu  48836  iscnrm3  48940  joindm2  48956  meetdm2  48958  oppcendc  49007  0funcg  49074  0funcALT  49077  istermc  49463  functermc2  49498  fulltermc  49500  elpglem2  49701