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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3bitr4g  317  bibi2i  340  mtt  367  nbn2  373  ifptru  1089  3bior1fd  1499  3biant1d  1502  clel4g  3625  eueq3  3677  sbceqal  3808  eqrrabd  4042  n0moeu  4315  sbcel12  4368  sbceqg  4369  sbcne12  4372  reldisj  4410  raldifeq  4450  r19.3rz  4458  eldifpr  4620  reusngf  4636  rexreusng  4641  eldiftp  4649  eqsndOLD  4792  reusv2lem5  5364  prelpw  5418  otthg  5458  2rbropap  5540  rabxp  5700  pwvrel  5702  ssrel3  5763  elrng  5872  iss  6028  idrefALT  6104  xpcan  6166  xpcan2  6167  dfpo2  6287  ordelpss  6378  fcnvres  6745  dffv3  6867  funimass4  6935  unima  6946  funcnvmpt  6981  fndmdif  7027  fneqeql  7031  funimass3  7039  elrnrexdmb  7075  dff4  7086  fnsnbg  7152  fnsnbOLD  7154  fconst4  7202  elunirn  7239  f12dfv  7261  riota1  7378  riota2df  7380  f1ocnvfv3  7395  eqfnov  7529  elrnmpores  7538  caoftrn  7705  ordsucun  7809  dflim3  7831  dfom2  7852  peano5  7878  opiota  8044  frxp2  8128  xpord2pred  8129  xpord2indlem  8131  suppssr  8179  mpoxopovel  8204  brtpos  8219  rntpos  8223  ordgt0ge1  8466  ondif2  8475  oelim2  8569  omabs  8625  naddrid  8658  iiner  8775  erinxp  8777  qliftfun  8788  mapdm0  8827  ordunifi  9238  elfi2  9362  elfiun  9378  fifo  9380  noinfep  9617  cantnflem1  9646  cantnf  9650  rankonidlem  9788  r1pwALT  9806  scottabf  9854  cardalephex  10062  alephinit  10067  cflim2  10235  cfsmolem  10242  compssiso  10346  fin1a2lem11  10382  itunisuc  10391  axdclem  10491  brdom6disj  10504  alephreg  10555  fpwwe2lem8  10611  pwfseqlem3  10633  indpi  10880  nqereu  10902  ordpinq  10916  ltanq  10944  ltmnq  10945  suplem2pr  11026  map2psrpr  11083  ssxr  11267  leltne  11287  ltneg  11702  leneg  11705  suprnub  12171  negiso  12186  elnnnn0  12538  nn0sub  12545  fcdmnn0fsupp  12553  zrevaddcl  12630  znnsub  12631  znn0sub  12632  prime  12668  eluz2  12859  indstr  12931  eluz2b1  12934  qrevaddcl  12986  rpneg  13041  xrleltne  13161  dfle2  13163  dflt2  13164  supxrleub  13343  infxrgelb  13353  ixxin  13380  iccid  13408  elicopnf  13463  iccsplit  13503  fzsplit2  13568  fzsn  13585  fzpr  13598  uzsplit  13615  preduz  13669  fvinim0ffz  13809  injresinj  13811  om2uzf1oi  13980  lt2sqi  14216  le2sqi  14217  hashsdom  14408  hashf1lem1  14482  fz1isolem  14488  prprrab  14500  ccatlcan  14745  ccatrcan  14746  s3eq3seq  14966  2swrd2eqwrdeq  14980  trclfvcotr  15036  cnpart  15281  limsuplt  15520  rlimresb  15606  mertenslem2  15929  fprod2dlem  16024  sadadd2lem2  16498  saddisjlem  16512  bitsuz  16522  gcddiv  16599  algcvgblem  16625  isprm3  16731  isprm5  16756  prmreclem5  16970  vdwapun  17024  vdwmc2  17029  ramcl  17079  pwsle  17536  ismre  17632  mreacs  17704  acsfn  17705  iscatd2  17727  cidpropd  17756  dfiso2  17819  oppcsect2  17826  isfunc  17911  setcinv  18137  lubeldm  18397  lubval  18400  glbeldm  18410  glbval  18413  tosso  18463  ipodrsfi  18585  acsfiindd  18599  submgmacs  18765  imasmnd2  18822  ismhm0  18838  resmndismnd  18856  submacs  18876  imasgrp2  19112  issubg  19183  resgrpisgrp  19205  subgacs  19218  eqgval  19236  ghmqusnsglem1  19341  ghmquskerlem1  19344  gaorber  19369  symgfix2  19477  psgnran  19576  isslw  19669  sylow2alem2  19679  sylow2a  19680  sylow3lem6  19693  efgcpbllemb  19816  prmcyg  19955  gsum2d2lem  20034  gsumcom2  20036  subgdmdprd  20097  dprd2d2  20107  pgpfac1lem2  20138  pgpfac1lem4  20141  imasrng  20246  imasring  20403  isrnghmmul  20515  isnzr2  20592  isdomn3  20790  drngmulne0  20835  subrgacs  20872  sdrgacs  20873  lssle0  21040  lssacs  21057  lssats2  21090  lvecvsn0  21202  isprmidl  21425  islpir  21456  zndvds  21659  znleval  21664  znleval2  21665  lindsmm  21938  islinds3  21944  islindf4  21948  ismhp3  22265  psdmul  22289  eltg2b  23077  discld  23207  opnssneib  23233  cldlp  23268  restbas  23276  leordtvallem1  23328  leordtvallem2  23329  ssidcn  23373  cnprest2  23408  lmss  23416  perfcls  23483  cmpfi  23526  1stccnp  23580  subislly  23599  hausmapdom  23618  locfindis  23648  iskgen3  23667  kgencn  23674  ptpjpre1  23689  xkoccn  23737  txrest  23749  txlm  23766  txkgen  23770  xkopt  23773  xkoinjcn  23805  imasnopn  23808  imasncld  23809  imasncls  23810  qtopcn  23832  kqfeq  23842  isr0  23855  fbfinnfr  23959  trfbas  23962  fbunfip  23987  ufileu  24037  cfinufil  24046  fmid  24078  txflf  24124  fclsrest  24142  alexsubALT  24169  tsmsres  24262  ucnima  24398  fmucndlem  24408  bldisj  24516  xmeter  24551  elbl4  24681  restmetu  24688  dscopn  24691  bl2ioo  24910  isphtpc  25114  tcphcph  25357  lmmbr2  25379  lmmbrf  25382  iscau2  25397  iscauf  25400  caucfil  25403  metcld  25426  metcld2  25427  bcthlem1  25444  bcthlem4  25447  cldcss2  25562  ovolgelb  25600  ovoliunlem1  25622  ismbfcn  25749  mbfmax  25769  mbfimaopnlem  25775  i1faddlem  25813  i1fmullem  25814  i1fres  25825  i1fpos  25826  itg1climres  25834  xrge0f  25851  itgresr  25899  iblcnlem1  25908  limcun  26015  dvres  26031  mdegmullem  26196  r1pid2  26280  ply1remlem  26283  plyremlem  26426  vieta1  26434  ulmcau  26516  sineq0  26647  coseq1  26648  ang180lem3  26934  cubic  26972  atandm  26999  atandm2  27000  atandm3  27001  rlimcnp  27088  rlimcnp2  27089  vmappw  27238  dchrelbas3  27360  dchrelbas4  27365  dchrsum2  27390  bposlem6  27411  2sqreuopltb  27587  2sqreuopnnltb  27589  dchrisumlem3  27613  pntleml  27733  noetasuplem4  27858  noetainflem4  27862  rightge0  27972  addsrid  28115  negleft  28209  negright  28210  mulsrid  28264  mulsne0bd  28337  oniso  28422  om2noseqf1o  28452  zn0subs  28554  avglts1d  28604  avglts2d  28605  istrkg3ld  28688  tgcgr4  28758  lnrot2  28851  islnopp  28970  islmib  29039  mptelee  29153  brbtwn2  29164  axsegconlem6  29181  axsegcon  29186  ax5seg  29197  axpasch  29200  axeuclid  29222  axcontlem4  29226  elntg2  29244  issubgr  29530  nb3gr2nb  29643  uhgrvd00  29793  isrusgr0  29825  wlkcpr  29887  wlkcomp  29889  upgr2wlk  29925  upgrf1istrl  29960  clwlkcomp  30037  clwlkcompbp  30040  iswwlksnx  30098  wspthsnwspthsnon  30174  wspniunwspnon  30181  2pthon3v  30201  usgr2wspthons3  30225  usgr2wspthon  30226  rusgrnumwwlks  30235  clwlkclwwlklem3  30261  clwlkclwwlk  30262  clwwlknonwwlknonb  30366  0pth  30385  eupth2lem2  30479  vdgn1frgrv2  30556  fusgreg2wsp  30596  clwwlknonclwlknonf1o  30622  dlwwlknondlwlknonf1o  30625  wlkl0  30627  nmoolb  31032  nmlno0lem  31054  ubthlem1  31131  ocsh  31544  shle0  31703  eigrei  32095  adjeu  32150  nmoplb  32168  nmfnlb  32185  eleigvec2  32219  nmlnop0iALT  32256  cnlnadjlem5  32332  adjbdln  32344  jplem2  32530  cvbr2  32544  mdsl2bi  32584  chrelat3  32632  eqelbid  32731  sq2reunnltb  32741  rmounid  32751  nelpr  32787  disjunsn  32849  ofpreima  32922  funcnv5mpt  32924  dfcnv2  32932  suppiniseg  32943  gtiso  32958  fpwrelmap  32990  infxrge0glb  33022  xrdifh  33037  fzsplit3  33050  fzo0opth  33060  swrdrn3  33188  toslublem  33205  tosglblem  33207  mgcval  33220  mndlrinvb  33258  xrge0tsmsbi  33307  cntzun  33312  isarchi  33415  dvdsrspss  33616  rspsnasso  33617  lsmsnorb  33620  nsgqusf1olem2  33639  ressply1mon1p  33775  constrfin  34053  smatrcl  34103  ist0cld  34140  rspectopn  34174  zarcls  34181  rhmpreimacnlem  34191  unitdivcld  34208  lmxrge0  34259  isrrext  34307  issibf  34640  eulerpartlemr  34681  eulerpartlemmf  34682  eulerpartlemn  34688  dstfrvunirn  34782  ballotlemfc0  34800  ballotlemfcc  34801  reprsuc  34919  reprpmtf1o  34930  reprdifc  34931  bnj919  35073  bnj976  35083  bnj1542  35162  bnj150  35181  bnj151  35182  bnj607  35221  bnj852  35226  bnj873  35229  bnj938  35242  bnj1171  35305  bnj1388  35338  bnj1489  35361  nummin  35399  usgrgt2cycl  35493  subfacp1lem3  35545  subfacp1lem5  35547  erdszelem9  35562  kur14  35579  iscvm  35622  satf0op  35740  mclsax  35932  rexxfr3dALT  36002  elintfv  36128  fundmpss  36130  opelco3  36138  dfon2  36153  dfbigcup2  36260  sscoid  36274  funpartfv  36308  dfrdg4  36314  cgr3permute3  36410  segletr  36477  segleantisym  36478  seglelin  36479  fneval  36725  neibastop3  36735  eltail  36747  filnetlem4  36754  mh-infprim2bi  36920  bj-hbntbi  37191  bj-equsvt  37258  bj-sbceqgALT  37399  bj-clel3gALT  37545  bj-rest10  37590  bj-0int  37603  qdiffALT  37832  topdifinffinlem  37853  isbasisrelowllem1  37861  isbasisrelowllem2  37862  rdgeqoa  37876  finxpreclem4  37900  finxpsuclem  37903  wl-ifp4impr  37973  wl-1xor  37988  uncf  38110  phpreu  38115  cos2h  38122  tan2h  38123  matunitlindflem1  38127  poimirlem16  38147  poimirlem19  38150  poimirlem23  38154  poimirlem24  38155  poimirlem26  38157  poimirlem27  38158  mbfposadd  38178  cnambfre  38179  itg2addnclem  38182  itg2addnc  38185  iblabsnclem  38194  ftc1anclem1  38204  ftc1anclem5  38208  caures  38271  heiborlem3  38324  heiborlem10  38331  elghomOLD  38398  divrngidl  38539  eqrelf  38769  brvbrvvdif  38780  elrnres  38789  eldmres3  38794  eldmqsres2  38805  exanres  38812  relcnveq  38839  iss2  38855  ecinn0  38864  raldmqsmo  38874  brxrn2  38895  ecxrn  38917  ecxrn2  38919  disjressuc2  38922  elrelsrel  38953  eldmcoss2  39060  eldm1cossres  39061  elrelscnveq  39139  elcoeleqvrelsrel  39191  brredundsredund  39222  brdmqssqs  39242  cnvepresdmqss  39248  eldmqs1cossres  39255  brerser  39273  erimeq2  39274  eleldisjseldisj  39340  prtlem10  39501  prtlem16  39505  prtlem19  39514  prtex  39516  prter3  39518  islshpat  39653  lcvbr2  39658  lcvbr3  39659  lshpsmreu  39745  isat3  39943  hlrelat5N  40037  islpln5  40171  cdlemblem  40429  paddvaln0N  40437  paddval0  40446  cdlemefrs29bpre1  41033  cdlemefrs29cpre1  41034  cdlemg27b  41332  cdlemg33c  41344  cdlemg33e  41346  diaglbN  41691  cdlemm10N  41754  dicopelval2  41817  dicelval2N  41818  dihopelvalcpre  41884  dihglbcpreN  41936  dih1dimatlem  41965  dihatexv  41974  dvh4dimlem  42079  mapdpglem3  42311  hdmap14lem13  42516  hdmapglem7a  42563  eluzp1  42928  fsuppind  43184  isnacs2  43299  rabrenfdioph  43403  expdiophlem1  43610  pw2f1ocnv  43626  pwfi2f1o  43685  numinfctb  43692  dfacbasgrp  43697  islnr3  43704  onsupneqmaxlim0  43813  onsupnmax  43817  onsupuni  43818  tfsconcatrnss  43939  safesnsupfilb  44006  dfhe3  44363  clsk3nimkb  44628  ntrneiiso  44679  ntrneikb  44682  mnuunid  44851  hashnzfzclim  44896  dvconstbi  44908  sbcoreleleqVD  45432  trfr  45536  permac8prim  45588  rfcnpre3  45611  rfcnpre4  45612  r19.3rzf  45734  cncfshift  46446  stoweidlem59  46631  chnsubseqwl  47453  dfafv23  47845  nelbrnel  47868  elsetpreimafvrab  47998  iccpartiun  48038  prproropf1olem0  48106  prprelb  48120  prprspr2  48122  reuprpr  48127  oddm1evenALTV  48295  oddp1evenALTV  48296  oddprmne2  48335  fpprel  48348  dfvopnbgr2  48473  uhgrimisgrgric  48551  isgrlim  48602  gpg5nbgrvtx03starlem1  48688  gpg5nbgrvtx03starlem3  48690  gpg5nbgrvtx13starlem1  48691  gpg5nbgrvtx13starlem3  48693  iscmgmALT  48844  iscsgrpALT  48846  mofeu  49477  iscnrm3  49581  joindm2  49597  meetdm2  49599  oppcendc  49647  0funcg  49714  0funcALT  49717  istermc  50103  functermc2  50138  fulltermc  50140  elpglem2  50341