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  3615  eueq3  3667  sbceqal  3800  eqrrabd  4037  n0moeu  4310  sbcel12  4362  sbceqg  4363  sbcne12  4366  reldisj  4404  raldifeq  4445  r19.3rz  4448  ralf0  4465  eldifpr  4612  reusngf  4628  rexreusng  4633  eldiftp  4641  eqsndOLD  4784  reusv2lem5  5344  prelpw  5391  otthg  5430  2rbropap  5509  rabxp  5669  pwvrel  5671  ssrel3  5732  elrng  5838  iss  5991  idrefALT  6067  xpcan  6131  xpcan2  6132  dfpo2  6251  ordelpss  6342  fcnvres  6708  dffv3  6827  funimass4  6895  unima  6906  fndmdif  6984  fneqeql  6988  funimass3  6996  elrnrexdmb  7032  dff4  7043  fnsnbg  7107  fnsnbOLD  7109  fconst4  7157  elunirn  7194  f12dfv  7216  riota1  7333  riota2df  7335  f1ocnvfv3  7350  eqfnov  7484  elrnmpores  7493  caoftrn  7660  ordsucun  7764  dflim3  7786  dfom2  7807  peano5  7832  opiota  8000  frxp2  8083  xpord2pred  8084  xpord2indlem  8086  suppssr  8134  mpoxopovel  8159  brtpos  8174  rntpos  8178  ordgt0ge1  8417  ondif2  8426  oelim2  8519  omabs  8575  naddrid  8607  iiner  8722  erinxp  8724  qliftfun  8735  mapdm0  8775  ordunifi  9184  elfi2  9308  elfiun  9324  fifo  9326  noinfep  9560  cantnflem1  9589  cantnf  9593  rankonidlem  9731  r1pwALT  9749  cardalephex  9991  alephinit  9996  dfac5lem4OLD  10029  cflim2  10164  cfsmolem  10171  compssiso  10275  fin1a2lem11  10311  itunisuc  10320  axdclem  10420  brdom6disj  10433  alephreg  10483  fpwwe2lem8  10539  pwfseqlem3  10561  indpi  10808  nqereu  10830  ordpinq  10844  ltanq  10872  ltmnq  10873  suplem2pr  10954  map2psrpr  11011  ssxr  11192  leltne  11212  ltneg  11627  leneg  11630  suprnub  12097  negiso  12112  elnnnn0  12434  nn0sub  12441  fcdmnn0fsupp  12449  zrevaddcl  12527  znnsub  12528  znn0sub  12529  prime  12564  eluz2  12748  indstr  12824  eluz2b1  12827  qrevaddcl  12879  rpneg  12934  xrleltne  13054  dfle2  13056  dflt2  13057  supxrleub  13235  infxrgelb  13245  ixxin  13272  iccid  13300  elicopnf  13355  iccsplit  13395  fzsplit2  13459  fzsn  13476  fzpr  13489  uzsplit  13506  preduz  13560  fvinim0ffz  13699  injresinj  13701  om2uzf1oi  13870  lt2sqi  14106  le2sqi  14107  hashsdom  14298  hashf1lem1  14372  fz1isolem  14378  prprrab  14390  ccatlcan  14635  ccatrcan  14636  s3eq3seq  14856  2swrd2eqwrdeq  14870  trclfvcotr  14926  cnpart  15157  limsuplt  15396  rlimresb  15482  mertenslem2  15802  fprod2dlem  15897  sadadd2lem2  16371  saddisjlem  16385  bitsuz  16395  gcddiv  16472  algcvgblem  16498  isprm3  16604  isprm5  16628  prmreclem5  16842  vdwapun  16896  vdwmc2  16901  ramcl  16951  pwsle  17406  ismre  17502  mreacs  17574  acsfn  17575  iscatd2  17597  cidpropd  17626  dfiso2  17689  oppcsect2  17696  isfunc  17781  setcinv  18007  lubeldm  18267  lubval  18270  glbeldm  18280  glbval  18283  tosso  18333  ipodrsfi  18455  acsfiindd  18469  submgmacs  18635  imasmnd2  18692  ismhm0  18708  resmndismnd  18726  submacs  18745  imasgrp2  18978  issubg  19049  resgrpisgrp  19070  subgacs  19083  eqgval  19099  ghmqusnsglem1  19202  ghmquskerlem1  19205  gaorber  19230  symgfix2  19338  psgnran  19437  isslw  19530  sylow2alem2  19540  sylow2a  19541  sylow3lem6  19554  efgcpbllemb  19677  prmcyg  19816  gsum2d2lem  19895  gsumcom2  19897  subgdmdprd  19958  dprd2d2  19968  pgpfac1lem2  19999  pgpfac1lem4  20002  imasrng  20105  imasring  20258  isrnghmmul  20370  isnzr2  20443  isdomn3  20640  drngmulne0  20687  subrgacs  20725  sdrgacs  20726  lssle0  20893  lssacs  20910  lssats2  20943  lvecvsn0  21056  islpir  21275  zndvds  21496  znleval  21501  znleval2  21502  lindsmm  21775  islinds3  21781  islindf4  21785  ismhp3  22067  psdmul  22091  eltg2b  22884  discld  23014  opnssneib  23040  cldlp  23075  restbas  23083  leordtvallem1  23135  leordtvallem2  23136  ssidcn  23180  cnprest2  23215  lmss  23223  perfcls  23290  cmpfi  23333  1stccnp  23387  subislly  23406  hausmapdom  23425  locfindis  23455  iskgen3  23474  kgencn  23481  ptpjpre1  23496  xkoccn  23544  txrest  23556  txlm  23573  txkgen  23577  xkopt  23580  xkoinjcn  23612  imasnopn  23615  imasncld  23616  imasncls  23617  qtopcn  23639  kqfeq  23649  isr0  23662  fbfinnfr  23766  trfbas  23769  fbunfip  23794  ufileu  23844  cfinufil  23853  fmid  23885  txflf  23931  fclsrest  23949  alexsubALT  23976  tsmsres  24069  ucnima  24205  fmucndlem  24215  bldisj  24323  xmeter  24358  elbl4  24488  restmetu  24495  dscopn  24498  bl2ioo  24717  isphtpc  24930  tcphcph  25174  lmmbr2  25196  lmmbrf  25199  iscau2  25214  iscauf  25217  caucfil  25220  metcld  25243  metcld2  25244  bcthlem1  25261  bcthlem4  25264  cldcss2  25379  ovolgelb  25418  ovoliunlem1  25440  ismbfcn  25567  mbfmax  25587  mbfimaopnlem  25593  i1faddlem  25631  i1fmullem  25632  i1fres  25643  i1fpos  25644  itg1climres  25652  xrge0f  25669  itgresr  25717  iblcnlem1  25726  limcun  25833  dvres  25849  mdegmullem  26020  r1pid2  26104  ply1remlem  26107  plyremlem  26249  vieta1  26257  ulmcau  26341  sineq0  26470  coseq1  26471  ang180lem3  26758  cubic  26796  atandm  26823  atandm2  26824  atandm3  26825  rlimcnp  26912  rlimcnp2  26913  vmappw  27063  dchrelbas3  27186  dchrelbas4  27191  dchrsum2  27216  bposlem6  27237  2sqreuopltb  27413  2sqreuopnnltb  27415  dchrisumlem3  27439  pntleml  27559  noetasuplem4  27685  noetainflem4  27689  rightpos  27792  addsrid  27917  mulsrid  28062  mulsne0bd  28135  onsiso  28215  om2noseqf1o  28241  zn0subs  28337  avgslt1d  28386  avgslt2d  28387  istrkg3ld  28449  tgcgr4  28519  lnrot2  28612  islnopp  28727  islmib  28775  mptelee  28883  brbtwn2  28894  axsegconlem6  28911  axsegcon  28916  ax5seg  28927  axpasch  28930  axeuclid  28952  axcontlem4  28956  elntg2  28974  issubgr  29260  nb3gr2nb  29373  uhgrvd00  29524  isrusgr0  29556  wlkcpr  29618  wlkcomp  29620  upgr2wlk  29656  upgrf1istrl  29691  clwlkcomp  29768  clwlkcompbp  29771  iswwlksnx  29829  wspthsnwspthsnon  29905  wspniunwspnon  29912  2pthon3v  29932  usgr2wspthons3  29956  usgr2wspthon  29957  rusgrnumwwlks  29966  clwlkclwwlklem3  29992  clwlkclwwlk  29993  clwwlknonwwlknonb  30097  0pth  30116  eupth2lem2  30210  vdgn1frgrv2  30287  fusgreg2wsp  30327  clwwlknonclwlknonf1o  30353  dlwwlknondlwlknonf1o  30356  wlkl0  30358  nmoolb  30762  nmlno0lem  30784  ubthlem1  30861  ocsh  31274  shle0  31433  eigrei  31825  adjeu  31880  nmoplb  31898  nmfnlb  31915  eleigvec2  31949  nmlnop0iALT  31986  cnlnadjlem5  32062  adjbdln  32074  jplem2  32260  cvbr2  32274  mdsl2bi  32314  chrelat3  32362  eqelbid  32465  sq2reunnltb  32475  rmounid  32485  nelpr  32522  disjunsn  32585  ofpreima  32658  funcnvmpt  32660  funcnv5mpt  32661  dfcnv2  32669  suppiniseg  32678  gtiso  32693  fpwrelmap  32727  infxrge0glb  32759  xrdifh  32774  fzsplit3  32787  fzo0opth  32796  swrdrn3  32947  toslublem  32964  tosglblem  32966  mgcval  32979  mndlrinvb  33017  xrge0tsmsbi  33054  cntzun  33059  isarchi  33162  dvdsrspss  33363  rspsnasso  33364  lsmsnorb  33367  nsgqusf1olem2  33390  isprmidl  33414  ressply1mon1p  33542  r1pid2OLD  33580  constrfin  33770  smatrcl  33820  ist0cld  33857  rspectopn  33891  zarcls  33898  rhmpreimacnlem  33908  unitdivcld  33925  lmxrge0  33976  isrrext  34024  issibf  34357  eulerpartlemr  34398  eulerpartlemmf  34399  eulerpartlemn  34405  dstfrvunirn  34499  ballotlemfc0  34517  ballotlemfcc  34518  reprsuc  34639  reprpmtf1o  34650  reprdifc  34651  bnj919  34790  bnj976  34800  bnj1542  34880  bnj150  34899  bnj151  34900  bnj607  34939  bnj852  34944  bnj873  34947  bnj938  34960  bnj1171  35023  bnj1388  35056  bnj1489  35079  nummin  35115  usgrgt2cycl  35185  subfacp1lem3  35237  subfacp1lem5  35239  erdszelem9  35254  kur14  35271  iscvm  35314  satf0op  35432  mclsax  35624  rexxfr3dALT  35694  elintfv  35820  fundmpss  35822  opelco3  35830  dfon2  35845  dfbigcup2  35952  sscoid  35966  funpartfv  36000  dfrdg4  36006  cgr3permute3  36102  segletr  36169  segleantisym  36170  seglelin  36171  fneval  36407  neibastop3  36417  eltail  36429  filnetlem4  36436  bj-hbntbi  36759  bj-equsvt  36834  bj-sbceqgALT  36957  bj-clel3gALT  37103  bj-rest10  37143  bj-0int  37156  topdifinffinlem  37402  isbasisrelowllem1  37410  isbasisrelowllem2  37411  rdgeqoa  37425  finxpreclem4  37449  finxpsuclem  37452  wl-ifp4impr  37522  wl-1xor  37537  uncf  37649  phpreu  37654  cos2h  37661  tan2h  37662  matunitlindflem1  37666  poimirlem16  37686  poimirlem19  37689  poimirlem23  37693  poimirlem24  37694  poimirlem26  37696  poimirlem27  37697  mbfposadd  37717  cnambfre  37718  itg2addnclem  37721  itg2addnc  37724  iblabsnclem  37733  ftc1anclem1  37743  ftc1anclem5  37747  caures  37810  heiborlem3  37863  heiborlem10  37870  elghomOLD  37937  divrngidl  38078  eqrelf  38302  brvbrvvdif  38311  elrnres  38320  eldmres3  38325  eldmqsres2  38336  exanres  38343  relcnveq  38370  iss2  38386  ecinn0  38395  brxrn2  38418  ecxrn  38440  ecxrn2  38442  disjressuc2  38445  elrelsrel  38476  eldmcoss2  38571  eldm1cossres  38572  elrelscnveq  38650  elcoeleqvrelsrel  38702  brredundsredund  38733  brdmqssqs  38754  cnvepresdmqss  38760  eldmqs1cossres  38767  brerser  38785  erimeq2  38786  eleldisjseldisj  38837  prtlem10  38974  prtlem16  38978  prtlem19  38987  prtex  38989  prter3  38991  islshpat  39126  lcvbr2  39131  lcvbr3  39132  lshpsmreu  39218  isat3  39416  hlrelat5N  39510  islpln5  39644  cdlemblem  39902  paddvaln0N  39910  paddval0  39919  cdlemefrs29bpre1  40506  cdlemefrs29cpre1  40507  cdlemg27b  40805  cdlemg33c  40817  cdlemg33e  40819  diaglbN  41164  cdlemm10N  41227  dicopelval2  41290  dicelval2N  41291  dihopelvalcpre  41357  dihglbcpreN  41409  dih1dimatlem  41438  dihatexv  41447  dvh4dimlem  41552  mapdpglem3  41784  hdmap14lem13  41989  hdmapglem7a  42036  eluzp1  42415  fsuppind  42698  isnacs2  42813  rabrenfdioph  42921  expdiophlem1  43128  pw2f1ocnv  43144  pwfi2f1o  43203  numinfctb  43210  dfacbasgrp  43215  islnr3  43222  onsupneqmaxlim0  43331  onsupnmax  43335  onsupuni  43336  tfsconcatrnss  43457  safesnsupfilb  43525  dfhe3  43882  clsk3nimkb  44147  ntrneiiso  44198  ntrneikb  44201  scottabf  44347  mnuunid  44384  hashnzfzclim  44429  dvconstbi  44441  sbcoreleleqVD  44965  trfr  45069  permac8prim  45121  rfcnpre3  45144  rfcnpre4  45145  r19.3rzf  45269  cncfshift  45986  stoweidlem59  46171  chnsubseqwl  46991  dfafv23  47367  nelbrnel  47390  elsetpreimafvrab  47508  iccpartiun  47548  prproropf1olem0  47616  prprelb  47630  prprspr2  47632  reuprpr  47637  oddm1evenALTV  47789  oddp1evenALTV  47790  oddprmne2  47829  fpprel  47842  dfvopnbgr2  47967  uhgrimisgrgric  48045  isgrlim  48096  gpg5nbgrvtx03starlem1  48182  gpg5nbgrvtx03starlem3  48184  gpg5nbgrvtx13starlem1  48185  gpg5nbgrvtx13starlem3  48187  iscmgmALT  48338  iscsgrpALT  48340  mofeu  48962  iscnrm3  49066  joindm2  49082  meetdm2  49084  oppcendc  49133  0funcg  49200  0funcALT  49203  istermc  49589  functermc2  49624  fulltermc  49626  elpglem2  49827