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  5337  prelpw  5391  otthg  5431  2rbropap  5510  rabxp  5670  pwvrel  5672  ssrel3  5733  elrng  5838  iss  5992  idrefALT  6068  xpcan  6132  xpcan2  6133  dfpo2  6252  ordelpss  6343  fcnvres  6709  dffv3  6828  funimass4  6896  unima  6907  funcnvmpt  6941  fndmdif  6986  fneqeql  6990  funimass3  6998  elrnrexdmb  7034  dff4  7045  fnsnbg  7110  fnsnbOLD  7112  fconst4  7160  elunirn  7197  f12dfv  7219  riota1  7336  riota2df  7338  f1ocnvfv3  7353  eqfnov  7487  elrnmpores  7496  caoftrn  7663  ordsucun  7767  dflim3  7789  dfom2  7810  peano5  7835  opiota  8003  frxp2  8085  xpord2pred  8086  xpord2indlem  8088  suppssr  8136  mpoxopovel  8161  brtpos  8176  rntpos  8180  ordgt0ge1  8419  ondif2  8428  oelim2  8522  omabs  8578  naddrid  8610  iiner  8727  erinxp  8729  qliftfun  8740  mapdm0  8780  ordunifi  9191  elfi2  9318  elfiun  9334  fifo  9336  noinfep  9570  cantnflem1  9599  cantnf  9603  rankonidlem  9741  r1pwALT  9759  cardalephex  10001  alephinit  10006  dfac5lem4OLD  10039  cflim2  10174  cfsmolem  10181  compssiso  10285  fin1a2lem11  10321  itunisuc  10330  axdclem  10430  brdom6disj  10443  alephreg  10494  fpwwe2lem8  10550  pwfseqlem3  10572  indpi  10819  nqereu  10841  ordpinq  10855  ltanq  10883  ltmnq  10884  suplem2pr  10965  map2psrpr  11022  ssxr  11204  leltne  11224  ltneg  11639  leneg  11642  suprnub  12110  negiso  12125  elnnnn0  12469  nn0sub  12476  fcdmnn0fsupp  12484  zrevaddcl  12561  znnsub  12562  znn0sub  12563  prime  12599  eluz2  12783  indstr  12855  eluz2b1  12858  qrevaddcl  12910  rpneg  12965  xrleltne  13085  dfle2  13087  dflt2  13088  supxrleub  13267  infxrgelb  13277  ixxin  13304  iccid  13332  elicopnf  13387  iccsplit  13427  fzsplit2  13492  fzsn  13509  fzpr  13522  uzsplit  13539  preduz  13593  fvinim0ffz  13733  injresinj  13735  om2uzf1oi  13904  lt2sqi  14140  le2sqi  14141  hashsdom  14332  hashf1lem1  14406  fz1isolem  14412  prprrab  14424  ccatlcan  14669  ccatrcan  14670  s3eq3seq  14890  2swrd2eqwrdeq  14904  trclfvcotr  14960  cnpart  15191  limsuplt  15430  rlimresb  15516  mertenslem2  15839  fprod2dlem  15934  sadadd2lem2  16408  saddisjlem  16422  bitsuz  16432  gcddiv  16509  algcvgblem  16535  isprm3  16641  isprm5  16666  prmreclem5  16880  vdwapun  16934  vdwmc2  16939  ramcl  16989  pwsle  17445  ismre  17541  mreacs  17613  acsfn  17614  iscatd2  17636  cidpropd  17665  dfiso2  17728  oppcsect2  17735  isfunc  17820  setcinv  18046  lubeldm  18306  lubval  18309  glbeldm  18319  glbval  18322  tosso  18372  ipodrsfi  18494  acsfiindd  18508  submgmacs  18674  imasmnd2  18731  ismhm0  18747  resmndismnd  18765  submacs  18784  imasgrp2  19020  issubg  19091  resgrpisgrp  19112  subgacs  19125  eqgval  19141  ghmqusnsglem1  19244  ghmquskerlem1  19247  gaorber  19272  symgfix2  19380  psgnran  19479  isslw  19572  sylow2alem2  19582  sylow2a  19583  sylow3lem6  19596  efgcpbllemb  19719  prmcyg  19858  gsum2d2lem  19937  gsumcom2  19939  subgdmdprd  20000  dprd2d2  20010  pgpfac1lem2  20041  pgpfac1lem4  20044  imasrng  20147  imasring  20299  isrnghmmul  20411  isnzr2  20484  isdomn3  20681  drngmulne0  20728  subrgacs  20766  sdrgacs  20767  lssle0  20934  lssacs  20951  lssats2  20984  lvecvsn0  21097  islpir  21316  zndvds  21537  znleval  21542  znleval2  21543  lindsmm  21816  islinds3  21822  islindf4  21826  ismhp3  22117  psdmul  22141  eltg2b  22933  discld  23063  opnssneib  23089  cldlp  23124  restbas  23132  leordtvallem1  23184  leordtvallem2  23185  ssidcn  23229  cnprest2  23264  lmss  23272  perfcls  23339  cmpfi  23382  1stccnp  23436  subislly  23455  hausmapdom  23474  locfindis  23504  iskgen3  23523  kgencn  23530  ptpjpre1  23545  xkoccn  23593  txrest  23605  txlm  23622  txkgen  23626  xkopt  23629  xkoinjcn  23661  imasnopn  23664  imasncld  23665  imasncls  23666  qtopcn  23688  kqfeq  23698  isr0  23711  fbfinnfr  23815  trfbas  23818  fbunfip  23843  ufileu  23893  cfinufil  23902  fmid  23934  txflf  23980  fclsrest  23998  alexsubALT  24025  tsmsres  24118  ucnima  24254  fmucndlem  24264  bldisj  24372  xmeter  24407  elbl4  24537  restmetu  24544  dscopn  24547  bl2ioo  24766  isphtpc  24970  tcphcph  25213  lmmbr2  25235  lmmbrf  25238  iscau2  25253  iscauf  25256  caucfil  25259  metcld  25282  metcld2  25283  bcthlem1  25300  bcthlem4  25303  cldcss2  25418  ovolgelb  25456  ovoliunlem1  25478  ismbfcn  25605  mbfmax  25625  mbfimaopnlem  25631  i1faddlem  25669  i1fmullem  25670  i1fres  25681  i1fpos  25682  itg1climres  25690  xrge0f  25707  itgresr  25755  iblcnlem1  25764  limcun  25871  dvres  25887  mdegmullem  26055  r1pid2  26139  ply1remlem  26142  plyremlem  26283  vieta1  26291  ulmcau  26375  sineq0  26504  coseq1  26505  ang180lem3  26792  cubic  26830  atandm  26857  atandm2  26858  atandm3  26859  rlimcnp  26946  rlimcnp2  26947  vmappw  27097  dchrelbas3  27220  dchrelbas4  27225  dchrsum2  27250  bposlem6  27271  2sqreuopltb  27447  2sqreuopnnltb  27449  dchrisumlem3  27473  pntleml  27593  noetasuplem4  27719  noetainflem4  27723  rightge0  27832  addsrid  27975  negleft  28069  negright  28070  mulsrid  28124  mulsne0bd  28197  oniso  28282  om2noseqf1o  28312  zn0subs  28414  avglts1d  28464  avglts2d  28465  istrkg3ld  28548  tgcgr4  28618  lnrot2  28711  islnopp  28826  islmib  28874  mptelee  28982  brbtwn2  28993  axsegconlem6  29010  axsegcon  29015  ax5seg  29026  axpasch  29029  axeuclid  29051  axcontlem4  29055  elntg2  29073  issubgr  29359  nb3gr2nb  29472  uhgrvd00  29623  isrusgr0  29655  wlkcpr  29717  wlkcomp  29719  upgr2wlk  29755  upgrf1istrl  29790  clwlkcomp  29867  clwlkcompbp  29870  iswwlksnx  29928  wspthsnwspthsnon  30004  wspniunwspnon  30011  2pthon3v  30031  usgr2wspthons3  30055  usgr2wspthon  30056  rusgrnumwwlks  30065  clwlkclwwlklem3  30091  clwlkclwwlk  30092  clwwlknonwwlknonb  30196  0pth  30215  eupth2lem2  30309  vdgn1frgrv2  30386  fusgreg2wsp  30426  clwwlknonclwlknonf1o  30452  dlwwlknondlwlknonf1o  30455  wlkl0  30457  nmoolb  30862  nmlno0lem  30884  ubthlem1  30961  ocsh  31374  shle0  31533  eigrei  31925  adjeu  31980  nmoplb  31998  nmfnlb  32015  eleigvec2  32049  nmlnop0iALT  32086  cnlnadjlem5  32162  adjbdln  32174  jplem2  32360  cvbr2  32374  mdsl2bi  32414  chrelat3  32462  eqelbid  32564  sq2reunnltb  32574  rmounid  32584  nelpr  32621  disjunsn  32684  ofpreima  32758  funcnv5mpt  32760  dfcnv2  32768  suppiniseg  32779  gtiso  32794  fpwrelmap  32826  infxrge0glb  32858  xrdifh  32873  fzsplit3  32886  fzo0opth  32896  swrdrn3  33035  toslublem  33052  tosglblem  33054  mgcval  33067  mndlrinvb  33105  xrge0tsmsbi  33155  cntzun  33160  isarchi  33263  dvdsrspss  33467  rspsnasso  33468  lsmsnorb  33471  nsgqusf1olem2  33494  isprmidl  33518  ressply1mon1p  33648  r1pid2OLD  33689  constrfin  33911  smatrcl  33961  ist0cld  33998  rspectopn  34032  zarcls  34039  rhmpreimacnlem  34049  unitdivcld  34066  lmxrge0  34117  isrrext  34165  issibf  34498  eulerpartlemr  34539  eulerpartlemmf  34540  eulerpartlemn  34546  dstfrvunirn  34640  ballotlemfc0  34658  ballotlemfcc  34659  reprsuc  34780  reprpmtf1o  34791  reprdifc  34792  bnj919  34931  bnj976  34941  bnj1542  35020  bnj150  35039  bnj151  35040  bnj607  35079  bnj852  35084  bnj873  35087  bnj938  35100  bnj1171  35163  bnj1388  35196  bnj1489  35219  nummin  35257  usgrgt2cycl  35333  subfacp1lem3  35385  subfacp1lem5  35387  erdszelem9  35402  kur14  35419  iscvm  35462  satf0op  35580  mclsax  35772  rexxfr3dALT  35842  elintfv  35968  fundmpss  35970  opelco3  35978  dfon2  35993  dfbigcup2  36100  sscoid  36114  funpartfv  36148  dfrdg4  36154  cgr3permute3  36250  segletr  36317  segleantisym  36318  seglelin  36319  fneval  36555  neibastop3  36565  eltail  36577  filnetlem4  36584  bj-hbntbi  37014  bj-equsvt  37081  bj-sbceqgALT  37222  bj-clel3gALT  37368  bj-rest10  37413  bj-0int  37426  topdifinffinlem  37674  isbasisrelowllem1  37682  isbasisrelowllem2  37683  rdgeqoa  37697  finxpreclem4  37721  finxpsuclem  37724  wl-ifp4impr  37794  wl-1xor  37809  uncf  37931  phpreu  37936  cos2h  37943  tan2h  37944  matunitlindflem1  37948  poimirlem16  37968  poimirlem19  37971  poimirlem23  37975  poimirlem24  37976  poimirlem26  37978  poimirlem27  37979  mbfposadd  37999  cnambfre  38000  itg2addnclem  38003  itg2addnc  38006  iblabsnclem  38015  ftc1anclem1  38025  ftc1anclem5  38029  caures  38092  heiborlem3  38145  heiborlem10  38152  elghomOLD  38219  divrngidl  38360  eqrelf  38590  brvbrvvdif  38601  elrnres  38610  eldmres3  38615  eldmqsres2  38626  exanres  38633  relcnveq  38660  iss2  38676  ecinn0  38685  raldmqsmo  38695  brxrn2  38716  ecxrn  38738  ecxrn2  38740  disjressuc2  38743  elrelsrel  38774  eldmcoss2  38881  eldm1cossres  38882  elrelscnveq  38960  elcoeleqvrelsrel  39012  brredundsredund  39043  brdmqssqs  39063  cnvepresdmqss  39069  eldmqs1cossres  39076  brerser  39094  erimeq2  39095  eleldisjseldisj  39161  prtlem10  39322  prtlem16  39326  prtlem19  39335  prtex  39337  prter3  39339  islshpat  39474  lcvbr2  39479  lcvbr3  39480  lshpsmreu  39566  isat3  39764  hlrelat5N  39858  islpln5  39992  cdlemblem  40250  paddvaln0N  40258  paddval0  40267  cdlemefrs29bpre1  40854  cdlemefrs29cpre1  40855  cdlemg27b  41153  cdlemg33c  41165  cdlemg33e  41167  diaglbN  41512  cdlemm10N  41575  dicopelval2  41638  dicelval2N  41639  dihopelvalcpre  41705  dihglbcpreN  41757  dih1dimatlem  41786  dihatexv  41795  dvh4dimlem  41900  mapdpglem3  42132  hdmap14lem13  42337  hdmapglem7a  42384  eluzp1  42750  fsuppind  43034  isnacs2  43149  rabrenfdioph  43257  expdiophlem1  43464  pw2f1ocnv  43480  pwfi2f1o  43539  numinfctb  43546  dfacbasgrp  43551  islnr3  43558  onsupneqmaxlim0  43667  onsupnmax  43671  onsupuni  43672  tfsconcatrnss  43793  safesnsupfilb  43860  dfhe3  44217  clsk3nimkb  44482  ntrneiiso  44533  ntrneikb  44536  scottabf  44682  mnuunid  44719  hashnzfzclim  44764  dvconstbi  44776  sbcoreleleqVD  45300  trfr  45404  permac8prim  45456  rfcnpre3  45479  rfcnpre4  45480  r19.3rzf  45603  cncfshift  46317  stoweidlem59  46502  chnsubseqwl  47322  dfafv23  47698  nelbrnel  47721  elsetpreimafvrab  47851  iccpartiun  47891  prproropf1olem0  47959  prprelb  47973  prprspr2  47975  reuprpr  47980  oddm1evenALTV  48148  oddp1evenALTV  48149  oddprmne2  48188  fpprel  48201  dfvopnbgr2  48326  uhgrimisgrgric  48404  isgrlim  48455  gpg5nbgrvtx03starlem1  48541  gpg5nbgrvtx03starlem3  48543  gpg5nbgrvtx13starlem1  48544  gpg5nbgrvtx13starlem3  48546  iscmgmALT  48697  iscsgrpALT  48699  mofeu  49320  iscnrm3  49424  joindm2  49440  meetdm2  49442  oppcendc  49490  0funcg  49557  0funcALT  49560  istermc  49946  functermc2  49981  fulltermc  49983  elpglem2  50184