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  3616  eueq3  3668  sbceqal  3799  eqrrabd  4033  n0moeu  4306  sbcel12  4368  sbceqg  4369  sbcne12  4372  reldisj  4405  raldifeq  4448  r19.3rz  4456  eldifpr  4618  reusngf  4634  rexreusng  4639  eldiftp  4647  reusv2lem5  5363  prelpw  5413  otthg  5453  2rbropap  5535  rabxp  5695  pwvrel  5697  ssrel3  5758  elrng  5869  iss  6025  idrefALT  6101  xpcan  6163  xpcan2  6164  dfpo2  6288  ordelpss  6379  fcnvres  6747  dffv3  6869  funimass4  6937  unima  6948  funcnvmpt  6983  fndmdif  7029  fneqeql  7033  funimass3  7041  elrnrexdmb  7078  dff4  7089  fnsnbg  7157  fnsnbOLD  7159  fconst4  7208  elunirn  7243  f12dfv  7269  riota1  7386  riota2df  7388  f1ocnvfv3  7403  eqfnov  7537  elrnmpores  7546  caoftrn  7717  ordsucun  7819  dflim3  7841  dfom2  7862  peano5  7888  opiota  8053  frxp2  8139  xpord2pred  8140  xpord2indlem  8142  suppssr  8190  mpoxopovel  8215  brtpos  8230  rntpos  8234  ordgt0ge1  8479  ondif2  8488  oelim2  8582  omabs  8638  naddrid  8671  iiner  8788  erinxp  8790  qliftfun  8801  mapdm0  8840  uncf  8869  ordunifi  9259  elfi2  9384  elfiun  9400  fifo  9402  noinfep  9639  cantnflem1  9668  cantnf  9672  rankonidlem  9811  r1pwALT  9833  scottabf  9911  cardalephex  10141  alephinit  10146  cflim2  10313  cfsmolem  10320  compssiso  10424  fin1a2lem11  10460  itunisuc  10469  axdclem  10569  brdom6disj  10583  alephreg  10639  fpwwe2lem8  10695  pwfseqlem3  10717  indpi  10964  nqereu  10986  ordpinq  11000  ltanq  11028  ltmnq  11029  suplem2pr  11110  map2psrpr  11167  ssxr  11351  leltne  11371  ltneg  11786  leneg  11789  suprnub  12252  negiso  12267  elnnnn0  12619  nn0sub  12626  fcdmnn0fsupp  12634  zrevaddcl  12711  znnsub  12712  znn0sub  12713  prime  12750  eluz2  12941  indstr  13013  eluz2b1  13016  qrevaddcl  13069  rpneg  13124  xrleltne  13244  dfle2  13246  dflt2  13247  supxrleub  13426  infxrgelb  13436  ixxin  13463  iccid  13491  elicopnf  13546  iccsplit  13586  fzsplit2  13652  fzsn  13669  fzpr  13682  uzsplit  13699  preduz  13753  fvinim0ffz  13893  injresinj  13895  om2uzf1oi  14065  lt2sqi  14301  le2sqi  14302  hashsdom  14493  hashf1lem1  14568  fz1isolem  14574  prprrab  14586  swrdrn3  14770  ccatlcan  14835  ccatrcan  14836  s3eq3seq  15058  2swrd2eqwrdeq  15074  trclfvcotr  15130  cnpart  15375  limsuplt  15614  rlimresb  15700  mertenslem2  16022  fprod2dlem  16115  sadadd2lem2  16588  saddisjlem  16602  bitsuz  16612  gcddiv  16689  algcvgblem  16715  isprm3  16821  isprm5  16846  prmreclem5  17060  vdwapun  17114  vdwmc2  17119  ramcl  17169  pwsle  17626  ismre  17722  mreacs  17794  acsfn  17795  iscatd2  17817  cidpropd  17846  dfiso2  17909  oppcsect2  17916  isfunc  18001  setcinv  18227  lubeldm  18487  lubval  18490  glbeldm  18500  glbval  18503  tosso  18553  ipodrsfi  18675  acsfiindd  18689  submgmacs  18868  imasmnd2  18930  ismhm0  18947  resmndismnd  18965  submacs  18985  imasgrp2  19227  issubg  19298  resgrpisgrp  19320  subgacs  19333  eqgval  19351  ghmqusnsglem1  19456  ghmquskerlem1  19459  gaorber  19484  symgfix2  19592  psgnran  19691  isslw  19784  sylow2alem2  19794  sylow2a  19795  sylow3lem6  19808  efgcpbllemb  19931  prmcyg  20070  gsum2d2lem  20149  gsumcom2  20151  subgdmdprd  20212  dprd2d2  20222  pgpfac1lem2  20253  pgpfac1lem4  20256  imasrng  20361  imasring  20522  isrnghmmul  20634  isnzr2  20730  isdomn3  20928  drngmulne0  20981  subrgacs  21019  sdrgacs  21020  lssle0  21187  lssacs  21204  lssats2  21237  lvecvsn0  21349  rspsn0  21488  isprmidl  21581  islpir  21614  zndvds  21817  znleval  21822  znleval2  21823  lindsmm  22096  islinds3  22102  islindf4  22106  ismhp3  22425  psdmul  22449  matunitlindflem1  22956  eltg2b  23239  discld  23369  opnssneib  23395  cldlp  23430  restbas  23438  leordtvallem1  23490  leordtvallem2  23491  ssidcn  23535  cnprest2  23570  lmss  23578  perfcls  23645  cmpfi  23688  1stccnp  23743  subislly  23762  hausmapdom  23781  locfindis  23811  iskgen3  23830  kgencn  23837  ptpjpre1  23852  xkoccn  23900  txrest  23912  txlm  23929  txkgen  23933  xkopt  23936  xkoinjcn  23968  imasnopn  23971  imasncld  23972  imasncls  23973  qtopcn  23995  kqfeq  24005  isr0  24018  fbfinnfr  24122  trfbas  24125  fbunfip  24150  ufileu  24200  cfinufil  24209  fmid  24241  txflf  24287  fclsrest  24305  alexsubALT  24332  tsmsres  24425  ucnima  24561  fmucndlem  24571  bldisj  24679  xmeter  24714  elbl4  24844  restmetu  24851  dscopn  24854  bl2ioo  25073  isphtpc  25277  tcphcph  25520  lmmbr2  25542  lmmbrf  25545  iscau2  25560  iscauf  25563  caucfil  25566  metcld  25589  metcld2  25590  bcthlem1  25607  bcthlem4  25610  cldcss2  25725  ovolgelb  25763  ovoliunlem1  25785  ismbfcn  25912  mbfmax  25932  mbfimaopnlem  25938  i1faddlem  25976  i1fmullem  25977  i1fres  25988  i1fpos  25989  itg1climres  25997  xrge0f  26014  itgresr  26061  iblcnlem1  26070  limcun  26177  dvres  26193  mdegmullem  26358  r1pid2  26442  ply1remlem  26445  plyremlem  26589  vieta1  26599  ulmcau  26686  sineq0  26816  coseq1  26817  ang180lem3  27103  cubic  27141  atandm  27168  atandm2  27169  atandm3  27170  rlimcnp  27257  rlimcnp2  27258  vmappw  27407  dchrelbas3  27529  dchrelbas4  27534  dchrsum2  27559  bposlem6  27580  2sqreuopltb  27756  2sqreuopnnltb  27758  dchrisumlem3  27782  pntleml  27902  noetasuplem4  28027  noetainflem4  28031  rightge0  28141  addsrid  28284  negleft  28378  negright  28379  mulsrid  28433  mulsne0bd  28506  oniso  28591  om2noseqf1o  28621  zn0subs  28723  avglts1d  28773  avglts2d  28774  istrkg3ld  28857  tgcgr4  28928  lnrot2  29026  islnopp  29149  islmib  29226  mptelee  29406  brbtwn2  29417  axsegconlem6  29434  axsegcon  29439  ax5seg  29450  axpasch  29453  axeuclid  29475  axcontlem4  29479  elntg2  29497  issubgr  29786  nb3gr2nb  29899  uhgrvd00  30049  isrusgr0  30081  wlkcpr  30143  wlkcomp  30145  upgr2wlk  30181  upgrf1istrl  30220  clwlkcomp  30300  clwlkcompbp  30303  iswwlksnx  30363  wspthsnwspthsnon  30439  wspniunwspnon  30446  2pthon3v  30466  usgr2wspthons3  30490  usgr2wspthon  30491  rusgrnumwwlks  30500  clwlkclwwlklem3  30526  clwlkclwwlk  30527  clwwlknonwwlknonb  30631  0pth  30650  eupth2lem2  30754  vdgn1frgrv2  30831  fusgreg2wsp  30871  clwwlknonclwlknonf1o  30897  dlwwlknondlwlknonf1o  30900  wlkl0  30902  nmoolb  31307  nmlno0lem  31329  ubthlem1  31406  ocsh  31819  shle0  31978  eigrei  32370  adjeu  32425  nmoplb  32443  nmfnlb  32460  eleigvec2  32494  nmlnop0iALT  32531  cnlnadjlem5  32607  adjbdln  32619  jplem2  32805  cvbr2  32819  mdsl2bi  32859  chrelat3  32907  eqelbid  33005  sq2reunnltb  33015  rmounid  33025  nelpr  33061  disjunsn  33122  ofpreima  33193  funcnv5mpt  33195  dfcnv2  33203  suppiniseg  33213  gtiso  33228  fpwrelmap  33259  infxrge0glb  33291  xrdifh  33306  fzsplit3  33319  fzo0opth  33329  toslublem  33467  tosglblem  33469  mgcval  33482  mndlrinvb  33520  xrge0tsmsbi  33569  cntzun  33574  isarchi  33677  dvdsrspss  33876  rspsnasso  33877  lsmsnorb  33880  nsgqusf1olem2  33899  ressply1mon1p  34034  constrfin  34312  smatrcl  34362  ist0cld  34399  rspectopn  34433  zarcls  34440  rhmpreimacnlem  34450  unitdivcld  34467  lmxrge0  34518  isrrext  34566  issibf  34900  eulerpartlemr  34941  eulerpartlemmf  34942  eulerpartlemn  34948  dstfrvunirn  35042  ballotlemfc0  35060  ballotlemfcc  35061  reprsuc  35179  reprpmtf1o  35190  reprdifc  35191  bnj919  35333  bnj976  35343  bnj1542  35422  bnj150  35441  bnj151  35442  bnj607  35481  bnj852  35486  bnj873  35489  bnj938  35502  bnj1171  35565  bnj1388  35598  bnj1489  35621  nummin  35653  dfscott3  35673  usgrgt2cycl  35830  subfacp1lem3  35868  subfacp1lem5  35870  erdszelem9  35885  kur14  35902  iscvm  35945  satf0op  36063  mclsax  36255  rexxfr3dALT  36325  elintfv  36451  fundmpss  36453  opelco3  36461  dfon2  36476  dfbigcup2  36583  sscoid  36597  funpartfv  36631  dfrdg4  36637  cgr3permute3  36734  segletr  36801  segleantisym  36802  seglelin  36803  nmulrid  36868  fneval  37062  neibastop3  37072  eltail  37084  filnetlem4  37091  mh-infprim2bi  37257  bj-hbntbi  37528  bj-equsvt  37595  bj-sbceqgALT  37736  bj-clel3gALT  37883  bj-rest10  37929  bj-0int  37942  qdiffALT  38169  topdifinffinlem  38190  isbasisrelowllem1  38198  isbasisrelowllem2  38199  rdgeqoa  38213  finxpreclem4  38237  finxpsuclem  38240  wl-ifp4impr  38310  wl-1xor  38325  phpreu  38447  cos2h  38454  tan2h  38455  poimirlem16  38474  poimirlem19  38477  poimirlem23  38481  poimirlem24  38482  poimirlem26  38484  poimirlem27  38485  mbfposadd  38505  cnambfre  38506  itg2addnclem  38509  itg2addnc  38512  iblabsnclem  38521  ftc1anclem1  38531  ftc1anclem5  38535  findcard4  38552  caures  38614  heiborlem3  38667  heiborlem10  38674  elghomOLD  38741  divrngidl  38882  eqrelf  39110  brvbrvvdif  39121  elrnres  39130  eldmres3  39135  eldmqsres2  39146  exanres  39153  relcnveq  39180  iss2  39196  ecinn0  39205  raldmqsmo  39215  brxrn2  39236  ecxrn  39258  ecxrn2  39260  disjressuc2  39263  elrelsrel  39294  eldmcoss2  39401  eldm1cossres  39402  elrelscnveq  39480  elcoeleqvrelsrel  39532  brredundsredund  39563  brdmqssqs  39583  cnvepresdmqss  39589  eldmqs1cossres  39596  brerser  39614  erimeq2  39615  eleldisjseldisj  39681  prtlem10  39842  prtlem16  39846  prtlem19  39855  prtex  39857  prter3  39859  islshpat  39994  lcvbr2  39999  lcvbr3  40000  lshpsmreu  40086  isat3  40284  hlrelat5N  40378  islpln5  40512  cdlemblem  40770  paddvaln0N  40778  paddval0  40787  cdlemefrs29bpre1  41374  cdlemefrs29cpre1  41375  cdlemg27b  41673  cdlemg33c  41685  cdlemg33e  41687  diaglbN  42032  cdlemm10N  42095  dicopelval2  42158  dicelval2N  42159  dihopelvalcpre  42225  dihglbcpreN  42277  dih1dimatlem  42306  dihatexv  42315  dvh4dimlem  42420  mapdpglem3  42652  hdmap14lem13  42857  hdmapglem7a  42904  eluzp1  43286  fsuppind  43540  isnacs2  43655  rabrenfdioph  43759  expdiophlem1  43966  pw2f1ocnv  43982  pwfi2f1o  44041  numinfctb  44048  dfacbasgrp  44053  islnr3  44060  onsupneqmaxlim0  44169  onsupnmax  44173  onsupuni  44174  tfsconcatrnss  44295  safesnsupfilb  44362  dfhe3  44719  clsk3nimkb  44984  ntrneiiso  45035  ntrneikb  45038  mnuunid  45205  hashnzfzclim  45250  dvconstbi  45262  sbcoreleleqVD  45785  trfr  45889  permac8prim  45941  rfcnpre3  45971  rfcnpre4  45972  r19.3rzf  46094  cncfshift  46806  stoweidlem59  46991  chnsubseqwl  47811  dfafv23  48245  nelbrnel  48268  elsetpreimafvrab  48398  iccpartiun  48438  prproropf1olem0  48506  prprelb  48520  prprspr2  48522  reuprpr  48527  oddm1evenALTV  48695  oddp1evenALTV  48696  oddprmne2  48735  fpprel  48748  dfvopnbgr2  48873  uhgrimisgrgric  48951  isgrlim  49002  gpg5nbgrvtx03starlem1  49088  gpg5nbgrvtx03starlem3  49090  gpg5nbgrvtx13starlem1  49091  gpg5nbgrvtx13starlem3  49093  iscmgmALT  49243  iscsgrpALT  49245  mofeu  49880  iscnrm3  49982  joindm2  49998  meetdm2  50000  oppcendc  50048  0funcg  50115  0funcALT  50118  istermc  50504  functermc2  50539  fulltermc  50541  elpglem2  50727