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  1474  3biant1d  1477  clel4g  3662  eueq3  3719  sbceqal  3856  eqrrabd  4095  n0moeu  4364  sbcel12  4416  sbceqg  4417  sbcne12  4420  reldisj  4458  raldifeq  4499  r19.3rz  4502  ralf0  4519  eldifpr  4662  reusngf  4678  rexreusng  4683  eldiftp  4691  eqsndOLD  4835  reusv2lem5  5407  prelpw  5456  otthg  5495  2rbropap  5575  rabxp  5736  pwvrel  5738  ssrel3  5798  elrng  5904  iss  6054  idrefALT  6133  xpcan  6197  xpcan2  6198  dfpo2  6317  ordelpss  6413  fcnvres  6785  dffv3  6902  funimass4  6972  unima  6983  fndmdif  7061  fneqeql  7065  funimass3  7073  elrnrexdmb  7109  dff4  7120  fnsnb  7185  fconst4  7233  elunirn  7270  f12dfv  7292  riota1  7408  riota2df  7410  f1ocnvfv3  7425  eqfnov  7561  elrnmpores  7570  caoftrn  7736  ordsucun  7844  dflim3  7867  dfom2  7888  peano5  7915  opiota  8082  frxp2  8167  xpord2pred  8168  xpord2indlem  8170  suppssr  8218  mpoxopovel  8243  brtpos  8258  rntpos  8262  ordgt0ge1  8529  ondif2  8538  oelim2  8631  omabs  8687  naddrid  8719  iiner  8827  erinxp  8829  qliftfun  8840  mapdm0  8880  ordunifi  9323  elfi2  9451  elfiun  9467  fifo  9469  noinfep  9697  cantnflem1  9726  cantnf  9730  rankonidlem  9865  r1pwALT  9883  pr2nelemOLD  10040  cardalephex  10127  alephinit  10132  dfac5lem4OLD  10165  cflim2  10300  cfsmolem  10307  compssiso  10411  fin1a2lem11  10447  itunisuc  10456  axdclem  10556  brdom6disj  10569  alephreg  10619  fpwwe2lem8  10675  pwfseqlem3  10697  indpi  10944  nqereu  10966  ordpinq  10980  ltanq  11008  ltmnq  11009  suplem2pr  11090  map2psrpr  11147  ssxr  11327  leltne  11347  ltneg  11760  leneg  11763  suprnub  12230  negiso  12245  elnnnn0  12566  nn0sub  12573  fcdmnn0fsupp  12581  zrevaddcl  12659  znnsub  12660  znn0sub  12661  prime  12696  eluz2  12881  indstr  12955  eluz2b1  12958  qrevaddcl  13010  rpneg  13064  xrleltne  13183  dfle2  13185  dflt2  13186  supxrleub  13364  infxrgelb  13373  ixxin  13400  iccid  13428  elicopnf  13481  iccsplit  13521  fzsplit2  13585  fzsn  13602  fzpr  13615  uzsplit  13632  preduz  13686  fvinim0ffz  13821  injresinj  13823  om2uzf1oi  13990  lt2sqi  14224  le2sqi  14225  hashsdom  14416  hashf1lem1  14490  fz1isolem  14496  prprrab  14508  ccatlcan  14752  ccatrcan  14753  s3eq3seq  14974  2swrd2eqwrdeq  14988  trclfvcotr  15044  cnpart  15275  limsuplt  15511  rlimresb  15597  mertenslem2  15917  fprod2dlem  16012  sadadd2lem2  16483  saddisjlem  16497  bitsuz  16507  gcddiv  16584  algcvgblem  16610  isprm3  16716  isprm5  16740  prmreclem5  16953  vdwapun  17007  vdwmc2  17012  ramcl  17062  pwsle  17538  ismre  17634  mreacs  17702  acsfn  17703  iscatd2  17725  cidpropd  17754  dfiso2  17819  oppcsect2  17826  isfunc  17914  setcinv  18143  lubeldm  18410  lubval  18413  glbeldm  18423  glbval  18426  tosso  18476  ipodrsfi  18596  acsfiindd  18610  submgmacs  18742  imasmnd2  18799  ismhm0  18815  resmndismnd  18833  submacs  18852  imasgrp2  19085  issubg  19156  resgrpisgrp  19177  subgacs  19191  eqgval  19207  ghmqusnsglem1  19310  ghmquskerlem1  19313  gaorber  19338  symgfix2  19448  psgnran  19547  isslw  19640  sylow2alem2  19650  sylow2a  19651  sylow3lem6  19664  efgcpbllemb  19787  prmcyg  19926  gsum2d2lem  20005  gsumcom2  20007  subgdmdprd  20068  dprd2d2  20078  pgpfac1lem2  20109  pgpfac1lem4  20112  imasrng  20194  imasring  20343  isrnghmmul  20458  isnzr2  20534  isdomn3  20731  drngmulne0  20778  subrgacs  20817  sdrgacs  20818  lssle0  20965  lssacs  20982  lssats2  21015  lvecvsn0  21128  islpir  21355  zndvds  21585  znleval  21590  znleval2  21591  lindsmm  21865  islinds3  21871  islindf4  21875  ismhp3  22163  psdmul  22187  eltg2b  22981  discld  23112  opnssneib  23138  cldlp  23173  restbas  23181  leordtvallem1  23233  leordtvallem2  23234  ssidcn  23278  cnprest2  23313  lmss  23321  perfcls  23388  cmpfi  23431  1stccnp  23485  subislly  23504  hausmapdom  23523  locfindis  23553  iskgen3  23572  kgencn  23579  ptpjpre1  23594  xkoccn  23642  txrest  23654  txlm  23671  txkgen  23675  xkopt  23678  xkoinjcn  23710  imasnopn  23713  imasncld  23714  imasncls  23715  qtopcn  23737  kqfeq  23747  isr0  23760  fbfinnfr  23864  trfbas  23867  fbunfip  23892  ufileu  23942  cfinufil  23951  fmid  23983  txflf  24029  fclsrest  24047  alexsubALT  24074  tsmsres  24167  ucnima  24305  fmucndlem  24315  bldisj  24423  xmeter  24458  elbl4  24591  restmetu  24598  dscopn  24601  bl2ioo  24827  isphtpc  25039  tcphcph  25284  lmmbr2  25306  lmmbrf  25309  iscau2  25324  iscauf  25327  caucfil  25330  metcld  25353  metcld2  25354  bcthlem1  25371  bcthlem4  25374  cldcss2  25489  ovolgelb  25528  ovoliunlem1  25550  ismbfcn  25677  mbfmax  25697  mbfimaopnlem  25703  i1faddlem  25741  i1fmullem  25742  i1fres  25754  i1fpos  25755  itg1climres  25763  xrge0f  25780  itgresr  25828  iblcnlem1  25837  limcun  25944  dvres  25960  mdegmullem  26131  r1pid2  26215  ply1remlem  26218  plyremlem  26360  vieta1  26368  ulmcau  26452  sineq0  26580  coseq1  26581  ang180lem3  26868  cubic  26906  atandm  26933  atandm2  26934  atandm3  26935  rlimcnp  27022  rlimcnp2  27023  vmappw  27173  dchrelbas3  27296  dchrelbas4  27301  dchrsum2  27326  bposlem6  27347  2sqreuopltb  27523  2sqreuopnnltb  27525  dchrisumlem3  27549  pntleml  27669  noetasuplem4  27795  noetainflem4  27799  addsrid  28011  mulsrid  28153  mulsne0bd  28226  om2noseqf1o  28321  zn0subs  28403  istrkg3ld  28483  tgcgr4  28553  lnrot2  28646  islnopp  28761  islmib  28809  brbtwn2  28934  axsegconlem6  28951  axsegcon  28956  ax5seg  28967  axpasch  28970  axeuclid  28992  axcontlem4  28996  elntg2  29014  issubgr  29302  nb3gr2nb  29415  uhgrvd00  29566  isrusgr0  29598  wlkcpr  29661  wlkcomp  29663  upgr2wlk  29700  upgrf1istrl  29735  clwlkcomp  29811  clwlkcompbp  29814  iswwlksnx  29869  wspthsnwspthsnon  29945  wspniunwspnon  29952  2pthon3v  29972  usgr2wspthons3  29993  usgr2wspthon  29994  rusgrnumwwlks  30003  clwlkclwwlklem3  30029  clwlkclwwlk  30030  clwwlknonwwlknonb  30134  0pth  30153  eupth2lem2  30247  vdgn1frgrv2  30324  fusgreg2wsp  30364  clwwlknonclwlknonf1o  30390  dlwwlknondlwlknonf1o  30393  wlkl0  30395  nmoolb  30799  nmlno0lem  30821  ubthlem1  30898  ocsh  31311  shle0  31470  eigrei  31862  adjeu  31917  nmoplb  31935  nmfnlb  31952  eleigvec2  31986  nmlnop0iALT  32023  cnlnadjlem5  32099  adjbdln  32111  jplem2  32297  cvbr2  32311  mdsl2bi  32351  chrelat3  32399  eqelbid  32502  sq2reunnltb  32512  rmounid  32522  nelpr  32556  disjunsn  32613  ofpreima  32681  funcnvmpt  32683  funcnv5mpt  32684  dfcnv2  32692  suppiniseg  32700  gtiso  32715  fpwrelmap  32750  infxrge0glb  32775  xrdifh  32788  fzsplit3  32801  fzo0opth  32812  swrdrn3  32924  toslublem  32946  tosglblem  32948  mgcval  32961  mndlrinvb  33012  xrge0tsmsbi  33048  cntzun  33053  isarchi  33171  dvdsrspss  33394  rspsnasso  33395  lsmsnorb  33398  nsgqusf1olem2  33421  isprmidl  33445  ressply1mon1p  33572  r1pid2OLD  33608  constrfin  33750  smatrcl  33756  ist0cld  33793  rspectopn  33827  zarcls  33834  rhmpreimacnlem  33844  unitdivcld  33861  lmxrge0  33912  isrrext  33962  issibf  34314  eulerpartlemr  34355  eulerpartlemmf  34356  eulerpartlemn  34362  dstfrvunirn  34455  ballotlemfc0  34473  ballotlemfcc  34474  reprsuc  34608  reprpmtf1o  34619  reprdifc  34620  bnj919  34759  bnj976  34769  bnj1542  34849  bnj150  34868  bnj151  34869  bnj607  34908  bnj852  34913  bnj873  34916  bnj938  34929  bnj1171  34992  bnj1388  35025  bnj1489  35048  nummin  35083  usgrgt2cycl  35114  subfacp1lem3  35166  subfacp1lem5  35168  erdszelem9  35183  kur14  35200  iscvm  35243  satf0op  35361  mclsax  35553  rexxfr3dALT  35623  elintfv  35745  fundmpss  35747  opelco3  35755  dfon2  35773  dfbigcup2  35880  sscoid  35894  funpartfv  35926  dfrdg4  35932  cgr3permute3  36028  segletr  36095  segleantisym  36096  seglelin  36097  fneval  36334  neibastop3  36344  eltail  36356  filnetlem4  36363  bj-hbntbi  36686  bj-equsvt  36761  bj-sbceqgALT  36884  bj-clel3gALT  37030  bj-rest10  37070  bj-0int  37083  topdifinffinlem  37329  isbasisrelowllem1  37337  isbasisrelowllem2  37338  rdgeqoa  37352  finxpreclem4  37376  finxpsuclem  37379  wl-ifp4impr  37449  wl-1xor  37464  uncf  37585  phpreu  37590  cos2h  37597  tan2h  37598  matunitlindflem1  37602  poimirlem16  37622  poimirlem19  37625  poimirlem23  37629  poimirlem24  37630  poimirlem26  37632  poimirlem27  37633  mbfposadd  37653  cnambfre  37654  itg2addnclem  37657  itg2addnc  37660  iblabsnclem  37669  ftc1anclem1  37679  ftc1anclem5  37683  caures  37746  heiborlem3  37799  heiborlem10  37806  elghomOLD  37873  divrngidl  38014  eqrelf  38236  brvbrvvdif  38245  elrnres  38252  eldmqsres2  38269  exanres  38276  relcnveq  38303  iss2  38325  ecinn0  38334  brxrn2  38356  ecxrn  38368  disjressuc2  38369  eldmcoss2  38440  eldm1cossres  38441  elrelsrel  38468  elrelscnveq  38473  elcoeleqvrelsrel  38577  brredundsredund  38608  brdmqssqs  38628  cnvepresdmqss  38633  eldmqs1cossres  38640  brerser  38658  erimeq2  38659  eleldisjseldisj  38710  prtlem10  38846  prtlem16  38850  prtlem19  38859  prtex  38861  prter3  38863  islshpat  38998  lcvbr2  39003  lcvbr3  39004  lshpsmreu  39090  isat3  39288  hlrelat5N  39383  islpln5  39517  cdlemblem  39775  paddvaln0N  39783  paddval0  39792  cdlemefrs29bpre1  40379  cdlemefrs29cpre1  40380  cdlemg27b  40678  cdlemg33c  40690  cdlemg33e  40692  diaglbN  41037  cdlemm10N  41100  dicopelval2  41163  dicelval2N  41164  dihopelvalcpre  41230  dihglbcpreN  41282  dih1dimatlem  41311  dihatexv  41320  dvh4dimlem  41425  mapdpglem3  41657  hdmap14lem13  41862  hdmapglem7a  41909  fnsnbt  42249  eluzp1  42319  fsuppind  42576  isnacs2  42693  rabrenfdioph  42801  expdiophlem1  43009  pw2f1ocnv  43025  pwfi2f1o  43084  numinfctb  43091  dfacbasgrp  43096  islnr3  43103  onsupneqmaxlim0  43212  onsupnmax  43216  onsupuni  43217  tfsconcatrnss  43339  safesnsupfilb  43407  dfhe3  43764  clsk3nimkb  44029  ntrneiiso  44080  ntrneikb  44083  scottabf  44235  mnuunid  44272  hashnzfzclim  44317  dvconstbi  44329  sbcoreleleqVD  44856  rfcnpre3  44970  rfcnpre4  44971  r19.3rzf  45100  cncfshift  45829  stoweidlem59  46014  dfafv23  47202  nelbrnel  47225  elsetpreimafvrab  47318  iccpartiun  47358  prproropf1olem0  47426  prprelb  47440  prprspr2  47442  reuprpr  47447  oddm1evenALTV  47599  oddp1evenALTV  47600  oddprmne2  47639  fpprel  47652  dfvopnbgr2  47776  uhgrimisgrgric  47836  isgrlim  47884  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem3  47963  iscmgmALT  48067  iscsgrpALT  48069  mofeu  48677  iscnrm3  48748  joindm2  48764  meetdm2  48766  elpglem2  48942