Theorem bitr4di 292

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 227	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	bitrdi 290	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr4g  317  bibi2i  340  mtt  367  nbn2  373  ifptru  1091  3bior1fd  1506  3biant1d  1509  clel4g  3625  eueq3  3677  sbceqal  3808  eqrrabd  4043  n0moeu  4317  sbcel12  4379  sbceqg  4380  sbcne12  4383  reldisj  4416  raldifeq  4457  r19.3rz  4465  eldifpr  4627  reusngf  4643  rexreusng  4648  eldiftp  4656  reusv2lem5  5376  prelpw  5430  otthg  5470  2rbropap  5552  rabxp  5712  pwvrel  5714  ssrel3  5775  elrng  5884  iss  6040  idrefALT  6116  xpcan  6177  xpcan2  6178  dfpo2  6301  ordelpss  6392  fcnvres  6759  dffv3  6881  funimass4  6949  unima  6960  funcnvmpt  6995  fndmdif  7041  fneqeql  7045  funimass3  7053  elrnrexdmb  7089  dff4  7100  fnsnbg  7166  fnsnbOLD  7168  fconst4  7216  elunirn  7253  f12dfv  7275  riota1  7394  riota2df  7396  f1ocnvfv3  7411  eqfnov  7545  elrnmpores  7554  caoftrn  7721  ordsucun  7823  dflim3  7845  dfom2  7866  peano5  7892  opiota  8058  frxp2  8142  xpord2pred  8143  xpord2indlem  8145  suppssr  8193  mpoxopovel  8218  brtpos  8233  rntpos  8237  ordgt0ge1  8480  ondif2  8489  oelim2  8583  omabs  8639  naddrid  8672  iiner  8789  erinxp  8791  qliftfun  8802  mapdm0  8841  ordunifi  9252  elfi2  9376  elfiun  9392  fifo  9394  noinfep  9631  cantnflem1  9660  cantnf  9664  rankonidlem  9802  r1pwALT  9820  scottabf  9870  cardalephex  10085  alephinit  10090  cflim2  10257  cfsmolem  10264  compssiso  10368  fin1a2lem11  10404  itunisuc  10413  axdclem  10513  brdom6disj  10526  alephreg  10577  fpwwe2lem8  10633  pwfseqlem3  10655  indpi  10902  nqereu  10924  ordpinq  10938  ltanq  10966  ltmnq  10967  suplem2pr  11048  map2psrpr  11105  ssxr  11289  leltne  11309  ltneg  11724  leneg  11727  suprnub  12190  negiso  12205  elnnnn0  12557  nn0sub  12564  fcdmnn0fsupp  12572  zrevaddcl  12649  znnsub  12650  znn0sub  12651  prime  12687  eluz2  12878  indstr  12950  eluz2b1  12953  qrevaddcl  13005  rpneg  13060  xrleltne  13180  dfle2  13182  dflt2  13183  supxrleub  13362  infxrgelb  13372  ixxin  13399  iccid  13427  elicopnf  13482  iccsplit  13522  fzsplit2  13588  fzsn  13605  fzpr  13618  uzsplit  13635  preduz  13689  fvinim0ffz  13829  injresinj  13831  om2uzf1oi  14000  lt2sqi  14236  le2sqi  14237  hashsdom  14428  hashf1lem1  14503  fz1isolem  14509  prprrab  14521  ccatlcan  14766  ccatrcan  14767  s3eq3seq  14987  2swrd2eqwrdeq  15001  trclfvcotr  15057  cnpart  15302  limsuplt  15541  rlimresb  15627  mertenslem2  15950  fprod2dlem  16045  sadadd2lem2  16518  saddisjlem  16532  bitsuz  16542  gcddiv  16619  algcvgblem  16645  isprm3  16751  isprm5  16776  prmreclem5  16990  vdwapun  17044  vdwmc2  17049  ramcl  17099  pwsle  17556  ismre  17652  mreacs  17724  acsfn  17725  iscatd2  17747  cidpropd  17776  dfiso2  17839  oppcsect2  17846  isfunc  17931  setcinv  18157  lubeldm  18417  lubval  18420  glbeldm  18430  glbval  18433  tosso  18483  ipodrsfi  18605  acsfiindd  18619  submgmacs  18785  imasmnd2  18842  ismhm0  18858  resmndismnd  18876  submacs  18896  imasgrp2  19131  issubg  19202  resgrpisgrp  19224  subgacs  19237  eqgval  19255  ghmqusnsglem1  19360  ghmquskerlem1  19363  gaorber  19388  symgfix2  19496  psgnran  19595  isslw  19688  sylow2alem2  19698  sylow2a  19699  sylow3lem6  19712  efgcpbllemb  19835  prmcyg  19974  gsum2d2lem  20053  gsumcom2  20055  subgdmdprd  20116  dprd2d2  20126  pgpfac1lem2  20157  pgpfac1lem4  20160  imasrng  20265  imasring  20423  isrnghmmul  20535  isnzr2  20630  isdomn3  20828  drngmulne0  20880  subrgacs  20918  sdrgacs  20919  lssle0  21086  lssacs  21103  lssats2  21136  lvecvsn0  21248  rspsn0  21387  isprmidl  21478  islpir  21511  zndvds  21714  znleval  21719  znleval2  21720  lindsmm  21993  islinds3  21999  islindf4  22003  ismhp3  22320  psdmul  22344  eltg2b  23131  discld  23261  opnssneib  23287  cldlp  23322  restbas  23330  leordtvallem1  23382  leordtvallem2  23383  ssidcn  23427  cnprest2  23462  lmss  23470  perfcls  23537  cmpfi  23580  1stccnp  23634  subislly  23653  hausmapdom  23672  locfindis  23702  iskgen3  23721  kgencn  23728  ptpjpre1  23743  xkoccn  23791  txrest  23803  txlm  23820  txkgen  23824  xkopt  23827  xkoinjcn  23859  imasnopn  23862  imasncld  23863  imasncls  23864  qtopcn  23886  kqfeq  23896  isr0  23909  fbfinnfr  24013  trfbas  24016  fbunfip  24041  ufileu  24091  cfinufil  24100  fmid  24132  txflf  24178  fclsrest  24196  alexsubALT  24223  tsmsres  24316  ucnima  24452  fmucndlem  24462  bldisj  24570  xmeter  24605  elbl4  24735  restmetu  24742  dscopn  24745  bl2ioo  24964  isphtpc  25168  tcphcph  25411  lmmbr2  25433  lmmbrf  25436  iscau2  25451  iscauf  25454  caucfil  25457  metcld  25480  metcld2  25481  bcthlem1  25498  bcthlem4  25501  cldcss2  25616  ovolgelb  25654  ovoliunlem1  25676  ismbfcn  25803  mbfmax  25823  mbfimaopnlem  25829  i1faddlem  25867  i1fmullem  25868  i1fres  25879  i1fpos  25880  itg1climres  25888  xrge0f  25905  itgresr  25953  iblcnlem1  25962  limcun  26069  dvres  26085  mdegmullem  26250  r1pid2  26334  ply1remlem  26337  plyremlem  26480  vieta1  26488  ulmcau  26573  sineq0  26704  coseq1  26705  ang180lem3  26991  cubic  27029  atandm  27056  atandm2  27057  atandm3  27058  rlimcnp  27145  rlimcnp2  27146  vmappw  27295  dchrelbas3  27417  dchrelbas4  27422  dchrsum2  27447  bposlem6  27468  2sqreuopltb  27644  2sqreuopnnltb  27646  dchrisumlem3  27670  pntleml  27790  noetasuplem4  27915  noetainflem4  27919  rightge0  28029  addsrid  28172  negleft  28266  negright  28267  mulsrid  28321  mulsne0bd  28394  oniso  28479  om2noseqf1o  28509  zn0subs  28611  avglts1d  28661  avglts2d  28662  istrkg3ld  28745  tgcgr4  28815  lnrot2  28912  islnopp  29035  islmib  29111  mptelee  29259  brbtwn2  29270  axsegconlem6  29287  axsegcon  29292  ax5seg  29303  axpasch  29306  axeuclid  29328  axcontlem4  29332  elntg2  29350  issubgr  29636  nb3gr2nb  29749  uhgrvd00  29899  isrusgr0  29931  wlkcpr  29993  wlkcomp  29995  upgr2wlk  30031  upgrf1istrl  30066  clwlkcomp  30143  clwlkcompbp  30146  iswwlksnx  30204  wspthsnwspthsnon  30280  wspniunwspnon  30287  2pthon3v  30307  usgr2wspthons3  30331  usgr2wspthon  30332  rusgrnumwwlks  30341  clwlkclwwlklem3  30367  clwlkclwwlk  30368  clwwlknonwwlknonb  30472  0pth  30491  eupth2lem2  30585  vdgn1frgrv2  30662  fusgreg2wsp  30702  clwwlknonclwlknonf1o  30728  dlwwlknondlwlknonf1o  30731  wlkl0  30733  nmoolb  31138  nmlno0lem  31160  ubthlem1  31237  ocsh  31650  shle0  31809  eigrei  32201  adjeu  32256  nmoplb  32274  nmfnlb  32291  eleigvec2  32325  nmlnop0iALT  32362  cnlnadjlem5  32438  adjbdln  32450  jplem2  32636  cvbr2  32650  mdsl2bi  32690  chrelat3  32738  eqelbid  32836  sq2reunnltb  32846  rmounid  32856  nelpr  32892  disjunsn  32954  ofpreima  33025  funcnv5mpt  33027  dfcnv2  33035  suppiniseg  33046  gtiso  33061  fpwrelmap  33093  infxrge0glb  33125  xrdifh  33140  fzsplit3  33153  fzo0opth  33163  swrdrn3  33288  toslublem  33305  tosglblem  33307  mgcval  33320  mndlrinvb  33358  xrge0tsmsbi  33407  cntzun  33412  isarchi  33515  dvdsrspss  33713  rspsnasso  33714  lsmsnorb  33717  nsgqusf1olem2  33736  ressply1mon1p  33871  constrfin  34149  smatrcl  34199  ist0cld  34236  rspectopn  34270  zarcls  34277  rhmpreimacnlem  34287  unitdivcld  34304  lmxrge0  34355  isrrext  34403  issibf  34736  eulerpartlemr  34777  eulerpartlemmf  34778  eulerpartlemn  34784  dstfrvunirn  34878  ballotlemfc0  34896  ballotlemfcc  34897  reprsuc  35015  reprpmtf1o  35026  reprdifc  35027  bnj919  35169  bnj976  35179  bnj1542  35258  bnj150  35277  bnj151  35278  bnj607  35317  bnj852  35322  bnj873  35325  bnj938  35338  bnj1171  35401  bnj1388  35434  bnj1489  35457  nummin  35497  dfscott3  35525  usgrgt2cycl  35634  subfacp1lem3  35686  subfacp1lem5  35688  erdszelem9  35703  kur14  35720  iscvm  35763  satf0op  35881  mclsax  36073  rexxfr3dALT  36143  elintfv  36269  fundmpss  36271  opelco3  36279  dfon2  36294  dfbigcup2  36401  sscoid  36415  funpartfv  36449  dfrdg4  36455  cgr3permute3  36551  segletr  36618  segleantisym  36619  seglelin  36620  nmulrid  36701  fneval  36895  neibastop3  36905  eltail  36917  filnetlem4  36924  mh-infprim2bi  37090  bj-hbntbi  37361  bj-equsvt  37428  bj-sbceqgALT  37569  bj-clel3gALT  37716  bj-rest10  37762  bj-0int  37775  qdiffALT  38004  topdifinffinlem  38025  isbasisrelowllem1  38033  isbasisrelowllem2  38034  rdgeqoa  38048  finxpreclem4  38072  finxpsuclem  38075  wl-ifp4impr  38145  wl-1xor  38160  uncf  38282  phpreu  38287  cos2h  38294  tan2h  38295  matunitlindflem1  38299  poimirlem16  38319  poimirlem19  38322  poimirlem23  38326  poimirlem24  38327  poimirlem26  38329  poimirlem27  38330  mbfposadd  38350  cnambfre  38351  itg2addnclem  38354  itg2addnc  38357  iblabsnclem  38366  ftc1anclem1  38376  ftc1anclem5  38380  caures  38443  heiborlem3  38496  heiborlem10  38503  elghomOLD  38570  divrngidl  38711  eqrelf  38939  brvbrvvdif  38950  elrnres  38959  eldmres3  38964  eldmqsres2  38975  exanres  38982  relcnveq  39009  iss2  39025  ecinn0  39034  raldmqsmo  39044  brxrn2  39065  ecxrn  39087  ecxrn2  39089  disjressuc2  39092  elrelsrel  39123  eldmcoss2  39230  eldm1cossres  39231  elrelscnveq  39309  elcoeleqvrelsrel  39361  brredundsredund  39392  brdmqssqs  39412  cnvepresdmqss  39418  eldmqs1cossres  39425  brerser  39443  erimeq2  39444  eleldisjseldisj  39510  prtlem10  39671  prtlem16  39675  prtlem19  39684  prtex  39686  prter3  39688  islshpat  39823  lcvbr2  39828  lcvbr3  39829  lshpsmreu  39915  isat3  40113  hlrelat5N  40207  islpln5  40341  cdlemblem  40599  paddvaln0N  40607  paddval0  40616  cdlemefrs29bpre1  41203  cdlemefrs29cpre1  41204  cdlemg27b  41502  cdlemg33c  41514  cdlemg33e  41516  diaglbN  41861  cdlemm10N  41924  dicopelval2  41987  dicelval2N  41988  dihopelvalcpre  42054  dihglbcpreN  42106  dih1dimatlem  42135  dihatexv  42144  dvh4dimlem  42249  mapdpglem3  42481  hdmap14lem13  42686  hdmapglem7a  42733  eluzp1  43100  fsuppind  43354  isnacs2  43469  rabrenfdioph  43573  expdiophlem1  43780  pw2f1ocnv  43796  pwfi2f1o  43855  numinfctb  43862  dfacbasgrp  43867  islnr3  43874  onsupneqmaxlim0  43983  onsupnmax  43987  onsupuni  43988  tfsconcatrnss  44109  safesnsupfilb  44176  dfhe3  44533  clsk3nimkb  44798  ntrneiiso  44849  ntrneikb  44852  mnuunid  45019  hashnzfzclim  45064  dvconstbi  45076  sbcoreleleqVD  45599  trfr  45703  permac8prim  45755  rfcnpre3  45785  rfcnpre4  45786  r19.3rzf  45908  cncfshift  46620  stoweidlem59  46805  chnsubseqwl  47627  dfafv23  48022  nelbrnel  48045  elsetpreimafvrab  48175  iccpartiun  48215  prproropf1olem0  48283  prprelb  48297  prprspr2  48299  reuprpr  48304  oddm1evenALTV  48472  oddp1evenALTV  48473  oddprmne2  48512  fpprel  48525  dfvopnbgr2  48650  uhgrimisgrgric  48728  isgrlim  48779  gpg5nbgrvtx03starlem1  48865  gpg5nbgrvtx03starlem3  48867  gpg5nbgrvtx13starlem1  48868  gpg5nbgrvtx13starlem3  48870  iscmgmALT  49021  iscsgrpALT  49023  mofeu  49658  iscnrm3  49762  joindm2  49778  meetdm2  49780  oppcendc  49828  0funcg  49895  0funcALT  49898  istermc  50284  functermc2  50319  fulltermc  50321  elpglem2  50522