Theorem bitr4di 290

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  3bitr4g  315  bibi2i  338  mtt  365  nbn2  371  ifptru  1080  3bior1fd  1483  3biant1d  1486  clel4g  3608  eueq3  3659  sbceqal  3791  eqrrabd  4024  n0moeu  4294  sbcel12  4346  sbceqg  4347  sbcne12  4350  reldisj  4388  raldifeq  4428  r19.3rz  4436  eldifpr  4597  reusngf  4613  rexreusng  4618  eldiftp  4626  eqsndOLD  4769  reusv2lem5  5338  prelpw  5392  otthg  5432  2rbropap  5513  rabxp  5673  pwvrel  5675  ssrel3  5736  elrng  5840  iss  5994  idrefALT  6070  xpcan  6134  xpcan2  6135  dfpo2  6254  ordelpss  6345  fcnvres  6711  dffv3  6830  funimass4  6898  unima  6909  funcnvmpt  6944  fndmdif  6990  fneqeql  6994  funimass3  7002  elrnrexdmb  7038  dff4  7049  fnsnbg  7115  fnsnbOLD  7117  fconst4  7165  elunirn  7202  f12dfv  7224  riota1  7341  riota2df  7343  f1ocnvfv3  7358  eqfnov  7492  elrnmpores  7501  caoftrn  7668  ordsucun  7772  dflim3  7794  dfom2  7815  peano5  7840  opiota  8008  frxp2  8091  xpord2pred  8092  xpord2indlem  8094  suppssr  8142  mpoxopovel  8167  brtpos  8182  rntpos  8186  ordgt0ge1  8425  ondif2  8434  oelim2  8528  omabs  8584  naddrid  8616  iiner  8733  erinxp  8735  qliftfun  8746  mapdm0  8786  ordunifi  9197  elfi2  9324  elfiun  9340  fifo  9342  noinfep  9579  cantnflem1  9608  cantnf  9612  rankonidlem  9750  r1pwALT  9768  cardalephex  10010  alephinit  10015  dfac5lem4OLD  10048  cflim2  10183  cfsmolem  10190  compssiso  10294  fin1a2lem11  10330  itunisuc  10339  axdclem  10439  brdom6disj  10452  alephreg  10503  fpwwe2lem8  10559  pwfseqlem3  10581  indpi  10828  nqereu  10850  ordpinq  10864  ltanq  10892  ltmnq  10893  suplem2pr  10974  map2psrpr  11031  ssxr  11213  leltne  11233  ltneg  11648  leneg  11651  suprnub  12119  negiso  12134  elnnnn0  12478  nn0sub  12485  fcdmnn0fsupp  12493  zrevaddcl  12570  znnsub  12571  znn0sub  12572  prime  12608  eluz2  12792  indstr  12864  eluz2b1  12867  qrevaddcl  12919  rpneg  12974  xrleltne  13094  dfle2  13096  dflt2  13097  supxrleub  13276  infxrgelb  13286  ixxin  13313  iccid  13341  elicopnf  13396  iccsplit  13436  fzsplit2  13501  fzsn  13518  fzpr  13531  uzsplit  13548  preduz  13602  fvinim0ffz  13742  injresinj  13744  om2uzf1oi  13913  lt2sqi  14149  le2sqi  14150  hashsdom  14341  hashf1lem1  14415  fz1isolem  14421  prprrab  14433  ccatlcan  14678  ccatrcan  14679  s3eq3seq  14899  2swrd2eqwrdeq  14913  trclfvcotr  14969  cnpart  15200  limsuplt  15439  rlimresb  15525  mertenslem2  15848  fprod2dlem  15943  sadadd2lem2  16417  saddisjlem  16431  bitsuz  16441  gcddiv  16518  algcvgblem  16544  isprm3  16650  isprm5  16675  prmreclem5  16889  vdwapun  16943  vdwmc2  16948  ramcl  16998  pwsle  17454  ismre  17550  mreacs  17622  acsfn  17623  iscatd2  17645  cidpropd  17674  dfiso2  17737  oppcsect2  17744  isfunc  17829  setcinv  18055  lubeldm  18315  lubval  18318  glbeldm  18328  glbval  18331  tosso  18381  ipodrsfi  18503  acsfiindd  18517  submgmacs  18683  imasmnd2  18740  ismhm0  18756  resmndismnd  18774  submacs  18793  imasgrp2  19029  issubg  19100  resgrpisgrp  19121  subgacs  19134  eqgval  19150  ghmqusnsglem1  19253  ghmquskerlem1  19256  gaorber  19281  symgfix2  19389  psgnran  19488  isslw  19581  sylow2alem2  19591  sylow2a  19592  sylow3lem6  19605  efgcpbllemb  19728  prmcyg  19867  gsum2d2lem  19946  gsumcom2  19948  subgdmdprd  20009  dprd2d2  20019  pgpfac1lem2  20050  pgpfac1lem4  20053  imasrng  20156  imasring  20308  isrnghmmul  20420  isnzr2  20497  isdomn3  20694  drngmulne0  20741  subrgacs  20779  sdrgacs  20780  lssle0  20947  lssacs  20964  lssats2  20997  lvecvsn0  21109  islpir  21328  zndvds  21531  znleval  21536  znleval2  21537  lindsmm  21810  islinds3  21816  islindf4  21820  ismhp3  22137  psdmul  22161  eltg2b  22949  discld  23079  opnssneib  23105  cldlp  23140  restbas  23148  leordtvallem1  23200  leordtvallem2  23201  ssidcn  23245  cnprest2  23280  lmss  23288  perfcls  23355  cmpfi  23398  1stccnp  23452  subislly  23471  hausmapdom  23490  locfindis  23520  iskgen3  23539  kgencn  23546  ptpjpre1  23561  xkoccn  23609  txrest  23621  txlm  23638  txkgen  23642  xkopt  23645  xkoinjcn  23677  imasnopn  23680  imasncld  23681  imasncls  23682  qtopcn  23704  kqfeq  23714  isr0  23727  fbfinnfr  23831  trfbas  23834  fbunfip  23859  ufileu  23909  cfinufil  23918  fmid  23950  txflf  23996  fclsrest  24014  alexsubALT  24041  tsmsres  24134  ucnima  24270  fmucndlem  24280  bldisj  24388  xmeter  24423  elbl4  24553  restmetu  24560  dscopn  24563  bl2ioo  24782  isphtpc  24986  tcphcph  25229  lmmbr2  25251  lmmbrf  25254  iscau2  25269  iscauf  25272  caucfil  25275  metcld  25298  metcld2  25299  bcthlem1  25316  bcthlem4  25319  cldcss2  25434  ovolgelb  25472  ovoliunlem1  25494  ismbfcn  25621  mbfmax  25641  mbfimaopnlem  25647  i1faddlem  25685  i1fmullem  25686  i1fres  25697  i1fpos  25698  itg1climres  25706  xrge0f  25723  itgresr  25771  iblcnlem1  25780  limcun  25887  dvres  25903  mdegmullem  26068  r1pid2  26152  ply1remlem  26155  plyremlem  26295  vieta1  26303  ulmcau  26385  sineq0  26513  coseq1  26514  ang180lem3  26800  cubic  26838  atandm  26865  atandm2  26866  atandm3  26867  rlimcnp  26954  rlimcnp2  26955  vmappw  27104  dchrelbas3  27226  dchrelbas4  27231  dchrsum2  27256  bposlem6  27277  2sqreuopltb  27453  2sqreuopnnltb  27455  dchrisumlem3  27479  pntleml  27599  noetasuplem4  27725  noetainflem4  27729  rightge0  27838  addsrid  27981  negleft  28075  negright  28076  mulsrid  28130  mulsne0bd  28203  oniso  28288  om2noseqf1o  28318  zn0subs  28420  avglts1d  28470  avglts2d  28471  istrkg3ld  28554  tgcgr4  28624  lnrot2  28717  islnopp  28832  islmib  28880  mptelee  28988  brbtwn2  28999  axsegconlem6  29016  axsegcon  29021  ax5seg  29032  axpasch  29035  axeuclid  29057  axcontlem4  29061  elntg2  29079  issubgr  29365  nb3gr2nb  29478  uhgrvd00  29628  isrusgr0  29660  wlkcpr  29722  wlkcomp  29724  upgr2wlk  29760  upgrf1istrl  29795  clwlkcomp  29872  clwlkcompbp  29875  iswwlksnx  29933  wspthsnwspthsnon  30009  wspniunwspnon  30016  2pthon3v  30036  usgr2wspthons3  30060  usgr2wspthon  30061  rusgrnumwwlks  30070  clwlkclwwlklem3  30096  clwlkclwwlk  30097  clwwlknonwwlknonb  30201  0pth  30220  eupth2lem2  30314  vdgn1frgrv2  30391  fusgreg2wsp  30431  clwwlknonclwlknonf1o  30457  dlwwlknondlwlknonf1o  30460  wlkl0  30462  nmoolb  30867  nmlno0lem  30889  ubthlem1  30966  ocsh  31379  shle0  31538  eigrei  31930  adjeu  31985  nmoplb  32003  nmfnlb  32020  eleigvec2  32054  nmlnop0iALT  32091  cnlnadjlem5  32167  adjbdln  32179  jplem2  32365  cvbr2  32379  mdsl2bi  32419  chrelat3  32467  eqelbid  32569  sq2reunnltb  32579  rmounid  32589  nelpr  32626  disjunsn  32690  ofpreima  32764  funcnv5mpt  32766  dfcnv2  32774  suppiniseg  32785  gtiso  32800  fpwrelmap  32832  infxrge0glb  32864  xrdifh  32879  fzsplit3  32892  fzo0opth  32902  swrdrn3  33041  toslublem  33058  tosglblem  33060  mgcval  33073  mndlrinvb  33111  xrge0tsmsbi  33162  cntzun  33167  isarchi  33270  dvdsrspss  33477  rspsnasso  33478  lsmsnorb  33481  nsgqusf1olem2  33504  isprmidl  33528  ressply1mon1p  33658  r1pid2OLD  33699  constrfin  33937  smatrcl  33987  ist0cld  34024  rspectopn  34058  zarcls  34065  rhmpreimacnlem  34075  unitdivcld  34092  lmxrge0  34143  isrrext  34191  issibf  34524  eulerpartlemr  34565  eulerpartlemmf  34566  eulerpartlemn  34572  dstfrvunirn  34666  ballotlemfc0  34684  ballotlemfcc  34685  reprsuc  34806  reprpmtf1o  34817  reprdifc  34818  bnj919  34957  bnj976  34967  bnj1542  35046  bnj150  35065  bnj151  35066  bnj607  35105  bnj852  35110  bnj873  35113  bnj938  35126  bnj1171  35189  bnj1388  35222  bnj1489  35245  nummin  35283  usgrgt2cycl  35359  subfacp1lem3  35411  subfacp1lem5  35413  erdszelem9  35428  kur14  35445  iscvm  35488  satf0op  35606  mclsax  35798  rexxfr3dALT  35868  elintfv  35994  fundmpss  35996  opelco3  36004  dfon2  36019  dfbigcup2  36126  sscoid  36140  funpartfv  36174  dfrdg4  36180  cgr3permute3  36276  segletr  36343  segleantisym  36344  seglelin  36345  fneval  36581  neibastop3  36591  eltail  36603  filnetlem4  36610  mh-infprim2bi  36776  bj-hbntbi  37048  bj-equsvt  37115  bj-sbceqgALT  37256  bj-clel3gALT  37402  bj-rest10  37447  bj-0int  37460  qdiffALT  37689  topdifinffinlem  37710  isbasisrelowllem1  37718  isbasisrelowllem2  37719  rdgeqoa  37733  finxpreclem4  37757  finxpsuclem  37760  wl-ifp4impr  37830  wl-1xor  37845  uncf  37967  phpreu  37972  cos2h  37979  tan2h  37980  matunitlindflem1  37984  poimirlem16  38004  poimirlem19  38007  poimirlem23  38011  poimirlem24  38012  poimirlem26  38014  poimirlem27  38015  mbfposadd  38035  cnambfre  38036  itg2addnclem  38039  itg2addnc  38042  iblabsnclem  38051  ftc1anclem1  38061  ftc1anclem5  38065  caures  38128  heiborlem3  38181  heiborlem10  38188  elghomOLD  38255  divrngidl  38396  eqrelf  38626  brvbrvvdif  38637  elrnres  38646  eldmres3  38651  eldmqsres2  38662  exanres  38669  relcnveq  38696  iss2  38712  ecinn0  38721  raldmqsmo  38731  brxrn2  38752  ecxrn  38774  ecxrn2  38776  disjressuc2  38779  elrelsrel  38810  eldmcoss2  38917  eldm1cossres  38918  elrelscnveq  38996  elcoeleqvrelsrel  39048  brredundsredund  39079  brdmqssqs  39099  cnvepresdmqss  39105  eldmqs1cossres  39112  brerser  39130  erimeq2  39131  eleldisjseldisj  39197  prtlem10  39358  prtlem16  39362  prtlem19  39371  prtex  39373  prter3  39375  islshpat  39510  lcvbr2  39515  lcvbr3  39516  lshpsmreu  39602  isat3  39800  hlrelat5N  39894  islpln5  40028  cdlemblem  40286  paddvaln0N  40294  paddval0  40303  cdlemefrs29bpre1  40890  cdlemefrs29cpre1  40891  cdlemg27b  41189  cdlemg33c  41201  cdlemg33e  41203  diaglbN  41548  cdlemm10N  41611  dicopelval2  41674  dicelval2N  41675  dihopelvalcpre  41741  dihglbcpreN  41793  dih1dimatlem  41822  dihatexv  41831  dvh4dimlem  41936  mapdpglem3  42168  hdmap14lem13  42373  hdmapglem7a  42420  eluzp1  42785  fsuppind  43041  isnacs2  43156  rabrenfdioph  43260  expdiophlem1  43467  pw2f1ocnv  43483  pwfi2f1o  43542  numinfctb  43549  dfacbasgrp  43554  islnr3  43561  onsupneqmaxlim0  43670  onsupnmax  43674  onsupuni  43675  tfsconcatrnss  43796  safesnsupfilb  43863  dfhe3  44220  clsk3nimkb  44485  ntrneiiso  44536  ntrneikb  44539  scottabf  44685  mnuunid  44722  hashnzfzclim  44767  dvconstbi  44779  sbcoreleleqVD  45303  trfr  45407  permac8prim  45459  rfcnpre3  45482  rfcnpre4  45483  r19.3rzf  45606  cncfshift  46318  stoweidlem59  46503  chnsubseqwl  47325  dfafv23  47717  nelbrnel  47740  elsetpreimafvrab  47870  iccpartiun  47910  prproropf1olem0  47978  prprelb  47992  prprspr2  47994  reuprpr  47999  oddm1evenALTV  48167  oddp1evenALTV  48168  oddprmne2  48207  fpprel  48220  dfvopnbgr2  48345  uhgrimisgrgric  48423  isgrlim  48474  gpg5nbgrvtx03starlem1  48560  gpg5nbgrvtx03starlem3  48562  gpg5nbgrvtx13starlem1  48563  gpg5nbgrvtx13starlem3  48565  iscmgmALT  48716  iscsgrpALT  48718  mofeu  49339  iscnrm3  49443  joindm2  49459  meetdm2  49461  oppcendc  49509  0funcg  49576  0funcALT  49579  istermc  49965  functermc2  50000  fulltermc  50002  elpglem2  50203