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  4011  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  5538  rabxp  5698  pwvrel  5700  ssrel3  5761  elrng  5872  iss  6026  idrefALT  6106  xpcan  6167  xpcan2  6168  dfpo2  6299  ordelpss  6390  fcnvres  6759  dffv3  6881  funimass4  6949  unima  6960  funcnvmpt  6995  fndmdif  7041  fneqeql  7045  funimass3  7053  elrnrexdmb  7090  dff4  7101  fnsnbg  7169  fnsnbOLD  7171  fconst4  7220  elunirn  7255  f12dfv  7281  riota1  7398  riota2df  7400  f1ocnvfv3  7415  eqfnov  7549  elrnmpores  7558  caoftrn  7734  ordsucun  7836  dflim3  7858  dfom2  7879  peano5  7905  opiota  8070  frxp2  8161  xpord2pred  8162  xpord2indlem  8164  suppssr  8213  mpoxopovel  8238  brtpos  8253  rntpos  8257  ordgt0ge1  8502  ondif2  8511  oelim2  8605  omabs  8661  naddrid  8694  iiner  8811  erinxp  8813  qliftfun  8824  mapdm0  8863  uncf  8892  ordunifi  9282  elfi2  9407  elfiun  9423  fifo  9425  noinfep  9662  cantnflem1  9691  cantnf  9695  rankonidlem  9839  r1pwALT  9861  scottabf  9940  cardalephex  10170  alephinit  10175  cflim2  10342  cfsmolem  10349  compssiso  10453  fin1a2lem11  10489  itunisuc  10498  axdclem  10598  brdom6disj  10612  alephreg  10668  fpwwe2lem8  10724  pwfseqlem3  10746  indpi  10993  nqereu  11015  ordpinq  11029  ltanq  11057  ltmnq  11058  suplem2pr  11139  map2psrpr  11196  ssxr  11380  leltne  11400  ltneg  11817  leneg  11820  suprnub  12283  negiso  12298  elnnnn0  12650  nn0sub  12657  fcdmnn0fsupp  12665  zrevaddcl  12742  znnsub  12743  znn0sub  12744  prime  12781  eluz2  12972  indstr  13044  eluz2b1  13047  qrevaddcl  13100  rpneg  13155  xrleltne  13275  dfle2  13277  dflt2  13278  supxrleub  13457  infxrgelb  13467  ixxin  13494  iccid  13522  elicopnf  13577  iccsplit  13617  fzsplit2  13684  fzsn  13701  fzpr  13714  uzsplit  13731  preduz  13785  fvinim0ffz  13925  injresinj  13927  om2uzf1oi  14097  lt2sqi  14333  le2sqi  14334  hashsdom  14526  hashf1lem1  14601  fz1isolem  14607  prprrab  14619  swrdrn3  14803  ccatlcan  14868  ccatrcan  14869  s3eq3seq  15091  2swrd2eqwrdeq  15107  trclfvcotr  15163  cnpart  15408  limsuplt  15647  rlimresb  15733  mertenslem2  16055  fprod2dlem  16148  sadadd2lem2  16621  saddisjlem  16635  bitsuz  16645  gcddiv  16725  algcvgblem  16753  isprm3  16859  isprm5  16884  prmreclem5  17099  vdwapun  17153  vdwmc2  17158  ramcl  17208  pwsle  17665  ismre  17761  mreacs  17833  acsfn  17834  iscatd2  17856  cidpropd  17885  dfiso2  17948  oppcsect2  17955  isfunc  18040  setcinv  18266  lubeldm  18526  lubval  18529  glbeldm  18539  glbval  18542  tosso  18592  ipodrsfi  18714  acsfiindd  18728  submgmacs  18907  imasmnd2  18969  ismhm0  18986  resmndismnd  19004  submacs  19024  imasgrp2  19266  issubg  19337  resgrpisgrp  19359  subgacs  19372  eqgval  19390  ghmqusnsglem1  19495  ghmquskerlem1  19498  gaorber  19523  symgfix2  19631  psgnran  19730  isslw  19823  sylow2alem2  19833  sylow2a  19834  sylow3lem6  19847  efgcpbllemb  19970  prmcyg  20109  gsum2d2lem  20188  gsumcom2  20190  subgdmdprd  20251  dprd2d2  20261  pgpfac1lem2  20292  pgpfac1lem4  20295  imasrng  20400  imasring  20561  isrnghmmul  20673  isnzr2  20769  isdomn3  20967  drngmulne0  21020  subrgacs  21058  sdrgacs  21059  lssle0  21226  lssacs  21243  lssats2  21276  lvecvsn0  21388  rspsn0  21527  isprmidl  21620  islpir  21653  zndvds  21856  znleval  21861  znleval2  21862  lindsmm  22135  islinds3  22141  islindf4  22145  ismhp3  22464  psdmul  22488  matunitlindflem1  22995  eltg2b  23278  discld  23408  opnssneib  23434  cldlp  23469  restbas  23477  leordtvallem1  23529  leordtvallem2  23530  ssidcn  23574  cnprest2  23609  lmss  23617  perfcls  23684  cmpfi  23727  1stccnp  23782  subislly  23801  hausmapdom  23820  locfindis  23850  iskgen3  23869  kgencn  23876  ptpjpre1  23891  xkoccn  23939  txrest  23951  txlm  23968  txkgen  23972  xkopt  23975  xkoinjcn  24007  imasnopn  24010  imasncld  24011  imasncls  24012  qtopcn  24034  kqfeq  24044  isr0  24057  fbfinnfr  24161  trfbas  24164  fbunfip  24189  ufileu  24239  cfinufil  24248  fmid  24280  txflf  24326  fclsrest  24344  alexsubALT  24371  tsmsres  24464  ucnima  24600  fmucndlem  24610  bldisj  24718  xmeter  24753  elbl4  24883  restmetu  24890  dscopn  24893  bl2ioo  25112  isphtpc  25316  tcphcph  25559  lmmbr2  25581  lmmbrf  25584  iscau2  25599  iscauf  25602  caucfil  25605  metcld  25628  metcld2  25629  bcthlem1  25646  bcthlem4  25649  cldcss2  25764  ovolgelb  25802  ovoliunlem1  25824  ismbfcn  25951  mbfmax  25971  mbfimaopnlem  25977  i1faddlem  26015  i1fmullem  26016  i1fres  26027  i1fpos  26028  itg1climres  26036  xrge0f  26053  itgresr  26100  iblcnlem1  26109  limcun  26216  dvres  26232  mdegmullem  26397  r1pid2  26481  ply1remlem  26484  plyremlem  26626  vieta1  26636  ulmcau  26723  sineq0  26853  coseq1  26854  ang180lem3  27140  cubic  27178  atandm  27205  atandm2  27206  atandm3  27207  rlimcnp  27294  rlimcnp2  27295  vmappw  27444  dchrelbas3  27566  dchrelbas4  27571  dchrsum2  27596  bposlem6  27617  2sqreuopltb  27793  2sqreuopnnltb  27795  dchrisumlem3  27819  pntleml  27939  noetasuplem4  28094  noetainflem4  28098  rightge0  28208  addsrid  28351  negleft  28445  negright  28446  mulsrid  28500  mulsne0bd  28573  oniso  28658  om2noseqf1o  28688  zn0subs  28790  avglts1d  28840  avglts2d  28841  istrkg3ld  28924  tgcgr4  28995  lnrot2  29093  islnopp  29216  islmib  29293  mptelee  29473  brbtwn2  29484  axsegconlem6  29501  axsegcon  29506  ax5seg  29517  axpasch  29520  axeuclid  29542  axcontlem4  29546  elntg2  29564  issubgr  29853  nb3gr2nb  29966  uhgrvd00  30116  isrusgr0  30148  wlkcpr  30210  wlkcomp  30212  upgr2wlk  30248  upgrf1istrl  30287  clwlkcomp  30367  clwlkcompbp  30370  iswwlksnx  30430  wspthsnwspthsnon  30506  wspniunwspnon  30513  2pthon3v  30533  usgr2wspthons3  30557  usgr2wspthon  30558  rusgrnumwwlks  30567  clwlkclwwlklem3  30593  clwlkclwwlk  30594  clwwlknonwwlknonb  30698  0pth  30717  eupth2lem2  30821  vdgn1frgrv2  30898  fusgreg2wsp  30938  clwwlknonclwlknonf1o  30964  dlwwlknondlwlknonf1o  30967  wlkl0  30969  nmoolb  31374  nmlno0lem  31396  ubthlem1  31473  ocsh  31886  shle0  32045  eigrei  32437  adjeu  32492  nmoplb  32510  nmfnlb  32527  eleigvec2  32561  nmlnop0iALT  32598  cnlnadjlem5  32674  adjbdln  32686  jplem2  32872  cvbr2  32886  mdsl2bi  32926  chrelat3  32974  eqelbid  33114  sq2reunnltb  33124  rmounid  33134  nelpr  33170  disjunsn  33231  ofpreima  33302  funcnv5mpt  33304  dfcnv2  33312  suppiniseg  33322  gtiso  33337  fpwrelmap  33368  infxrge0glb  33400  xrdifh  33415  fzsplit3  33428  fzo0opth  33438  toslublem  33576  tosglblem  33578  mgcval  33591  mndlrinvb  33629  xrge0tsmsbi  33678  cntzun  33683  isarchi  33786  dvdsrspss  33985  rspsnasso  33986  lsmsnorb  33989  nsgqusf1olem2  34008  ressply1mon1p  34143  constrfin  34421  smatrcl  34471  ist0cld  34508  rspectopn  34542  zarcls  34549  rhmpreimacnlem  34559  unitdivcld  34576  lmxrge0  34627  isrrext  34675  issibf  35008  eulerpartlemr  35049  eulerpartlemmf  35050  eulerpartlemn  35056  dstfrvunirn  35150  ballotlemfc0  35168  ballotlemfcc  35169  reprsuc  35287  reprpmtf1o  35298  reprdifc  35299  bnj919  35441  bnj976  35451  bnj1542  35530  bnj150  35549  bnj151  35550  bnj607  35589  bnj852  35594  bnj873  35597  bnj938  35610  bnj1171  35673  bnj1388  35706  bnj1489  35729  nummin  35767  dfscott3  35790  usgrgt2cycl  35978  subfacp1lem3  36016  subfacp1lem5  36018  erdszelem9  36033  kur14  36050  iscvm  36093  satf0op  36211  mclsax  36403  rexxfr3dALT  36473  elintfv  36605  fundmpss  36607  opelco3  36614  dfon2  36629  dfbigcup2  36736  sscoid  36750  funpartfv  36784  dfrdg4  36790  cgr3permute3  36887  segletr  36954  segleantisym  36955  seglelin  36956  nmulrid  37021  fneval  37215  neibastop3  37225  eltail  37237  filnetlem4  37244  mh-infprim2bi  37410  bj-hbntbi  37681  bj-equsvt  37748  bj-sbceqgALT  37889  bj-clel3gALT  38038  bj-rest10  38084  bj-0int  38097  qdiffALT  38325  topdifinffinlem  38346  isbasisrelowllem1  38354  isbasisrelowllem2  38355  rdgeqoa  38369  finxpreclem4  38393  finxpsuclem  38396  wl-ifp4impr  38466  wl-1xor  38481  phpreu  38603  cos2h  38610  tan2h  38611  poimirlem16  38630  poimirlem19  38633  poimirlem23  38637  poimirlem24  38638  poimirlem26  38640  poimirlem27  38641  mbfposadd  38661  cnambfre  38662  itg2addnclem  38665  itg2addnc  38668  iblabsnclem  38677  ftc1anclem1  38687  ftc1anclem5  38691  findcard4  38708  caures  38770  heiborlem3  38823  heiborlem10  38830  elghomOLD  38897  divrngidl  39038  eqrelf  39266  brvbrvvdif  39277  elrnres  39286  eldmres3  39291  eldmqsres2  39302  exanres  39309  relcnveq  39336  iss2  39352  ecinn0  39361  raldmqsmo  39371  brxrn2  39392  ecxrn  39414  ecxrn2  39416  disjressuc2  39419  elrelsrel  39450  eldmcoss2  39557  eldm1cossres  39558  elrelscnveq  39636  elcoeleqvrelsrel  39688  brredundsredund  39719  brdmqssqs  39739  cnvepresdmqss  39745  eldmqs1cossres  39752  brerser  39770  erimeq2  39771  eleldisjseldisj  39837  prtlem10  39998  prtlem16  40002  prtlem19  40011  prtex  40013  prter3  40015  islshpat  40150  lcvbr2  40155  lcvbr3  40156  lshpsmreu  40242  isat3  40440  hlrelat5N  40534  islpln5  40668  cdlemblem  40926  paddvaln0N  40934  paddval0  40943  cdlemefrs29bpre1  41530  cdlemefrs29cpre1  41531  cdlemg27b  41829  cdlemg33c  41841  cdlemg33e  41843  diaglbN  42188  cdlemm10N  42251  dicopelval2  42314  dicelval2N  42315  dihopelvalcpre  42381  dihglbcpreN  42433  dih1dimatlem  42462  dihatexv  42471  dvh4dimlem  42576  mapdpglem3  42808  hdmap14lem13  43013  hdmapglem7a  43060  eluzp1  43440  fsuppind  43694  isnacs2  43793  rabrenfdioph  43897  expdiophlem1  44104  pw2f1ocnv  44120  pwfi2f1o  44174  numinfctb  44181  dfacbasgrp  44186  islnr3  44193  onsupneqmaxlim0  44302  onsupnmax  44306  onsupuni  44307  tfsconcatrnss  44428  safesnsupfilb  44495  dfhe3  44851  clsk3nimkb  45116  ntrneiiso  45167  ntrneikb  45170  mnuunid  45337  hashnzfzclim  45382  dvconstbi  45394  sbcoreleleqVD  45917  trfr  46028  permac8prim  46080  rfcnpre3  46126  rfcnpre4  46127  r19.3rzf  46249  cncfshift  46960  stoweidlem59  47145  chnsubseqwl  47965  dfafv23  48399  nelbrnel  48422  elsetpreimafvrab  48552  iccpartiun  48592  prproropf1olem0  48660  prprelb  48674  prprspr2  48676  reuprpr  48681  oddm1evenALTV  48849  oddp1evenALTV  48850  oddprmne2  48889  fpprel  48902  dfvopnbgr2  49027  uhgrimisgrgric  49105  isgrlim  49156  gpg5nbgrvtx03starlem1  49242  gpg5nbgrvtx03starlem3  49244  gpg5nbgrvtx13starlem1  49245  gpg5nbgrvtx13starlem3  49247  iscmgmALT  49397  iscsgrpALT  49399  mofeu  50034  iscnrm3  50136  joindm2  50152  meetdm2  50154  oppcendc  50202  0funcg  50269  0funcALT  50272  istermc  50658  functermc2  50693  fulltermc  50695  elpglem2  50881