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  1504  3biant1d  1507  clel4g  3621  eueq3  3673  sbceqal  3804  eqrrabd  4039  n0moeu  4313  sbcel12  4375  sbceqg  4376  sbcne12  4379  reldisj  4412  raldifeq  4453  r19.3rz  4461  eldifpr  4623  reusngf  4639  rexreusng  4644  eldiftp  4652  reusv2lem5  5373  prelpw  5427  otthg  5467  2rbropap  5549  rabxp  5709  pwvrel  5711  ssrel3  5772  elrng  5881  iss  6037  idrefALT  6113  xpcan  6174  xpcan2  6175  dfpo2  6297  ordelpss  6388  fcnvres  6755  dffv3  6877  funimass4  6945  unima  6956  funcnvmpt  6991  fndmdif  7037  fneqeql  7041  funimass3  7049  elrnrexdmb  7085  dff4  7096  fnsnbg  7162  fnsnbOLD  7164  fconst4  7212  elunirn  7249  f12dfv  7271  riota1  7388  riota2df  7390  f1ocnvfv3  7405  eqfnov  7539  elrnmpores  7548  caoftrn  7715  ordsucun  7820  dflim3  7842  dfom2  7863  peano5  7889  opiota  8055  frxp2  8139  xpord2pred  8140  xpord2indlem  8142  suppssr  8190  mpoxopovel  8215  brtpos  8230  rntpos  8234  ordgt0ge1  8477  ondif2  8486  oelim2  8580  omabs  8636  naddrid  8669  iiner  8786  erinxp  8788  qliftfun  8799  mapdm0  8838  ordunifi  9249  elfi2  9373  elfiun  9389  fifo  9391  noinfep  9628  cantnflem1  9657  cantnf  9661  rankonidlem  9799  r1pwALT  9817  scottabf  9865  cardalephex  10073  alephinit  10078  cflim2  10246  cfsmolem  10253  compssiso  10357  fin1a2lem11  10393  itunisuc  10402  axdclem  10502  brdom6disj  10515  alephreg  10566  fpwwe2lem8  10622  pwfseqlem3  10644  indpi  10891  nqereu  10913  ordpinq  10927  ltanq  10955  ltmnq  10956  suplem2pr  11037  map2psrpr  11094  ssxr  11278  leltne  11298  ltneg  11713  leneg  11716  suprnub  12179  negiso  12194  elnnnn0  12546  nn0sub  12553  fcdmnn0fsupp  12561  zrevaddcl  12638  znnsub  12639  znn0sub  12640  prime  12676  eluz2  12867  indstr  12939  eluz2b1  12942  qrevaddcl  12994  rpneg  13049  xrleltne  13169  dfle2  13171  dflt2  13172  supxrleub  13351  infxrgelb  13361  ixxin  13388  iccid  13416  elicopnf  13471  iccsplit  13511  fzsplit2  13577  fzsn  13594  fzpr  13607  uzsplit  13624  preduz  13678  fvinim0ffz  13818  injresinj  13820  om2uzf1oi  13989  lt2sqi  14225  le2sqi  14226  hashsdom  14417  hashf1lem1  14492  fz1isolem  14498  prprrab  14510  ccatlcan  14755  ccatrcan  14756  s3eq3seq  14976  2swrd2eqwrdeq  14990  trclfvcotr  15046  cnpart  15291  limsuplt  15530  rlimresb  15616  mertenslem2  15939  fprod2dlem  16034  sadadd2lem2  16507  saddisjlem  16521  bitsuz  16531  gcddiv  16608  algcvgblem  16634  isprm3  16740  isprm5  16765  prmreclem5  16979  vdwapun  17033  vdwmc2  17038  ramcl  17088  pwsle  17545  ismre  17641  mreacs  17713  acsfn  17714  iscatd2  17736  cidpropd  17765  dfiso2  17828  oppcsect2  17835  isfunc  17920  setcinv  18146  lubeldm  18406  lubval  18409  glbeldm  18419  glbval  18422  tosso  18472  ipodrsfi  18594  acsfiindd  18608  submgmacs  18774  imasmnd2  18831  ismhm0  18847  resmndismnd  18865  submacs  18885  imasgrp2  19120  issubg  19191  resgrpisgrp  19213  subgacs  19226  eqgval  19244  ghmqusnsglem1  19349  ghmquskerlem1  19352  gaorber  19377  symgfix2  19485  psgnran  19584  isslw  19677  sylow2alem2  19687  sylow2a  19688  sylow3lem6  19701  efgcpbllemb  19824  prmcyg  19963  gsum2d2lem  20042  gsumcom2  20044  subgdmdprd  20105  dprd2d2  20115  pgpfac1lem2  20146  pgpfac1lem4  20149  imasrng  20254  imasring  20411  isrnghmmul  20523  isnzr2  20600  isdomn3  20798  drngmulne0  20845  subrgacs  20882  sdrgacs  20883  lssle0  21050  lssacs  21067  lssats2  21100  lvecvsn0  21212  rspsn0  21351  isprmidl  21442  islpir  21475  zndvds  21678  znleval  21683  znleval2  21684  lindsmm  21957  islinds3  21963  islindf4  21967  ismhp3  22284  psdmul  22308  eltg2b  23095  discld  23225  opnssneib  23251  cldlp  23286  restbas  23294  leordtvallem1  23346  leordtvallem2  23347  ssidcn  23391  cnprest2  23426  lmss  23434  perfcls  23501  cmpfi  23544  1stccnp  23598  subislly  23617  hausmapdom  23636  locfindis  23666  iskgen3  23685  kgencn  23692  ptpjpre1  23707  xkoccn  23755  txrest  23767  txlm  23784  txkgen  23788  xkopt  23791  xkoinjcn  23823  imasnopn  23826  imasncld  23827  imasncls  23828  qtopcn  23850  kqfeq  23860  isr0  23873  fbfinnfr  23977  trfbas  23980  fbunfip  24005  ufileu  24055  cfinufil  24064  fmid  24096  txflf  24142  fclsrest  24160  alexsubALT  24187  tsmsres  24280  ucnima  24416  fmucndlem  24426  bldisj  24534  xmeter  24569  elbl4  24699  restmetu  24706  dscopn  24709  bl2ioo  24928  isphtpc  25132  tcphcph  25375  lmmbr2  25397  lmmbrf  25400  iscau2  25415  iscauf  25418  caucfil  25421  metcld  25444  metcld2  25445  bcthlem1  25462  bcthlem4  25465  cldcss2  25580  ovolgelb  25618  ovoliunlem1  25640  ismbfcn  25767  mbfmax  25787  mbfimaopnlem  25793  i1faddlem  25831  i1fmullem  25832  i1fres  25843  i1fpos  25844  itg1climres  25852  xrge0f  25869  itgresr  25917  iblcnlem1  25926  limcun  26033  dvres  26049  mdegmullem  26214  r1pid2  26298  ply1remlem  26301  plyremlem  26444  vieta1  26452  ulmcau  26534  sineq0  26665  coseq1  26666  ang180lem3  26952  cubic  26990  atandm  27017  atandm2  27018  atandm3  27019  rlimcnp  27106  rlimcnp2  27107  vmappw  27256  dchrelbas3  27378  dchrelbas4  27383  dchrsum2  27408  bposlem6  27429  2sqreuopltb  27605  2sqreuopnnltb  27607  dchrisumlem3  27631  pntleml  27751  noetasuplem4  27876  noetainflem4  27880  rightge0  27990  addsrid  28133  negleft  28227  negright  28228  mulsrid  28282  mulsne0bd  28355  oniso  28440  om2noseqf1o  28470  zn0subs  28572  avglts1d  28622  avglts2d  28623  istrkg3ld  28706  tgcgr4  28776  lnrot2  28873  islnopp  28995  islmib  29070  mptelee  29210  brbtwn2  29221  axsegconlem6  29238  axsegcon  29243  ax5seg  29254  axpasch  29257  axeuclid  29279  axcontlem4  29283  elntg2  29301  issubgr  29587  nb3gr2nb  29700  uhgrvd00  29850  isrusgr0  29882  wlkcpr  29944  wlkcomp  29946  upgr2wlk  29982  upgrf1istrl  30017  clwlkcomp  30094  clwlkcompbp  30097  iswwlksnx  30155  wspthsnwspthsnon  30231  wspniunwspnon  30238  2pthon3v  30258  usgr2wspthons3  30282  usgr2wspthon  30283  rusgrnumwwlks  30292  clwlkclwwlklem3  30318  clwlkclwwlk  30319  clwwlknonwwlknonb  30423  0pth  30442  eupth2lem2  30536  vdgn1frgrv2  30613  fusgreg2wsp  30653  clwwlknonclwlknonf1o  30679  dlwwlknondlwlknonf1o  30682  wlkl0  30684  nmoolb  31089  nmlno0lem  31111  ubthlem1  31188  ocsh  31601  shle0  31760  eigrei  32152  adjeu  32207  nmoplb  32225  nmfnlb  32242  eleigvec2  32276  nmlnop0iALT  32313  cnlnadjlem5  32389  adjbdln  32401  jplem2  32587  cvbr2  32601  mdsl2bi  32641  chrelat3  32689  eqelbid  32787  sq2reunnltb  32797  rmounid  32807  nelpr  32843  disjunsn  32905  ofpreima  32976  funcnv5mpt  32978  dfcnv2  32986  suppiniseg  32997  gtiso  33012  fpwrelmap  33044  infxrge0glb  33076  xrdifh  33091  fzsplit3  33104  fzo0opth  33114  swrdrn3  33241  toslublem  33258  tosglblem  33260  mgcval  33273  mndlrinvb  33311  xrge0tsmsbi  33360  cntzun  33365  isarchi  33468  dvdsrspss  33666  rspsnasso  33667  lsmsnorb  33670  nsgqusf1olem2  33689  ressply1mon1p  33824  constrfin  34102  smatrcl  34152  ist0cld  34189  rspectopn  34223  zarcls  34230  rhmpreimacnlem  34240  unitdivcld  34257  lmxrge0  34308  isrrext  34356  issibf  34689  eulerpartlemr  34730  eulerpartlemmf  34731  eulerpartlemn  34737  dstfrvunirn  34831  ballotlemfc0  34849  ballotlemfcc  34850  reprsuc  34968  reprpmtf1o  34979  reprdifc  34980  bnj919  35122  bnj976  35132  bnj1542  35211  bnj150  35230  bnj151  35231  bnj607  35270  bnj852  35275  bnj873  35278  bnj938  35291  bnj1171  35354  bnj1388  35387  bnj1489  35410  nummin  35450  dfscott3  35478  usgrgt2cycl  35588  subfacp1lem3  35640  subfacp1lem5  35642  erdszelem9  35657  kur14  35674  iscvm  35717  satf0op  35835  mclsax  36027  rexxfr3dALT  36097  elintfv  36223  fundmpss  36225  opelco3  36233  dfon2  36248  dfbigcup2  36355  sscoid  36369  funpartfv  36403  dfrdg4  36409  cgr3permute3  36505  segletr  36572  segleantisym  36573  seglelin  36574  nmulrid  36663  fneval  36829  neibastop3  36839  eltail  36851  filnetlem4  36858  mh-infprim2bi  37024  bj-hbntbi  37295  bj-equsvt  37362  bj-sbceqgALT  37503  bj-clel3gALT  37650  bj-rest10  37696  bj-0int  37709  qdiffALT  37938  topdifinffinlem  37959  isbasisrelowllem1  37967  isbasisrelowllem2  37968  rdgeqoa  37982  finxpreclem4  38006  finxpsuclem  38009  wl-ifp4impr  38079  wl-1xor  38094  uncf  38216  phpreu  38221  cos2h  38228  tan2h  38229  matunitlindflem1  38233  poimirlem16  38253  poimirlem19  38256  poimirlem23  38260  poimirlem24  38261  poimirlem26  38263  poimirlem27  38264  mbfposadd  38284  cnambfre  38285  itg2addnclem  38288  itg2addnc  38291  iblabsnclem  38300  ftc1anclem1  38310  ftc1anclem5  38314  caures  38377  heiborlem3  38430  heiborlem10  38437  elghomOLD  38504  divrngidl  38645  eqrelf  38875  brvbrvvdif  38886  elrnres  38895  eldmres3  38900  eldmqsres2  38911  exanres  38918  relcnveq  38945  iss2  38961  ecinn0  38970  raldmqsmo  38980  brxrn2  39001  ecxrn  39023  ecxrn2  39025  disjressuc2  39028  elrelsrel  39059  eldmcoss2  39166  eldm1cossres  39167  elrelscnveq  39245  elcoeleqvrelsrel  39297  brredundsredund  39328  brdmqssqs  39348  cnvepresdmqss  39354  eldmqs1cossres  39361  brerser  39379  erimeq2  39380  eleldisjseldisj  39446  prtlem10  39607  prtlem16  39611  prtlem19  39620  prtex  39622  prter3  39624  islshpat  39759  lcvbr2  39764  lcvbr3  39765  lshpsmreu  39851  isat3  40049  hlrelat5N  40143  islpln5  40277  cdlemblem  40535  paddvaln0N  40543  paddval0  40552  cdlemefrs29bpre1  41139  cdlemefrs29cpre1  41140  cdlemg27b  41438  cdlemg33c  41450  cdlemg33e  41452  diaglbN  41797  cdlemm10N  41860  dicopelval2  41923  dicelval2N  41924  dihopelvalcpre  41990  dihglbcpreN  42042  dih1dimatlem  42071  dihatexv  42080  dvh4dimlem  42185  mapdpglem3  42417  hdmap14lem13  42622  hdmapglem7a  42669  eluzp1  43036  fsuppind  43292  isnacs2  43407  rabrenfdioph  43511  expdiophlem1  43718  pw2f1ocnv  43734  pwfi2f1o  43793  numinfctb  43800  dfacbasgrp  43805  islnr3  43812  onsupneqmaxlim0  43921  onsupnmax  43925  onsupuni  43926  tfsconcatrnss  44047  safesnsupfilb  44114  dfhe3  44471  clsk3nimkb  44736  ntrneiiso  44787  ntrneikb  44790  mnuunid  44957  hashnzfzclim  45002  dvconstbi  45014  sbcoreleleqVD  45537  trfr  45641  permac8prim  45693  rfcnpre3  45723  rfcnpre4  45724  r19.3rzf  45846  cncfshift  46558  stoweidlem59  46743  chnsubseqwl  47565  dfafv23  47957  nelbrnel  47980  elsetpreimafvrab  48110  iccpartiun  48150  prproropf1olem0  48218  prprelb  48232  prprspr2  48234  reuprpr  48239  oddm1evenALTV  48407  oddp1evenALTV  48408  oddprmne2  48447  fpprel  48460  dfvopnbgr2  48585  uhgrimisgrgric  48663  isgrlim  48714  gpg5nbgrvtx03starlem1  48800  gpg5nbgrvtx03starlem3  48802  gpg5nbgrvtx13starlem1  48803  gpg5nbgrvtx13starlem3  48805  iscmgmALT  48956  iscsgrpALT  48958  mofeu  49593  iscnrm3  49697  joindm2  49713  meetdm2  49715  oppcendc  49763  0funcg  49830  0funcALT  49833  istermc  50219  functermc2  50254  fulltermc  50256  elpglem2  50457