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  3620  eueq3  3673  sbceqal  3806  eqrrabd  4039  n0moeu  4312  sbcel12  4364  sbceqg  4365  sbcne12  4368  reldisj  4406  raldifeq  4447  r19.3rz  4450  ralf0  4467  eldifpr  4612  reusngf  4628  rexreusng  4633  eldiftp  4641  eqsndOLD  4785  reusv2lem5  5344  prelpw  5393  otthg  5432  2rbropap  5511  rabxp  5671  pwvrel  5673  ssrel3  5733  elrng  5838  iss  5990  idrefALT  6066  xpcan  6129  xpcan2  6130  dfpo2  6248  ordelpss  6339  fcnvres  6705  dffv3  6822  funimass4  6891  unima  6902  fndmdif  6980  fneqeql  6984  funimass3  6992  elrnrexdmb  7028  dff4  7039  fnsnbg  7104  fnsnbOLD  7106  fconst4  7154  elunirn  7191  f12dfv  7214  riota1  7331  riota2df  7333  f1ocnvfv3  7348  eqfnov  7482  elrnmpores  7491  caoftrn  7658  ordsucun  7764  dflim3  7787  dfom2  7808  peano5  7833  opiota  8001  frxp2  8084  xpord2pred  8085  xpord2indlem  8087  suppssr  8135  mpoxopovel  8160  brtpos  8175  rntpos  8179  ordgt0ge1  8418  ondif2  8427  oelim2  8520  omabs  8576  naddrid  8608  iiner  8723  erinxp  8725  qliftfun  8736  mapdm0  8776  ordunifi  9195  elfi2  9323  elfiun  9339  fifo  9341  noinfep  9575  cantnflem1  9604  cantnf  9608  rankonidlem  9743  r1pwALT  9761  cardalephex  10003  alephinit  10008  dfac5lem4OLD  10041  cflim2  10176  cfsmolem  10183  compssiso  10287  fin1a2lem11  10323  itunisuc  10332  axdclem  10432  brdom6disj  10445  alephreg  10495  fpwwe2lem8  10551  pwfseqlem3  10573  indpi  10820  nqereu  10842  ordpinq  10856  ltanq  10884  ltmnq  10885  suplem2pr  10966  map2psrpr  11023  ssxr  11203  leltne  11223  ltneg  11638  leneg  11641  suprnub  12108  negiso  12123  elnnnn0  12445  nn0sub  12452  fcdmnn0fsupp  12460  zrevaddcl  12538  znnsub  12539  znn0sub  12540  prime  12575  eluz2  12759  indstr  12835  eluz2b1  12838  qrevaddcl  12890  rpneg  12945  xrleltne  13065  dfle2  13067  dflt2  13068  supxrleub  13246  infxrgelb  13256  ixxin  13283  iccid  13311  elicopnf  13366  iccsplit  13406  fzsplit2  13470  fzsn  13487  fzpr  13500  uzsplit  13517  preduz  13571  fvinim0ffz  13707  injresinj  13709  om2uzf1oi  13878  lt2sqi  14114  le2sqi  14115  hashsdom  14306  hashf1lem1  14380  fz1isolem  14386  prprrab  14398  ccatlcan  14642  ccatrcan  14643  s3eq3seq  14864  2swrd2eqwrdeq  14878  trclfvcotr  14934  cnpart  15165  limsuplt  15404  rlimresb  15490  mertenslem2  15810  fprod2dlem  15905  sadadd2lem2  16379  saddisjlem  16393  bitsuz  16403  gcddiv  16480  algcvgblem  16506  isprm3  16612  isprm5  16636  prmreclem5  16850  vdwapun  16904  vdwmc2  16909  ramcl  16959  pwsle  17414  ismre  17510  mreacs  17582  acsfn  17583  iscatd2  17605  cidpropd  17634  dfiso2  17697  oppcsect2  17704  isfunc  17789  setcinv  18015  lubeldm  18275  lubval  18278  glbeldm  18288  glbval  18291  tosso  18341  ipodrsfi  18463  acsfiindd  18477  submgmacs  18609  imasmnd2  18666  ismhm0  18682  resmndismnd  18700  submacs  18719  imasgrp2  18952  issubg  19023  resgrpisgrp  19044  subgacs  19058  eqgval  19074  ghmqusnsglem1  19177  ghmquskerlem1  19180  gaorber  19205  symgfix2  19313  psgnran  19412  isslw  19505  sylow2alem2  19515  sylow2a  19516  sylow3lem6  19529  efgcpbllemb  19652  prmcyg  19791  gsum2d2lem  19870  gsumcom2  19872  subgdmdprd  19933  dprd2d2  19943  pgpfac1lem2  19974  pgpfac1lem4  19977  imasrng  20080  imasring  20233  isrnghmmul  20345  isnzr2  20421  isdomn3  20618  drngmulne0  20665  subrgacs  20703  sdrgacs  20704  lssle0  20871  lssacs  20888  lssats2  20921  lvecvsn0  21034  islpir  21253  zndvds  21474  znleval  21479  znleval2  21480  lindsmm  21753  islinds3  21759  islindf4  21763  ismhp3  22045  psdmul  22069  eltg2b  22862  discld  22992  opnssneib  23018  cldlp  23053  restbas  23061  leordtvallem1  23113  leordtvallem2  23114  ssidcn  23158  cnprest2  23193  lmss  23201  perfcls  23268  cmpfi  23311  1stccnp  23365  subislly  23384  hausmapdom  23403  locfindis  23433  iskgen3  23452  kgencn  23459  ptpjpre1  23474  xkoccn  23522  txrest  23534  txlm  23551  txkgen  23555  xkopt  23558  xkoinjcn  23590  imasnopn  23593  imasncld  23594  imasncls  23595  qtopcn  23617  kqfeq  23627  isr0  23640  fbfinnfr  23744  trfbas  23747  fbunfip  23772  ufileu  23822  cfinufil  23831  fmid  23863  txflf  23909  fclsrest  23927  alexsubALT  23954  tsmsres  24047  ucnima  24184  fmucndlem  24194  bldisj  24302  xmeter  24337  elbl4  24467  restmetu  24474  dscopn  24477  bl2ioo  24696  isphtpc  24909  tcphcph  25153  lmmbr2  25175  lmmbrf  25178  iscau2  25193  iscauf  25196  caucfil  25199  metcld  25222  metcld2  25223  bcthlem1  25240  bcthlem4  25243  cldcss2  25358  ovolgelb  25397  ovoliunlem1  25419  ismbfcn  25546  mbfmax  25566  mbfimaopnlem  25572  i1faddlem  25610  i1fmullem  25611  i1fres  25622  i1fpos  25623  itg1climres  25631  xrge0f  25648  itgresr  25696  iblcnlem1  25705  limcun  25812  dvres  25828  mdegmullem  25999  r1pid2  26083  ply1remlem  26086  plyremlem  26228  vieta1  26236  ulmcau  26320  sineq0  26449  coseq1  26450  ang180lem3  26737  cubic  26775  atandm  26802  atandm2  26803  atandm3  26804  rlimcnp  26891  rlimcnp2  26892  vmappw  27042  dchrelbas3  27165  dchrelbas4  27170  dchrsum2  27195  bposlem6  27216  2sqreuopltb  27392  2sqreuopnnltb  27394  dchrisumlem3  27418  pntleml  27538  noetasuplem4  27664  noetainflem4  27668  addsrid  27894  mulsrid  28039  mulsne0bd  28112  onsiso  28192  om2noseqf1o  28218  zn0subs  28314  avgslt1d  28362  avgslt2d  28363  istrkg3ld  28424  tgcgr4  28494  lnrot2  28587  islnopp  28702  islmib  28750  brbtwn2  28868  axsegconlem6  28885  axsegcon  28890  ax5seg  28901  axpasch  28904  axeuclid  28926  axcontlem4  28930  elntg2  28948  issubgr  29234  nb3gr2nb  29347  uhgrvd00  29498  isrusgr0  29530  wlkcpr  29592  wlkcomp  29594  upgr2wlk  29630  upgrf1istrl  29665  clwlkcomp  29742  clwlkcompbp  29745  iswwlksnx  29803  wspthsnwspthsnon  29879  wspniunwspnon  29886  2pthon3v  29906  usgr2wspthons3  29927  usgr2wspthon  29928  rusgrnumwwlks  29937  clwlkclwwlklem3  29963  clwlkclwwlk  29964  clwwlknonwwlknonb  30068  0pth  30087  eupth2lem2  30181  vdgn1frgrv2  30258  fusgreg2wsp  30298  clwwlknonclwlknonf1o  30324  dlwwlknondlwlknonf1o  30327  wlkl0  30329  nmoolb  30733  nmlno0lem  30755  ubthlem1  30832  ocsh  31245  shle0  31404  eigrei  31796  adjeu  31851  nmoplb  31869  nmfnlb  31886  eleigvec2  31920  nmlnop0iALT  31957  cnlnadjlem5  32033  adjbdln  32045  jplem2  32231  cvbr2  32245  mdsl2bi  32285  chrelat3  32333  eqelbid  32437  sq2reunnltb  32447  rmounid  32457  nelpr  32493  disjunsn  32556  ofpreima  32622  funcnvmpt  32624  funcnv5mpt  32625  dfcnv2  32633  suppiniseg  32642  gtiso  32657  fpwrelmap  32689  infxrge0glb  32721  xrdifh  32736  fzsplit3  32749  fzo0opth  32761  swrdrn3  32910  toslublem  32927  tosglblem  32929  mgcval  32942  mndlrinvb  32992  xrge0tsmsbi  33029  cntzun  33034  isarchi  33134  dvdsrspss  33334  rspsnasso  33335  lsmsnorb  33338  nsgqusf1olem2  33361  isprmidl  33385  ressply1mon1p  33513  r1pid2OLD  33550  constrfin  33712  smatrcl  33762  ist0cld  33799  rspectopn  33833  zarcls  33840  rhmpreimacnlem  33850  unitdivcld  33867  lmxrge0  33918  isrrext  33966  issibf  34300  eulerpartlemr  34341  eulerpartlemmf  34342  eulerpartlemn  34348  dstfrvunirn  34442  ballotlemfc0  34460  ballotlemfcc  34461  reprsuc  34582  reprpmtf1o  34593  reprdifc  34594  bnj919  34733  bnj976  34743  bnj1542  34823  bnj150  34842  bnj151  34843  bnj607  34882  bnj852  34887  bnj873  34890  bnj938  34903  bnj1171  34966  bnj1388  34999  bnj1489  35022  nummin  35057  usgrgt2cycl  35102  subfacp1lem3  35154  subfacp1lem5  35156  erdszelem9  35171  kur14  35188  iscvm  35231  satf0op  35349  mclsax  35541  rexxfr3dALT  35611  elintfv  35737  fundmpss  35739  opelco3  35747  dfon2  35765  dfbigcup2  35872  sscoid  35886  funpartfv  35918  dfrdg4  35924  cgr3permute3  36020  segletr  36087  segleantisym  36088  seglelin  36089  fneval  36325  neibastop3  36335  eltail  36347  filnetlem4  36354  bj-hbntbi  36677  bj-equsvt  36752  bj-sbceqgALT  36875  bj-clel3gALT  37021  bj-rest10  37061  bj-0int  37074  topdifinffinlem  37320  isbasisrelowllem1  37328  isbasisrelowllem2  37329  rdgeqoa  37343  finxpreclem4  37367  finxpsuclem  37370  wl-ifp4impr  37440  wl-1xor  37455  uncf  37578  phpreu  37583  cos2h  37590  tan2h  37591  matunitlindflem1  37595  poimirlem16  37615  poimirlem19  37618  poimirlem23  37622  poimirlem24  37623  poimirlem26  37625  poimirlem27  37626  mbfposadd  37646  cnambfre  37647  itg2addnclem  37650  itg2addnc  37653  iblabsnclem  37662  ftc1anclem1  37672  ftc1anclem5  37676  caures  37739  heiborlem3  37792  heiborlem10  37799  elghomOLD  37866  divrngidl  38007  eqrelf  38229  brvbrvvdif  38238  elrnres  38245  eldmres3  38250  eldmqsres2  38261  exanres  38268  relcnveq  38295  iss2  38311  ecinn0  38320  brxrn2  38342  ecxrn  38358  disjressuc2  38359  eldmcoss2  38435  eldm1cossres  38436  elrelsrel  38463  elrelscnveq  38468  elcoeleqvrelsrel  38572  brredundsredund  38603  brdmqssqs  38623  cnvepresdmqss  38629  eldmqs1cossres  38636  brerser  38654  erimeq2  38655  eleldisjseldisj  38706  prtlem10  38843  prtlem16  38847  prtlem19  38856  prtex  38858  prter3  38860  islshpat  38995  lcvbr2  39000  lcvbr3  39001  lshpsmreu  39087  isat3  39285  hlrelat5N  39380  islpln5  39514  cdlemblem  39772  paddvaln0N  39780  paddval0  39789  cdlemefrs29bpre1  40376  cdlemefrs29cpre1  40377  cdlemg27b  40675  cdlemg33c  40687  cdlemg33e  40689  diaglbN  41034  cdlemm10N  41097  dicopelval2  41160  dicelval2N  41161  dihopelvalcpre  41227  dihglbcpreN  41279  dih1dimatlem  41308  dihatexv  41317  dvh4dimlem  41422  mapdpglem3  41654  hdmap14lem13  41859  hdmapglem7a  41906  eluzp1  42280  fsuppind  42563  isnacs2  42679  rabrenfdioph  42787  expdiophlem1  42994  pw2f1ocnv  43010  pwfi2f1o  43069  numinfctb  43076  dfacbasgrp  43081  islnr3  43088  onsupneqmaxlim0  43197  onsupnmax  43201  onsupuni  43202  tfsconcatrnss  43323  safesnsupfilb  43391  dfhe3  43748  clsk3nimkb  44013  ntrneiiso  44064  ntrneikb  44067  scottabf  44213  mnuunid  44250  hashnzfzclim  44295  dvconstbi  44307  sbcoreleleqVD  44832  trfr  44936  permac8prim  44988  rfcnpre3  45011  rfcnpre4  45012  r19.3rzf  45136  cncfshift  45856  stoweidlem59  46041  dfafv23  47238  nelbrnel  47261  elsetpreimafvrab  47379  iccpartiun  47419  prproropf1olem0  47487  prprelb  47501  prprspr2  47503  reuprpr  47508  oddm1evenALTV  47660  oddp1evenALTV  47661  oddprmne2  47700  fpprel  47713  dfvopnbgr2  47837  uhgrimisgrgric  47915  isgrlim  47965  gpg5nbgrvtx03starlem1  48043  gpg5nbgrvtx03starlem3  48045  gpg5nbgrvtx13starlem1  48046  gpg5nbgrvtx13starlem3  48048  iscmgmALT  48196  iscsgrpALT  48198  mofeu  48820  iscnrm3  48924  joindm2  48940  meetdm2  48942  oppcendc  48991  0funcg  49058  0funcALT  49061  istermc  49447  functermc2  49482  fulltermc  49484  elpglem2  49685