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  1967  sb4a  2484  hbsb2  2486  dfsb2  2497  2eu2  2653  reu6  3684  2reu2  3848  sseq0  4355  disjel  4409  disjpss  4413  preq12b  4806  prneimg  4810  preqsnd  4815  elinti  4911  zfrepclf  5236  dtruALT2  5315  opth1g  5426  sbcop1  5436  snopeqop  5454  propeqop  5455  otsndisj  5467  otiunsndisj  5468  iunopeqop  5469  po2ne  5548  soasym  5565  elreldm  5884  dfres3  5943  relcnvtrg  6225  relresfld  6234  elpredimg  6274  ordtr2  6362  ordssun  6421  funopg  6526  funimass2  6575  f1imadifssran  6578  f0dom0  6718  elfv2ex  6877  fveqdmss  7023  eldmrexrnb  7037  fvcofneq  7038  funopsn  7093  funopdmsn  7095  funsndifnop  7096  elunirn  7197  oprabidw  7389  oprabid  7390  brfvopab  7415  limuni3  7794  peano5  7835  resf1ext2b  7877  op1steq  7977  el2mpocsbcl  8027  bropopvvv  8032  bropfvvvv  8034  f1o2ndf1  8064  frxp  8068  fnwelem  8073  poxp2  8085  suppimacnv  8116  fvn0elsuppb  8123  suppfnss  8131  reldmtpos  8176  rntpos  8181  seqomlem2  8382  oaordi  8473  oa00  8486  oalimcl  8487  omeulem1  8509  nnaordi  8546  ecopovtrn  8759  undifixp  8874  mapdom2  9078  unxpdomlem3  9160  en1eqsn  9177  infssuni  9248  wdompwdom  9485  preleqg  9526  opthreg  9529  inf3lemd  9538  inf3lem2  9540  inf3lem6  9544  cnfcomlem  9610  cnfcom3  9615  karden  9809  carden2a  9880  alephdom  9993  dfac5lem4  10038  dfac5lem4OLD  10040  dfac12r  10059  kmlem2  10064  kmlem12  10074  cfslb2n  10180  alephsing  10188  fin23lem30  10254  fin1a2lem6  10317  fin1a2lem13  10324  axcc2lem  10348  domtriomlem  10354  axdc3lem2  10363  axdc4lem  10367  brdom6disj  10444  alephexp1  10492  pwfseq  10577  addnidpi  10814  indpi  10820  nqereu  10842  ltsonq  10882  distrlem5pr  10940  addcanpr  10959  suplem1pr  10965  suplem2pr  10966  ltsrpr  10990  ltsosr  11007  sqgt0sr  11019  leltne  11224  ltnsym  11233  ltlen  11236  eqlei  11245  eqlei2  11246  infm3  12103  nnunb  12399  0mnnnnn0  12435  elnnnn0b  12447  nn0ge2m1nn  12473  nn0le2is012  12558  btwnz  12597  uz11  12778  xrleltne  13061  xltnegi  13133  xnn0lenn0nn0  13162  xnn0xadd0  13164  xmulasslem2  13199  reltxrnmnf  13260  icogelb  13314  iccleub  13319  uznfz  13528  2ffzeq  13567  elfzonlteqm1  13659  elfzo0l  13674  fzoopth  13680  elfznelfzob  13692  elfzr  13699  elfzlmr  13700  injresinjlem  13708  injresinj  13709  fleqceilz  13776  modadd1  13830  modmul1  13849  modirr  13867  addmodlteq  13871  uzrdgfni  13883  fsuppmapnn0fiub0  13918  fsuppmapnn0ub  13920  seqf1o  13968  expnngt1  14166  hashrabsn01  14298  hashrabsn1  14299  hash1snb  14344  hash1n0  14346  hashf1lem2  14381  hash2prde  14395  hash2prd  14400  hash2pwpr  14401  hashle2pr  14402  hashle2prv  14403  hashge2el2dif  14405  hashge2el2difr  14406  hash3tpde  14418  fundmge2nop0  14427  ffz0iswrd  14466  ccatrcl1  14520  pfxsuff1eqwrdeq  14624  wrdind  14647  wrd2ind  14648  swrdccatin1  14650  swrdccat3blem  14664  2cshwcshw  14750  cshwcsh2id  14753  cshimadifsn  14754  2swrd2eqwrdeq  14878  wwlktovf  14881  wwlktovfo  14883  s3sndisj  14892  s3iunsndisj  14893  relexpindlem  14988  rexico  15279  lo1le  15577  fsum2dlem  15695  ntrivcvg  15822  fprodss  15873  fprod2dlem  15905  0dvds  16205  mod2eq1n2dvds  16276  opoe  16292  omoe  16293  opeo  16294  omeo  16295  m1exp1  16305  nn0enne  16306  nn0o1gt2  16310  gcdneg  16451  dfgcd2  16475  algcvga  16508  eucalglt  16514  lcmf  16562  coprmdvds  16582  divgcdcoprmex  16595  cncongr1  16596  prm2orodd  16620  prm23lt5  16744  pockthi  16837  prmreclem5  16850  ramtcl2  16941  cshwrepswhash1  17032  f1ocpbl  17448  f1ovscpbl  17449  f1olecpbl  17450  monhom  17661  epihom  17668  inveq  17700  invcoisoid  17718  isocoinvid  17719  ciclcl  17728  cicrcl  17729  isinitoi  17925  istermoi  17926  2initoinv  17936  2termoinv  17943  setciso  18017  embedsetcestrclem  18082  ipopos  18461  mgmpropd  18578  gsumval2a  18612  ismnddef  18663  dfgrp2e  18895  symg2bas  19324  snsymgefmndeq  19326  symgvalstruct  19328  symgfix2  19347  gsmsymgreq  19363  pmtrdifellem4  19410  mndodcongi  19474  pj1eu  19627  cycsubmcmn  19820  dprd2da  19975  rngimf1o  20392  rngimrnghm  20393  c0snmgmhm  20400  0ring01eq  20464  elrngchom  20559  rnghmsubcsetclem1  20566  rnghmsubcsetclem2  20567  rngcid  20570  rngcinv  20572  rngciso  20573  funcrngcsetcALT  20576  zrinitorngc  20577  zrtermorngc  20578  elringchom  20588  rhmsubcsetclem1  20595  rhmsubcsetclem2  20596  ringcid  20599  rhmsubcrngclem1  20601  rhmsubcrngclem2  20602  ringciso  20607  zrtermoringc  20610  rhmsubclem3  20622  rhmsubclem4  20623  lmodfopnelem1  20851  lspdisjb  21083  lspsnsubn0  21097  rngqiprngfulem2  21269  irinitoringc  21436  obs2ss  21686  mamufacex  22342  mat0dim0  22413  mat0dimid  22414  mat0dimscm  22415  dmatmat  22440  scmatmat  22455  mat1scmat  22485  1mavmul  22494  mavmulsolcl  22497  gsummatr01  22605  cpmatpmat  22656  cpmadugsumlemF  22822  tg2  22911  tgcl  22915  neii1  23052  neii2  23054  neindisj2  23069  perfopn  23131  ordtbas2  23137  pnfnei  23166  mnfnei  23167  llyidm  23434  txlm  23594  qtopuni  23648  tgqtop  23658  isfild  23804  snfil  23810  fbunfip  23815  fgss2  23820  fmco  23907  fbflim2  23923  cnpflf2  23946  fcfelbas  23982  fcfneii  23983  alexsubALTlem2  23994  alexsubALT  23997  tgpconncompeqg  24058  tsmscl  24081  tngngpim  24605  tgioo  24742  xrsmopn  24759  iccntr  24768  reconnlem2  24774  addcnlem  24811  htpycn  24930  phtpyhtpy  24939  pi1blem  24997  fgcfil  25229  ioombl1lem4  25520  dyadmbl  25559  itg2gt0  25719  ditgneg  25816  dvivthlem1  25971  coeeq2  26205  aannenlem2  26295  sineq0  26491  efif1o  26513  xrlimcnp  26936  vmacl  27086  efvmacl  27088  vmalelog  27174  dchrelbasd  27208  lgsqr  27320  lgsqrmodndvds  27322  gausslemma2dlem0i  27333  2lgslem2  27364  2lgs  27376  2lgsoddprmlem3  27383  2sqnn  27408  2sqreultlem  27416  2sqreultblem  27417  2sqreunnltlem  27419  2sqreunnltblem  27420  ltsintdifex  27631  ltsres  27632  nosepnelem  27649  nolt02o  27665  ltlesnd  27745  negsprop  28033  mulsprop  28128  onnolt  28264  onlts  28265  n0subs  28361  bdaypw2n0bndlem  28461  bdaypw2n0bnd  28462  bdayfinbndlem2  28466  elntg2  29060  uhgr0vb  29147  umgrupgr  29178  umgrnloopv  29181  umgredgprv  29182  umgrislfupgrlem  29197  umgredg  29213  uspgrushgr  29252  uspgrupgr  29253  usgruspgr  29255  usgredgprvALT  29270  usgrnloopvALT  29276  uhgr2edg  29283  edg0usgr  29328  egrsubgr  29352  0uhgrsubgr  29354  uhgrspansubgrlem  29365  nbuhgr  29418  cusgrsize2inds  29529  cusgrfilem2  29532  vtxdg0v  29549  1loopgrnb0  29578  vtxdginducedm1lem4  29618  wlkvtxeledg  29699  wlkeq  29709  wlkl1loop  29713  wlk1walk  29714  upgrwlkedg  29717  uspgr2wlkeq  29721  wlkv0  29725  wlkonl1iedg  29739  wlkon2n0  29740  wlkp1lem8  29754  wlkp1  29755  lfgrwlkprop  29761  lfgrwlknloop  29763  2pthnloop  29806  upgrwlkdvde  29812  spthonepeq  29827  uhgrwkspthlem2  29829  usgr2wlkneq  29831  usgr2trlncl  29835  usgr2trlspth  29836  pthdlem2lem  29842  clwlkcompbp  29857  uspgrn2crct  29883  wwlks  29910  wwlknbp  29917  0enwwlksnge1  29939  wwlkswwlksn  29940  wlklnwwlkln1  29943  wwlksnextproplem3  29986  wwlksnextprop  29987  wspthsnonn0vne  29992  wspn0  29999  2pthon3v  30018  umgr2adedgspth  30023  rusgr0edg  30051  clwwlkccat  30067  clwlkclwwlklem2fv2  30073  clwlkclwwlklem2a4  30074  clwlkclwwlklem2  30077  clwlkclwwlkflem  30081  clwwlknp  30114  clwwlkwwlksb  30131  clwwlkext2edg  30133  erclwwlkneqlen  30145  hashecclwwlkn1  30154  umgrhashecclwwlk  30155  clwwlknonwwlknonb  30183  upgr1wlkdlem1  30222  upgr3v3e3cycl  30257  uhgr3cyclexlem  30258  1conngr  30271  conngrv2edg  30272  eupth2lem3lem4  30308  eulercrct  30319  isfrgr  30337  frgr3vlem2  30351  1to2vfriswmgr  30356  1to3vfriswmgr  30357  frgrncvvdeqlem9  30384  frgrwopreg  30400  frgr2wwlkeqm  30408  2wspmdisj  30414  numclwwlk1lem2f  30432  frgrreggt1  30470  frgrregord013  30472  frgrregord13  30473  l2p  30556  nmlno0lem  30870  normgt0  31204  ocin  31373  nmlnop0iALT  32072  nmopun  32091  cvpss  32362  cvnbtwn  32363  atcvati  32463  mdsymlem6  32485  iunrnmptss  32642  expgt0b  32899  wrdt2ind  33037  irngssv  33847  issgon  34282  mbfmcnt  34427  ballotlemfc0  34652  ballotlemfcc  34653  satfv0  35554  satfv0fun  35567  fmla1  35583  gonarlem  35590  gonar  35591  goalrlem  35592  goalr  35593  fmla0disjsuc  35594  satffunlem  35597  satffunlem1lem1  35598  satffunlem2lem1  35600  satfun  35607  satfv0fvfmla0  35609  sategoelfv  35616  mthmblem  35776  pprodss4v  36078  funpartfun  36139  funpartfv  36141  5segofs  36202  btwnxfr  36252  brofs2  36273  brifs2  36274  btwnconn1  36297  segleantisym  36311  broutsideof2  36318  outsidene1  36319  outsidene2  36320  funray  36336  lineunray  36343  cldbnd  36522  bj-imdirval3  37391  topdifinffinlem  37554  isbasisrelowllem1  37562  isbasisrelowllem2  37563  relowlpssretop  37571  inunissunidif  37582  pibt2  37624  matunitlindf  37821  poimir  37856  volsupnfl  37868  itg2addnclem  37874  cover2  37918  sdclem2  37945  fdc  37948  sstotbnd3  37979  heibor1  38013  clmgmOLD  38054  smgrpmgm  38067  smgrpassOLD  38068  dvrunz  38157  0rngo  38230  mopickr  38569  sucmapleftuniq  38685  lsatcvat  39332  lshpkrex  39400  cmtbr3N  39536  atn0  39590  atnle  39599  cvlsupr4  39627  cvlsupr5  39628  cvlsupr6  39629  cvrval4N  39696  cvratlem  39703  2llnjN  39849  2lplnj  39902  linepsubN  40034  elpaddatiN  40087  elpcliN  40175  pclcmpatN  40183  ldilval  40395  ltrnu  40403  cdleme18d  40577  tendotp  41043  tendof  41045  tendovalco  41047  diatrl  41326  diaintclN  41340  dvheveccl  41394  dibintclN  41449  dihord6apre  41538  dihmeetlem1N  41572  dihpN  41618  dihintcl  41626  dochkrshp4  41671  oexpreposd  42598  pw2f1ocnv  43300  iocinico  43475  onsucf1olem  43533  succlg  43591  oacl2g  43593  omabs2  43595  omcl2  43596  naddcnfcom  43629  naddcnfass  43632  safesnsupfidom1o  43679  infordmin  43794  pr2cv  43810  expgrowthi  44595  iotavalsb  44695  bi23imp1  44757  ioogtlb  45762  iocgtlb  45769  iocleub  45770  icoltub  45775  iooltub  45777  stoweidlem31  46296  oppr  47297  funressnfv  47310  fsetsniunop  47316  fsetsnf1  47319  eu2ndop1stv  47392  afvelrnb0  47431  otiunsndisjX  47546  el1fzopredsuc  47592  2ffzoeq  47594  uniimaprimaeqfv  47649  elsetpreimafveqfv  47659  iccpartimp  47684  iccpartrn  47697  iccpartf  47698  iccpartnel  47705  fargshiftf  47707  fargshiftfo  47709  ichnfimlem  47730  ichnfim  47731  ichreuopeq  47740  sprel  47751  sprsymrelfvlem  47757  sprsymrelfolem2  47760  prproropf1olem4  47773  prprelb  47783  poprelb  47791  fmtnofac1  47837  prmdvdsfmtnof1lem2  47852  31prm  47864  lighneallem3  47874  nn0o1gt2ALTV  47961  nn0oALTV  47963  odd2prm2  47985  mogoldbblem  47987  fpprbasnn  47996  fpprnn  47997  sbgoldbaltlem1  48046  nnsum3primesle9  48061  bgoldbtbndlem1  48072  bgoldbtbndlem2  48073  grimedgi  48203  grtriproplem  48206  grtriprop  48208  cycl3grtrilem  48213  cycl3grtri  48214  isubgr3stgrlem8  48240  gpgvtxel2  48315  gpgedgiov  48332  gpgedg2iv  48334  gpgprismgr4cycllem7  48368  pgnbgreunbgrlem1  48380  pgnbgreunbgrlem2lem1  48381  pgnbgreunbgrlem2lem2  48382  pgnbgreunbgrlem2lem3  48383  pgnbgreunbgrlem2  48384  pgnbgreunbgrlem4  48386  pgnbgreunbgrlem5  48390  upwlkbprop  48405  clcllaw  48458  intop  48470  assintop  48476  assintopcllaw  48479  elrngchomALTV  48536  rngccatidALTV  48539  rngcinvALTV  48543  rngcisoALTV  48544  rhmsubcALTVlem3  48550  rhmsubcALTVlem4  48551  funcringcsetcALTV2lem7  48563  elringchomALTV  48570  ringccatidALTV  48573  ringcisoALTV  48578  funcringcsetclem7ALTV  48586  ztprmneprm  48614  suppmptcfin  48643  linccl  48681  linc1  48692  lincolss  48701  ldepspr  48740  nn0sumshdiglem1  48888  0aryfvalelfv  48902  rrxlines  49000  rrxsphere  49015  itsclc0yqsol  49031  itschlc0xyqsol1  49033  fdomne0  49116  f002  49120  fvconstr2  49130  fullthinc  49716