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  3620  eueq3  3672  sbceqal  3803  eqrrabd  4037  n0moeu  4310  sbcel12  4372  sbceqg  4373  sbcne12  4376  reldisj  4409  raldifeq  4452  r19.3rz  4460  eldifpr  4622  reusngf  4638  rexreusng  4643  eldiftp  4651  reusv2lem5  5371  prelpw  5425  otthg  5465  2rbropap  5547  rabxp  5707  pwvrel  5709  ssrel3  5770  elrng  5879  iss  6035  idrefALT  6111  xpcan  6173  xpcan2  6174  dfpo2  6298  ordelpss  6389  fcnvres  6756  dffv3  6878  funimass4  6946  unima  6957  funcnvmpt  6992  fndmdif  7038  fneqeql  7042  funimass3  7050  elrnrexdmb  7087  dff4  7098  fnsnbg  7166  fnsnbOLD  7168  fconst4  7217  elunirn  7252  f12dfv  7278  riota1  7395  riota2df  7397  f1ocnvfv3  7412  eqfnov  7546  elrnmpores  7555  caoftrn  7723  ordsucun  7825  dflim3  7847  dfom2  7868  peano5  7894  opiota  8060  frxp2  8146  xpord2pred  8147  xpord2indlem  8149  suppssr  8197  mpoxopovel  8222  brtpos  8237  rntpos  8241  ordgt0ge1  8484  ondif2  8493  oelim2  8587  omabs  8643  naddrid  8676  iiner  8793  erinxp  8795  qliftfun  8806  mapdm0  8845  uncf  8874  ordunifi  9264  elfi2  9388  elfiun  9404  fifo  9406  noinfep  9643  cantnflem1  9672  cantnf  9676  rankonidlem  9814  r1pwALT  9832  scottabf  9882  cardalephex  10097  alephinit  10102  cflim2  10269  cfsmolem  10276  compssiso  10380  fin1a2lem11  10416  itunisuc  10425  axdclem  10525  brdom6disj  10539  alephreg  10595  fpwwe2lem8  10651  pwfseqlem3  10673  indpi  10920  nqereu  10942  ordpinq  10956  ltanq  10984  ltmnq  10985  suplem2pr  11066  map2psrpr  11123  ssxr  11307  leltne  11327  ltneg  11742  leneg  11745  suprnub  12208  negiso  12223  elnnnn0  12575  nn0sub  12582  fcdmnn0fsupp  12590  zrevaddcl  12667  znnsub  12668  znn0sub  12669  prime  12706  eluz2  12897  indstr  12969  eluz2b1  12972  qrevaddcl  13025  rpneg  13080  xrleltne  13200  dfle2  13202  dflt2  13203  supxrleub  13382  infxrgelb  13392  ixxin  13419  iccid  13447  elicopnf  13502  iccsplit  13542  fzsplit2  13608  fzsn  13625  fzpr  13638  uzsplit  13655  preduz  13709  fvinim0ffz  13849  injresinj  13851  om2uzf1oi  14021  lt2sqi  14257  le2sqi  14258  hashsdom  14449  hashf1lem1  14524  fz1isolem  14530  prprrab  14542  swrdrn3  14726  ccatlcan  14791  ccatrcan  14792  s3eq3seq  15014  2swrd2eqwrdeq  15030  trclfvcotr  15086  cnpart  15331  limsuplt  15570  rlimresb  15656  mertenslem2  15978  fprod2dlem  16073  sadadd2lem2  16546  saddisjlem  16560  bitsuz  16570  gcddiv  16647  algcvgblem  16673  isprm3  16779  isprm5  16804  prmreclem5  17018  vdwapun  17072  vdwmc2  17077  ramcl  17127  pwsle  17584  ismre  17680  mreacs  17752  acsfn  17753  iscatd2  17775  cidpropd  17804  dfiso2  17867  oppcsect2  17874  isfunc  17959  setcinv  18185  lubeldm  18445  lubval  18448  glbeldm  18458  glbval  18461  tosso  18511  ipodrsfi  18633  acsfiindd  18647  submgmacs  18825  imasmnd2  18887  ismhm0  18904  resmndismnd  18922  submacs  18942  imasgrp2  19184  issubg  19255  resgrpisgrp  19277  subgacs  19290  eqgval  19308  ghmqusnsglem1  19413  ghmquskerlem1  19416  gaorber  19441  symgfix2  19549  psgnran  19648  isslw  19741  sylow2alem2  19751  sylow2a  19752  sylow3lem6  19765  efgcpbllemb  19888  prmcyg  20027  gsum2d2lem  20106  gsumcom2  20108  subgdmdprd  20169  dprd2d2  20179  pgpfac1lem2  20210  pgpfac1lem4  20213  imasrng  20318  imasring  20477  isrnghmmul  20589  isnzr2  20684  isdomn3  20882  drngmulne0  20934  subrgacs  20972  sdrgacs  20973  lssle0  21140  lssacs  21157  lssats2  21190  lvecvsn0  21302  rspsn0  21441  isprmidl  21532  islpir  21565  zndvds  21768  znleval  21773  znleval2  21774  lindsmm  22047  islinds3  22053  islindf4  22057  ismhp3  22376  psdmul  22400  matunitlindflem1  22907  eltg2b  23190  discld  23320  opnssneib  23346  cldlp  23381  restbas  23389  leordtvallem1  23441  leordtvallem2  23442  ssidcn  23486  cnprest2  23521  lmss  23529  perfcls  23596  cmpfi  23639  1stccnp  23694  subislly  23713  hausmapdom  23732  locfindis  23762  iskgen3  23781  kgencn  23788  ptpjpre1  23803  xkoccn  23851  txrest  23863  txlm  23880  txkgen  23884  xkopt  23887  xkoinjcn  23919  imasnopn  23922  imasncld  23923  imasncls  23924  qtopcn  23946  kqfeq  23956  isr0  23969  fbfinnfr  24073  trfbas  24076  fbunfip  24101  ufileu  24151  cfinufil  24160  fmid  24192  txflf  24238  fclsrest  24256  alexsubALT  24283  tsmsres  24376  ucnima  24512  fmucndlem  24522  bldisj  24630  xmeter  24665  elbl4  24795  restmetu  24802  dscopn  24805  bl2ioo  25024  isphtpc  25228  tcphcph  25471  lmmbr2  25493  lmmbrf  25496  iscau2  25511  iscauf  25514  caucfil  25517  metcld  25540  metcld2  25541  bcthlem1  25558  bcthlem4  25561  cldcss2  25676  ovolgelb  25714  ovoliunlem1  25736  ismbfcn  25863  mbfmax  25883  mbfimaopnlem  25889  i1faddlem  25927  i1fmullem  25928  i1fres  25939  i1fpos  25940  itg1climres  25948  xrge0f  25965  itgresr  26013  iblcnlem1  26022  limcun  26129  dvres  26145  mdegmullem  26310  r1pid2  26394  ply1remlem  26397  plyremlem  26541  vieta1  26551  ulmcau  26638  sineq0  26769  coseq1  26770  ang180lem3  27056  cubic  27094  atandm  27121  atandm2  27122  atandm3  27123  rlimcnp  27210  rlimcnp2  27211  vmappw  27360  dchrelbas3  27482  dchrelbas4  27487  dchrsum2  27512  bposlem6  27533  2sqreuopltb  27709  2sqreuopnnltb  27711  dchrisumlem3  27735  pntleml  27855  noetasuplem4  27980  noetainflem4  27984  rightge0  28094  addsrid  28237  negleft  28331  negright  28332  mulsrid  28386  mulsne0bd  28459  oniso  28544  om2noseqf1o  28574  zn0subs  28676  avglts1d  28726  avglts2d  28727  istrkg3ld  28810  tgcgr4  28881  lnrot2  28979  islnopp  29102  islmib  29179  mptelee  29359  brbtwn2  29370  axsegconlem6  29387  axsegcon  29392  ax5seg  29403  axpasch  29406  axeuclid  29428  axcontlem4  29432  elntg2  29450  issubgr  29739  nb3gr2nb  29852  uhgrvd00  30002  isrusgr0  30034  wlkcpr  30096  wlkcomp  30098  upgr2wlk  30134  upgrf1istrl  30173  clwlkcomp  30253  clwlkcompbp  30256  iswwlksnx  30316  wspthsnwspthsnon  30392  wspniunwspnon  30399  2pthon3v  30419  usgr2wspthons3  30443  usgr2wspthon  30444  rusgrnumwwlks  30453  clwlkclwwlklem3  30479  clwlkclwwlk  30480  clwwlknonwwlknonb  30584  0pth  30603  eupth2lem2  30707  vdgn1frgrv2  30784  fusgreg2wsp  30824  clwwlknonclwlknonf1o  30850  dlwwlknondlwlknonf1o  30853  wlkl0  30855  nmoolb  31260  nmlno0lem  31282  ubthlem1  31359  ocsh  31772  shle0  31931  eigrei  32323  adjeu  32378  nmoplb  32396  nmfnlb  32413  eleigvec2  32447  nmlnop0iALT  32484  cnlnadjlem5  32560  adjbdln  32572  jplem2  32758  cvbr2  32772  mdsl2bi  32812  chrelat3  32860  eqelbid  32958  sq2reunnltb  32968  rmounid  32978  nelpr  33014  disjunsn  33075  ofpreima  33146  funcnv5mpt  33148  dfcnv2  33156  suppiniseg  33166  gtiso  33181  fpwrelmap  33212  infxrge0glb  33244  xrdifh  33259  fzsplit3  33272  fzo0opth  33282  toslublem  33420  tosglblem  33422  mgcval  33435  mndlrinvb  33473  xrge0tsmsbi  33522  cntzun  33527  isarchi  33630  dvdsrspss  33828  rspsnasso  33829  lsmsnorb  33832  nsgqusf1olem2  33851  ressply1mon1p  33986  constrfin  34264  smatrcl  34314  ist0cld  34351  rspectopn  34385  zarcls  34392  rhmpreimacnlem  34402  unitdivcld  34419  lmxrge0  34470  isrrext  34518  issibf  34852  eulerpartlemr  34893  eulerpartlemmf  34894  eulerpartlemn  34900  dstfrvunirn  34994  ballotlemfc0  35012  ballotlemfcc  35013  reprsuc  35131  reprpmtf1o  35142  reprdifc  35143  bnj919  35285  bnj976  35295  bnj1542  35374  bnj150  35393  bnj151  35394  bnj607  35433  bnj852  35438  bnj873  35441  bnj938  35454  bnj1171  35517  bnj1388  35550  bnj1489  35573  nummin  35606  dfscott3  35634  usgrgt2cycl  35731  subfacp1lem3  35769  subfacp1lem5  35771  erdszelem9  35786  kur14  35803  iscvm  35846  satf0op  35964  mclsax  36156  rexxfr3dALT  36226  elintfv  36352  fundmpss  36354  opelco3  36362  dfon2  36377  dfbigcup2  36484  sscoid  36498  funpartfv  36532  dfrdg4  36538  cgr3permute3  36635  segletr  36702  segleantisym  36703  seglelin  36704  nmulrid  36785  fneval  36979  neibastop3  36989  eltail  37001  filnetlem4  37008  mh-infprim2bi  37174  bj-hbntbi  37445  bj-equsvt  37512  bj-sbceqgALT  37653  bj-clel3gALT  37800  bj-rest10  37846  bj-0int  37859  qdiffALT  38088  topdifinffinlem  38109  isbasisrelowllem1  38117  isbasisrelowllem2  38118  rdgeqoa  38132  finxpreclem4  38156  finxpsuclem  38159  wl-ifp4impr  38229  wl-1xor  38244  phpreu  38366  cos2h  38373  tan2h  38374  poimirlem16  38393  poimirlem19  38396  poimirlem23  38400  poimirlem24  38401  poimirlem26  38403  poimirlem27  38404  mbfposadd  38424  cnambfre  38425  itg2addnclem  38428  itg2addnc  38431  iblabsnclem  38440  ftc1anclem1  38450  ftc1anclem5  38454  findcard4  38471  caures  38518  heiborlem3  38571  heiborlem10  38578  elghomOLD  38645  divrngidl  38786  eqrelf  39014  brvbrvvdif  39025  elrnres  39034  eldmres3  39039  eldmqsres2  39050  exanres  39057  relcnveq  39084  iss2  39100  ecinn0  39109  raldmqsmo  39119  brxrn2  39140  ecxrn  39162  ecxrn2  39164  disjressuc2  39167  elrelsrel  39198  eldmcoss2  39305  eldm1cossres  39306  elrelscnveq  39384  elcoeleqvrelsrel  39436  brredundsredund  39467  brdmqssqs  39487  cnvepresdmqss  39493  eldmqs1cossres  39500  brerser  39518  erimeq2  39519  eleldisjseldisj  39585  prtlem10  39746  prtlem16  39750  prtlem19  39759  prtex  39761  prter3  39763  islshpat  39898  lcvbr2  39903  lcvbr3  39904  lshpsmreu  39990  isat3  40188  hlrelat5N  40282  islpln5  40416  cdlemblem  40674  paddvaln0N  40682  paddval0  40691  cdlemefrs29bpre1  41278  cdlemefrs29cpre1  41279  cdlemg27b  41577  cdlemg33c  41589  cdlemg33e  41591  diaglbN  41936  cdlemm10N  41999  dicopelval2  42062  dicelval2N  42063  dihopelvalcpre  42129  dihglbcpreN  42181  dih1dimatlem  42210  dihatexv  42219  dvh4dimlem  42324  mapdpglem3  42556  hdmap14lem13  42761  hdmapglem7a  42808  eluzp1  43190  fsuppind  43444  isnacs2  43559  rabrenfdioph  43663  expdiophlem1  43870  pw2f1ocnv  43886  pwfi2f1o  43945  numinfctb  43952  dfacbasgrp  43957  islnr3  43964  onsupneqmaxlim0  44073  onsupnmax  44077  onsupuni  44078  tfsconcatrnss  44199  safesnsupfilb  44266  dfhe3  44623  clsk3nimkb  44888  ntrneiiso  44939  ntrneikb  44942  mnuunid  45109  hashnzfzclim  45154  dvconstbi  45166  sbcoreleleqVD  45689  trfr  45793  permac8prim  45845  rfcnpre3  45875  rfcnpre4  45876  r19.3rzf  45998  cncfshift  46710  stoweidlem59  46895  chnsubseqwl  47715  dfafv23  48149  nelbrnel  48172  elsetpreimafvrab  48302  iccpartiun  48342  prproropf1olem0  48410  prprelb  48424  prprspr2  48426  reuprpr  48431  oddm1evenALTV  48599  oddp1evenALTV  48600  oddprmne2  48639  fpprel  48652  dfvopnbgr2  48777  uhgrimisgrgric  48855  isgrlim  48906  gpg5nbgrvtx03starlem1  48992  gpg5nbgrvtx03starlem3  48994  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem3  48997  iscmgmALT  49147  iscsgrpALT  49149  mofeu  49784  iscnrm3  49886  joindm2  49902  meetdm2  49904  oppcendc  49952  0funcg  50019  0funcALT  50022  istermc  50408  functermc2  50443  fulltermc  50445  elpglem2  50646