Theorem bitr4di 291

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3bitr4g  316  bibi2i  339  mtt  366  nbn2  372  ifptru  1083  3bior1fd  1490  3biant1d  1493  clel4g  3617  eueq3  3668  sbceqal  3800  eqrrabd  4034  n0moeu  4306  sbcel12  4359  sbceqg  4360  sbcne12  4363  reldisj  4401  raldifeq  4441  r19.3rz  4449  eldifpr  4611  reusngf  4627  rexreusng  4632  eldiftp  4640  eqsndOLD  4783  reusv2lem5  5353  prelpw  5407  otthg  5447  2rbropap  5528  rabxp  5688  pwvrel  5690  ssrel3  5751  elrng  5860  iss  6014  idrefALT  6090  xpcan  6151  xpcan2  6152  dfpo2  6272  ordelpss  6363  fcnvres  6730  dffv3  6852  funimass4  6920  unima  6931  funcnvmpt  6966  fndmdif  7012  fneqeql  7016  funimass3  7024  elrnrexdmb  7060  dff4  7071  fnsnbg  7137  fnsnbOLD  7139  fconst4  7187  elunirn  7224  f12dfv  7246  riota1  7363  riota2df  7365  f1ocnvfv3  7380  eqfnov  7514  elrnmpores  7523  caoftrn  7690  ordsucun  7794  dflim3  7816  dfom2  7837  peano5  7863  opiota  8029  frxp2  8112  xpord2pred  8113  xpord2indlem  8115  suppssr  8163  mpoxopovel  8188  brtpos  8203  rntpos  8207  ordgt0ge1  8450  ondif2  8459  oelim2  8553  omabs  8609  naddrid  8642  iiner  8759  erinxp  8761  qliftfun  8772  mapdm0  8812  ordunifi  9223  elfi2  9350  elfiun  9366  fifo  9368  noinfep  9605  cantnflem1  9634  cantnf  9638  rankonidlem  9776  r1pwALT  9794  cardalephex  10036  alephinit  10041  dfac5lem4OLD  10074  cflim2  10210  cfsmolem  10217  compssiso  10321  fin1a2lem11  10357  itunisuc  10366  axdclem  10466  brdom6disj  10479  alephreg  10530  fpwwe2lem8  10586  pwfseqlem3  10608  indpi  10855  nqereu  10877  ordpinq  10891  ltanq  10919  ltmnq  10920  suplem2pr  11001  map2psrpr  11058  ssxr  11242  leltne  11262  ltneg  11677  leneg  11680  suprnub  12147  negiso  12162  elnnnn0  12514  nn0sub  12521  fcdmnn0fsupp  12529  zrevaddcl  12606  znnsub  12607  znn0sub  12608  prime  12644  eluz2  12835  indstr  12907  eluz2b1  12910  qrevaddcl  12962  rpneg  13017  xrleltne  13137  dfle2  13139  dflt2  13140  supxrleub  13319  infxrgelb  13329  ixxin  13356  iccid  13384  elicopnf  13439  iccsplit  13479  fzsplit2  13544  fzsn  13561  fzpr  13574  uzsplit  13591  preduz  13645  fvinim0ffz  13785  injresinj  13787  om2uzf1oi  13956  lt2sqi  14192  le2sqi  14193  hashsdom  14384  hashf1lem1  14458  fz1isolem  14464  prprrab  14476  ccatlcan  14721  ccatrcan  14722  s3eq3seq  14942  2swrd2eqwrdeq  14956  trclfvcotr  15012  cnpart  15243  limsuplt  15482  rlimresb  15568  mertenslem2  15891  fprod2dlem  15986  sadadd2lem2  16460  saddisjlem  16474  bitsuz  16484  gcddiv  16561  algcvgblem  16587  isprm3  16693  isprm5  16718  prmreclem5  16932  vdwapun  16986  vdwmc2  16991  ramcl  17041  pwsle  17498  ismre  17594  mreacs  17666  acsfn  17667  iscatd2  17689  cidpropd  17718  dfiso2  17781  oppcsect2  17788  isfunc  17873  setcinv  18099  lubeldm  18359  lubval  18362  glbeldm  18372  glbval  18375  tosso  18425  ipodrsfi  18547  acsfiindd  18561  submgmacs  18727  imasmnd2  18784  ismhm0  18800  resmndismnd  18818  submacs  18837  imasgrp2  19073  issubg  19144  resgrpisgrp  19165  subgacs  19178  eqgval  19194  ghmqusnsglem1  19296  ghmquskerlem1  19299  gaorber  19324  symgfix2  19432  psgnran  19531  isslw  19624  sylow2alem2  19634  sylow2a  19635  sylow3lem6  19648  efgcpbllemb  19771  prmcyg  19910  gsum2d2lem  19989  gsumcom2  19991  subgdmdprd  20052  dprd2d2  20062  pgpfac1lem2  20093  pgpfac1lem4  20096  imasrng  20199  imasring  20351  isrnghmmul  20463  isnzr2  20540  isdomn3  20737  drngmulne0  20784  subrgacs  20822  sdrgacs  20823  lssle0  20990  lssacs  21007  lssats2  21040  lvecvsn0  21152  islpir  21371  zndvds  21574  znleval  21579  znleval2  21580  lindsmm  21853  islinds3  21859  islindf4  21863  ismhp3  22180  psdmul  22204  eltg2b  22992  discld  23122  opnssneib  23148  cldlp  23183  restbas  23191  leordtvallem1  23243  leordtvallem2  23244  ssidcn  23288  cnprest2  23323  lmss  23331  perfcls  23398  cmpfi  23441  1stccnp  23495  subislly  23514  hausmapdom  23533  locfindis  23563  iskgen3  23582  kgencn  23589  ptpjpre1  23604  xkoccn  23652  txrest  23664  txlm  23681  txkgen  23685  xkopt  23688  xkoinjcn  23720  imasnopn  23723  imasncld  23724  imasncls  23725  qtopcn  23747  kqfeq  23757  isr0  23770  fbfinnfr  23874  trfbas  23877  fbunfip  23902  ufileu  23952  cfinufil  23961  fmid  23993  txflf  24039  fclsrest  24057  alexsubALT  24084  tsmsres  24177  ucnima  24313  fmucndlem  24323  bldisj  24431  xmeter  24466  elbl4  24596  restmetu  24603  dscopn  24606  bl2ioo  24825  isphtpc  25029  tcphcph  25272  lmmbr2  25294  lmmbrf  25297  iscau2  25312  iscauf  25315  caucfil  25318  metcld  25341  metcld2  25342  bcthlem1  25359  bcthlem4  25362  cldcss2  25477  ovolgelb  25515  ovoliunlem1  25537  ismbfcn  25664  mbfmax  25684  mbfimaopnlem  25690  i1faddlem  25728  i1fmullem  25729  i1fres  25740  i1fpos  25741  itg1climres  25749  xrge0f  25766  itgresr  25814  iblcnlem1  25823  limcun  25930  dvres  25946  mdegmullem  26111  r1pid2  26195  ply1remlem  26198  plyremlem  26338  vieta1  26346  ulmcau  26428  sineq0  26559  coseq1  26560  ang180lem3  26846  cubic  26884  atandm  26911  atandm2  26912  atandm3  26913  rlimcnp  27000  rlimcnp2  27001  vmappw  27150  dchrelbas3  27272  dchrelbas4  27277  dchrsum2  27302  bposlem6  27323  2sqreuopltb  27499  2sqreuopnnltb  27501  dchrisumlem3  27525  pntleml  27645  noetasuplem4  27770  noetainflem4  27774  rightge0  27884  addsrid  28027  negleft  28121  negright  28122  mulsrid  28176  mulsne0bd  28249  oniso  28334  om2noseqf1o  28364  zn0subs  28466  avglts1d  28516  avglts2d  28517  istrkg3ld  28600  tgcgr4  28670  lnrot2  28763  islnopp  28878  islmib  28926  mptelee  29034  brbtwn2  29045  axsegconlem6  29062  axsegcon  29067  ax5seg  29078  axpasch  29081  axeuclid  29103  axcontlem4  29107  elntg2  29125  issubgr  29411  nb3gr2nb  29524  uhgrvd00  29674  isrusgr0  29706  wlkcpr  29768  wlkcomp  29770  upgr2wlk  29806  upgrf1istrl  29841  clwlkcomp  29918  clwlkcompbp  29921  iswwlksnx  29979  wspthsnwspthsnon  30055  wspniunwspnon  30062  2pthon3v  30082  usgr2wspthons3  30106  usgr2wspthon  30107  rusgrnumwwlks  30116  clwlkclwwlklem3  30142  clwlkclwwlk  30143  clwwlknonwwlknonb  30247  0pth  30266  eupth2lem2  30360  vdgn1frgrv2  30437  fusgreg2wsp  30477  clwwlknonclwlknonf1o  30503  dlwwlknondlwlknonf1o  30506  wlkl0  30508  nmoolb  30913  nmlno0lem  30935  ubthlem1  31012  ocsh  31425  shle0  31584  eigrei  31976  adjeu  32031  nmoplb  32049  nmfnlb  32066  eleigvec2  32100  nmlnop0iALT  32137  cnlnadjlem5  32213  adjbdln  32225  jplem2  32411  cvbr2  32425  mdsl2bi  32465  chrelat3  32513  eqelbid  32615  sq2reunnltb  32625  rmounid  32635  nelpr  32672  disjunsn  32736  ofpreima  32810  funcnv5mpt  32812  dfcnv2  32820  suppiniseg  32831  gtiso  32846  fpwrelmap  32878  infxrge0glb  32910  xrdifh  32925  fzsplit3  32938  fzo0opth  32948  swrdrn3  33087  toslublem  33104  tosglblem  33106  mgcval  33119  mndlrinvb  33157  xrge0tsmsbi  33208  cntzun  33213  isarchi  33316  dvdsrspss  33527  rspsnasso  33528  lsmsnorb  33531  nsgqusf1olem2  33554  isprmidl  33578  ressply1mon1p  33718  r1pid2OLD  33759  constrfin  33997  smatrcl  34047  ist0cld  34084  rspectopn  34118  zarcls  34125  rhmpreimacnlem  34135  unitdivcld  34152  lmxrge0  34203  isrrext  34251  issibf  34584  eulerpartlemr  34625  eulerpartlemmf  34626  eulerpartlemn  34632  dstfrvunirn  34726  ballotlemfc0  34744  ballotlemfcc  34745  reprsuc  34866  reprpmtf1o  34877  reprdifc  34878  bnj919  35020  bnj976  35030  bnj1542  35109  bnj150  35128  bnj151  35129  bnj607  35168  bnj852  35173  bnj873  35176  bnj938  35189  bnj1171  35252  bnj1388  35285  bnj1489  35308  nummin  35344  usgrgt2cycl  35428  subfacp1lem3  35480  subfacp1lem5  35482  erdszelem9  35497  kur14  35514  iscvm  35557  satf0op  35675  mclsax  35867  rexxfr3dALT  35937  elintfv  36063  fundmpss  36065  opelco3  36073  dfon2  36088  dfbigcup2  36195  sscoid  36209  funpartfv  36243  dfrdg4  36249  cgr3permute3  36345  segletr  36412  segleantisym  36413  seglelin  36414  fneval  36660  neibastop3  36670  eltail  36682  filnetlem4  36689  mh-infprim2bi  36855  bj-hbntbi  37127  bj-equsvt  37194  bj-sbceqgALT  37335  bj-clel3gALT  37481  bj-rest10  37526  bj-0int  37539  qdiffALT  37768  topdifinffinlem  37789  isbasisrelowllem1  37797  isbasisrelowllem2  37798  rdgeqoa  37812  finxpreclem4  37836  finxpsuclem  37839  wl-ifp4impr  37909  wl-1xor  37924  uncf  38046  phpreu  38051  cos2h  38058  tan2h  38059  matunitlindflem1  38063  poimirlem16  38083  poimirlem19  38086  poimirlem23  38090  poimirlem24  38091  poimirlem26  38093  poimirlem27  38094  mbfposadd  38114  cnambfre  38115  itg2addnclem  38118  itg2addnc  38121  iblabsnclem  38130  ftc1anclem1  38140  ftc1anclem5  38144  caures  38207  heiborlem3  38260  heiborlem10  38267  elghomOLD  38334  divrngidl  38475  eqrelf  38705  brvbrvvdif  38716  elrnres  38725  eldmres3  38730  eldmqsres2  38741  exanres  38748  relcnveq  38775  iss2  38791  ecinn0  38800  raldmqsmo  38810  brxrn2  38831  ecxrn  38853  ecxrn2  38855  disjressuc2  38858  elrelsrel  38889  eldmcoss2  38996  eldm1cossres  38997  elrelscnveq  39075  elcoeleqvrelsrel  39127  brredundsredund  39158  brdmqssqs  39178  cnvepresdmqss  39184  eldmqs1cossres  39191  brerser  39209  erimeq2  39210  eleldisjseldisj  39276  prtlem10  39437  prtlem16  39441  prtlem19  39450  prtex  39452  prter3  39454  islshpat  39589  lcvbr2  39594  lcvbr3  39595  lshpsmreu  39681  isat3  39879  hlrelat5N  39973  islpln5  40107  cdlemblem  40365  paddvaln0N  40373  paddval0  40382  cdlemefrs29bpre1  40969  cdlemefrs29cpre1  40970  cdlemg27b  41268  cdlemg33c  41280  cdlemg33e  41282  diaglbN  41627  cdlemm10N  41690  dicopelval2  41753  dicelval2N  41754  dihopelvalcpre  41820  dihglbcpreN  41872  dih1dimatlem  41901  dihatexv  41910  dvh4dimlem  42015  mapdpglem3  42247  hdmap14lem13  42452  hdmapglem7a  42499  eluzp1  42864  fsuppind  43120  isnacs2  43235  rabrenfdioph  43339  expdiophlem1  43546  pw2f1ocnv  43562  pwfi2f1o  43621  numinfctb  43628  dfacbasgrp  43633  islnr3  43640  onsupneqmaxlim0  43749  onsupnmax  43753  onsupuni  43754  tfsconcatrnss  43875  safesnsupfilb  43942  dfhe3  44299  clsk3nimkb  44564  ntrneiiso  44615  ntrneikb  44618  scottabf  44764  mnuunid  44801  hashnzfzclim  44846  dvconstbi  44858  sbcoreleleqVD  45382  trfr  45486  permac8prim  45538  rfcnpre3  45561  rfcnpre4  45562  r19.3rzf  45684  cncfshift  46396  stoweidlem59  46581  chnsubseqwl  47403  dfafv23  47795  nelbrnel  47818  elsetpreimafvrab  47948  iccpartiun  47988  prproropf1olem0  48056  prprelb  48070  prprspr2  48072  reuprpr  48077  oddm1evenALTV  48245  oddp1evenALTV  48246  oddprmne2  48285  fpprel  48298  dfvopnbgr2  48423  uhgrimisgrgric  48501  isgrlim  48552  gpg5nbgrvtx03starlem1  48638  gpg5nbgrvtx03starlem3  48640  gpg5nbgrvtx13starlem1  48641  gpg5nbgrvtx13starlem3  48643  iscmgmALT  48794  iscsgrpALT  48796  mofeu  49417  iscnrm3  49521  joindm2  49537  meetdm2  49539  oppcendc  49587  0funcg  49654  0funcALT  49657  istermc  50043  functermc2  50078  fulltermc  50080  elpglem2  50281