Theorem biimtrdi 253

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

Ref	Expression
biimtrdi.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
biimtrdi.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
biimtrdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem biimtrdi

Step	Hyp	Ref	Expression
1		biimtrdi.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 229	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	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:  ax12i  1968  sb4a  2484  hbsb2  2486  dfsb2  2497  2eu2  2653  reu6  3672  2reu2  3836  sseq0  4343  disjel  4397  disjpss  4401  preq12b  4793  prneimg  4797  preqsnd  4802  elinti  4898  zfrepclf  5226  exnelv  5248  dtruALT2  5312  opth1g  5431  sbcop1  5441  snopeqop  5460  propeqop  5461  otsndisj  5473  otiunsndisj  5474  iunopeqop  5475  iunopeqopOLD  5476  po2ne  5555  soasym  5572  elreldm  5890  dfres3  5949  relcnvtrg  6231  relresfld  6240  elpredimg  6280  ordtr2  6368  ordssun  6427  funopg  6532  funimass2  6581  f1imadifssran  6584  f0dom0  6724  elfv2ex  6883  fveqdmss  7030  eldmrexrnb  7044  fvcofneq  7045  funopsn  7101  funopsnOLD  7102  funopdmsn  7104  funsndifnop  7105  elunirn  7206  oprabidw  7398  oprabid  7399  brfvopab  7424  limuni3  7803  peano5  7844  resf1ext2b  7886  op1steq  7986  el2mpocsbcl  8035  bropopvvv  8040  bropfvvvv  8042  f1o2ndf1  8072  frxp  8076  fnwelem  8081  poxp2  8093  suppimacnv  8124  fvn0elsuppb  8131  suppfnss  8139  reldmtpos  8184  rntpos  8189  seqomlem2  8390  oaordi  8481  oa00  8494  oalimcl  8495  omeulem1  8517  nnaordi  8554  ecopovtrn  8767  undifixp  8882  mapdom2  9086  unxpdomlem3  9168  en1eqsn  9185  infssuni  9256  wdompwdom  9493  preleqg  9536  opthreg  9539  inf3lemd  9548  inf3lem2  9550  inf3lem6  9554  cnfcomlem  9620  cnfcom3  9625  karden  9819  carden2a  9890  alephdom  10003  dfac5lem4  10048  dfac5lem4OLD  10050  dfac12r  10069  kmlem2  10074  kmlem12  10084  cfslb2n  10190  alephsing  10198  fin23lem30  10264  fin1a2lem6  10327  fin1a2lem13  10334  axcc2lem  10358  domtriomlem  10364  axdc3lem2  10373  axdc4lem  10377  brdom6disj  10454  alephexp1  10502  pwfseq  10587  addnidpi  10824  indpi  10830  nqereu  10852  ltsonq  10892  distrlem5pr  10950  addcanpr  10969  suplem1pr  10975  suplem2pr  10976  ltsrpr  11000  ltsosr  11017  sqgt0sr  11029  leltne  11235  ltnsym  11244  ltlen  11247  eqlei  11256  eqlei2  11257  infm3  12115  nnunb  12433  0mnnnnn0  12469  elnnnn0b  12481  nn0ge2m1nn  12507  nn0le2is012  12593  btwnz  12632  uz11  12813  xrleltne  13096  xltnegi  13168  xnn0lenn0nn0  13197  xnn0xadd0  13199  xmulasslem2  13234  reltxrnmnf  13295  icogelb  13349  iccleub  13354  uznfz  13564  2ffzeq  13603  elfzonlteqm1  13696  elfzo0l  13711  fzoopth  13717  elfznelfzob  13729  elfzr  13736  elfzlmr  13737  injresinjlem  13745  injresinj  13746  fleqceilz  13813  modadd1  13867  modmul1  13886  modirr  13904  addmodlteq  13908  uzrdgfni  13920  fsuppmapnn0fiub0  13955  fsuppmapnn0ub  13957  seqf1o  14005  expnngt1  14203  hashrabsn01  14335  hashrabsn1  14336  hash1snb  14381  hash1n0  14383  hashf1lem2  14418  hash2prde  14432  hash2prd  14437  hash2pwpr  14438  hashle2pr  14439  hashle2prv  14440  hashge2el2dif  14442  hashge2el2difr  14443  hash3tpde  14455  fundmge2nop0  14464  ffz0iswrd  14503  ccatrcl1  14557  pfxsuff1eqwrdeq  14661  wrdind  14684  wrd2ind  14685  swrdccatin1  14687  swrdccat3blem  14701  2cshwcshw  14787  cshwcsh2id  14790  cshimadifsn  14791  2swrd2eqwrdeq  14915  wwlktovf  14918  wwlktovfo  14920  s3sndisj  14929  s3iunsndisj  14930  relexpindlem  15025  rexico  15316  lo1le  15614  fsum2dlem  15732  ntrivcvg  15862  fprodss  15913  fprod2dlem  15945  0dvds  16245  mod2eq1n2dvds  16316  opoe  16332  omoe  16333  opeo  16334  omeo  16335  m1exp1  16345  nn0enne  16346  nn0o1gt2  16350  gcdneg  16491  dfgcd2  16515  algcvga  16548  eucalglt  16554  lcmf  16602  coprmdvds  16622  divgcdcoprmex  16635  cncongr1  16636  prm2orodd  16660  prm23lt5  16785  pockthi  16878  prmreclem5  16891  ramtcl2  16982  cshwrepswhash1  17073  f1ocpbl  17489  f1ovscpbl  17490  f1olecpbl  17491  monhom  17702  epihom  17709  inveq  17741  invcoisoid  17759  isocoinvid  17760  ciclcl  17769  cicrcl  17770  isinitoi  17966  istermoi  17967  2initoinv  17977  2termoinv  17984  setciso  18058  embedsetcestrclem  18123  ipopos  18502  mgmpropd  18619  gsumval2a  18653  ismnddef  18704  dfgrp2e  18939  symg2bas  19368  snsymgefmndeq  19370  symgvalstruct  19372  symgfix2  19391  gsmsymgreq  19407  pmtrdifellem4  19454  mndodcongi  19518  pj1eu  19671  cycsubmcmn  19864  dprd2da  20019  rngimf1o  20434  rngimrnghm  20435  c0snmgmhm  20442  0ring01eq  20506  elrngchom  20601  rnghmsubcsetclem1  20608  rnghmsubcsetclem2  20609  rngcid  20612  rngcinv  20614  rngciso  20615  funcrngcsetcALT  20618  zrinitorngc  20619  zrtermorngc  20620  elringchom  20630  rhmsubcsetclem1  20637  rhmsubcsetclem2  20638  ringcid  20641  rhmsubcrngclem1  20643  rhmsubcrngclem2  20644  ringciso  20649  zrtermoringc  20652  rhmsubclem3  20664  rhmsubclem4  20665  lmodfopnelem1  20893  lspdisjb  21124  lspsnsubn0  21138  rngqiprngfulem2  21310  irinitoringc  21459  obs2ss  21709  mamufacex  22361  mat0dim0  22432  mat0dimid  22433  mat0dimscm  22434  dmatmat  22459  scmatmat  22474  mat1scmat  22504  1mavmul  22513  mavmulsolcl  22516  gsummatr01  22624  cpmatpmat  22675  cpmadugsumlemF  22841  tg2  22930  tgcl  22934  neii1  23071  neii2  23073  neindisj2  23088  perfopn  23150  ordtbas2  23156  pnfnei  23185  mnfnei  23186  llyidm  23453  txlm  23613  qtopuni  23667  tgqtop  23677  isfild  23823  snfil  23829  fbunfip  23834  fgss2  23839  fmco  23926  fbflim2  23942  cnpflf2  23965  fcfelbas  24001  fcfneii  24002  alexsubALTlem2  24013  alexsubALT  24016  tgpconncompeqg  24077  tsmscl  24100  tngngpim  24624  tgioo  24761  xrsmopn  24778  iccntr  24787  reconnlem2  24793  addcnlem  24830  htpycn  24940  phtpyhtpy  24949  pi1blem  25006  fgcfil  25238  ioombl1lem4  25528  dyadmbl  25567  itg2gt0  25727  ditgneg  25824  dvivthlem1  25975  coeeq2  26207  aannenlem2  26295  sineq0  26488  efif1o  26510  xrlimcnp  26932  vmacl  27081  efvmacl  27083  vmalelog  27168  dchrelbasd  27202  lgsqr  27314  lgsqrmodndvds  27316  gausslemma2dlem0i  27327  2lgslem2  27358  2lgs  27370  2lgsoddprmlem3  27377  2sqnn  27402  2sqreultlem  27410  2sqreultblem  27411  2sqreunnltlem  27413  2sqreunnltblem  27414  ltsintdifex  27625  ltsres  27626  nosepnelem  27643  nolt02o  27659  ltlesnd  27739  negsprop  28027  mulsprop  28122  onnolt  28258  onlts  28259  n0subs  28355  bdaypw2n0bndlem  28455  bdaypw2n0bnd  28456  bdayfinbndlem2  28460  elntg2  29054  uhgr0vb  29141  umgrupgr  29172  umgrnloopv  29175  umgredgprv  29176  umgrislfupgrlem  29191  umgredg  29207  uspgrushgr  29246  uspgrupgr  29247  usgruspgr  29249  usgredgprvALT  29264  usgrnloopvALT  29270  uhgr2edg  29277  edg0usgr  29322  egrsubgr  29346  0uhgrsubgr  29348  uhgrspansubgrlem  29359  nbuhgr  29412  cusgrsize2inds  29522  cusgrfilem2  29525  vtxdg0v  29542  1loopgrnb0  29571  vtxdginducedm1lem4  29611  wlkvtxeledg  29692  wlkeq  29702  wlkl1loop  29706  wlk1walk  29707  upgrwlkedg  29710  uspgr2wlkeq  29714  wlkv0  29718  wlkonl1iedg  29732  wlkon2n0  29733  wlkp1lem8  29747  wlkp1  29748  lfgrwlkprop  29754  lfgrwlknloop  29756  2pthnloop  29799  upgrwlkdvde  29805  spthonepeq  29820  uhgrwkspthlem2  29822  usgr2wlkneq  29824  usgr2trlncl  29828  usgr2trlspth  29829  pthdlem2lem  29835  clwlkcompbp  29850  uspgrn2crct  29876  wwlks  29903  wwlknbp  29910  0enwwlksnge1  29932  wwlkswwlksn  29933  wlklnwwlkln1  29936  wwlksnextproplem3  29979  wwlksnextprop  29980  wspthsnonn0vne  29985  wspn0  29992  2pthon3v  30011  umgr2adedgspth  30016  rusgr0edg  30044  clwwlkccat  30060  clwlkclwwlklem2fv2  30066  clwlkclwwlklem2a4  30067  clwlkclwwlklem2  30070  clwlkclwwlkflem  30074  clwwlknp  30107  clwwlkwwlksb  30124  clwwlkext2edg  30126  erclwwlkneqlen  30138  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  clwwlknonwwlknonb  30176  upgr1wlkdlem1  30215  upgr3v3e3cycl  30250  uhgr3cyclexlem  30251  1conngr  30264  conngrv2edg  30265  eupth2lem3lem4  30301  eulercrct  30312  isfrgr  30330  frgr3vlem2  30344  1to2vfriswmgr  30349  1to3vfriswmgr  30350  frgrncvvdeqlem9  30377  frgrwopreg  30393  frgr2wwlkeqm  30401  2wspmdisj  30407  numclwwlk1lem2f  30425  frgrreggt1  30463  frgrregord013  30465  frgrregord13  30466  l2p  30550  nmlno0lem  30864  normgt0  31198  ocin  31367  nmlnop0iALT  32066  nmopun  32085  cvpss  32356  cvnbtwn  32357  atcvati  32457  mdsymlem6  32479  iunrnmptss  32635  expgt0b  32890  wrdt2ind  33013  irngssv  33832  issgon  34267  mbfmcnt  34412  ballotlemfc0  34637  ballotlemfcc  34638  satfv0  35540  satfv0fun  35553  fmla1  35569  gonarlem  35576  gonar  35577  goalrlem  35578  goalr  35579  fmla0disjsuc  35580  satffunlem  35583  satffunlem1lem1  35584  satffunlem2lem1  35586  satfun  35593  satfv0fvfmla0  35595  sategoelfv  35602  mthmblem  35762  pprodss4v  36064  funpartfun  36125  funpartfv  36127  5segofs  36188  btwnxfr  36238  brofs2  36259  brifs2  36260  btwnconn1  36283  segleantisym  36297  broutsideof2  36304  outsidene1  36305  outsidene2  36306  funray  36322  lineunray  36329  cldbnd  36508  bj-imdirval3  37498  topdifinffinlem  37663  isbasisrelowllem1  37671  isbasisrelowllem2  37672  relowlpssretop  37680  inunissunidif  37691  pibt2  37733  matunitlindf  37939  poimir  37974  volsupnfl  37986  itg2addnclem  37992  cover2  38036  sdclem2  38063  fdc  38066  sstotbnd3  38097  heibor1  38131  clmgmOLD  38172  smgrpmgm  38185  smgrpassOLD  38186  dvrunz  38275  0rngo  38348  mopickr  38692  sucmapleftuniq  38811  lsatcvat  39496  lshpkrex  39564  cmtbr3N  39700  atn0  39754  atnle  39763  cvlsupr4  39791  cvlsupr5  39792  cvlsupr6  39793  cvrval4N  39860  cvratlem  39867  2llnjN  40013  2lplnj  40066  linepsubN  40198  elpaddatiN  40251  elpcliN  40339  pclcmpatN  40347  ldilval  40559  ltrnu  40567  cdleme18d  40741  tendotp  41207  tendof  41209  tendovalco  41211  diatrl  41490  diaintclN  41504  dvheveccl  41558  dibintclN  41613  dihord6apre  41702  dihmeetlem1N  41736  dihpN  41782  dihintcl  41790  dochkrshp4  41835  oexpreposd  42754  pw2f1ocnv  43465  iocinico  43640  onsucf1olem  43698  succlg  43756  oacl2g  43758  omabs2  43760  omcl2  43761  naddcnfcom  43794  naddcnfass  43797  safesnsupfidom1o  43844  infordmin  43959  pr2cv  43975  expgrowthi  44760  iotavalsb  44860  bi23imp1  44922  ioogtlb  45925  iocgtlb  45932  iocleub  45933  icoltub  45938  iooltub  45940  stoweidlem31  46459  oppr  47478  funressnfv  47491  fsetsniunop  47497  fsetsnf1  47500  eu2ndop1stv  47573  afvelrnb0  47612  otiunsndisjX  47727  el1fzopredsuc  47774  2ffzoeq  47776  uniimaprimaeqfv  47842  elsetpreimafveqfv  47852  iccpartimp  47877  iccpartrn  47890  iccpartf  47891  iccpartnel  47898  fargshiftf  47900  fargshiftfo  47902  ichnfimlem  47923  ichnfim  47924  ichreuopeq  47933  sprel  47944  sprsymrelfvlem  47950  sprsymrelfolem2  47953  prproropf1olem4  47966  prprelb  47976  poprelb  47984  fmtnofac1  48033  prmdvdsfmtnof1lem2  48048  31prm  48060  lighneallem3  48070  ppivalnnnprm  48091  nn0o1gt2ALTV  48170  nn0oALTV  48172  odd2prm2  48194  mogoldbblem  48196  fpprbasnn  48205  fpprnn  48206  sbgoldbaltlem1  48255  nnsum3primesle9  48270  bgoldbtbndlem1  48281  bgoldbtbndlem2  48282  grimedgi  48412  grtriproplem  48415  grtriprop  48417  cycl3grtrilem  48422  cycl3grtri  48423  isubgr3stgrlem8  48449  gpgvtxel2  48524  gpgedgiov  48541  gpgedg2iv  48543  gpgprismgr4cycllem7  48577  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5  48599  upwlkbprop  48614  clcllaw  48667  intop  48679  assintop  48685  assintopcllaw  48688  elrngchomALTV  48745  rngccatidALTV  48748  rngcinvALTV  48752  rngcisoALTV  48753  rhmsubcALTVlem3  48759  rhmsubcALTVlem4  48760  funcringcsetcALTV2lem7  48772  elringchomALTV  48779  ringccatidALTV  48782  ringcisoALTV  48787  funcringcsetclem7ALTV  48795  ztprmneprm  48823  suppmptcfin  48852  linccl  48890  linc1  48901  lincolss  48910  ldepspr  48949  nn0sumshdiglem1  49097  0aryfvalelfv  49111  rrxlines  49209  rrxsphere  49224  itsclc0yqsol  49240  itschlc0xyqsol1  49242  fdomne0  49325  f002  49329  fvconstr2  49339  fullthinc  49925