Theorem biimtrdi 255

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 231	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  ax12i  1987  sb4a  2512  hbsb2  2514  dfsb2  2525  2eu2  2680  reu6  3690  2reu2  3852  sseq0  4358  disjel  4412  disjpss  4416  preq12b  4809  prneimg  4813  preqsnd  4818  elinti  4915  zfrepclf  5242  exnelv  5264  dtruALT2  5328  opth1g  5447  sbcop1  5457  snopeqop  5476  propeqop  5477  otsndisj  5489  otiunsndisj  5490  iunopeqop  5491  iunopeqopOLD  5492  po2ne  5572  soasym  5589  elreldm  5912  dfres3  5971  relcnvtrg  6255  relresfld  6264  elpredimg  6304  ordtr2  6392  ordssun  6451  funopg  6556  funimass2  6605  f1imadifssran  6608  f0dom0  6749  elfv2ex  6911  fveqdmss  7060  eldmrexrnb  7074  fvcofneq  7075  funopsn  7131  funopsnOLD  7132  funopdmsn  7134  funsndifnop  7135  elunirn  7236  oprabidw  7428  oprabid  7429  brfvopab  7454  limuni3  7833  peano5  7875  resf1ext2b  7917  op1steq  8015  el2mpocsbcl  8065  bropopvvv  8070  bropfvvvv  8072  f1o2ndf1  8102  frxp  8107  fnwelem  8112  poxp2  8124  suppimacnv  8155  fvn0elsuppb  8162  suppfnss  8170  reldmtpos  8215  rntpos  8220  seqomlem2  8423  oaordi  8516  oa00  8529  oalimcl  8530  omeulem1  8552  nnaordi  8589  ecopovtrn  8803  undifixp  8917  mapdom2  9121  unxpdomlem3  9203  en1eqsn  9220  infssuni  9290  wdompwdom  9527  preleqg  9571  opthreg  9574  inf3lemd  9583  inf3lem2  9585  inf3lem6  9589  cnfcomlem  9655  cnfcom3  9660  karden  9854  carden2a  9925  alephdom  10038  dfac5lem4  10083  dfac5lem4OLD  10085  dfac12r  10104  kmlem2  10109  kmlem12  10119  cfslb2n  10226  alephsing  10234  fin23lem30  10300  fin1a2lem6  10363  fin1a2lem13  10370  axcc2lem  10394  domtriomlem  10400  axdc3lem2  10409  axdc4lem  10413  brdom6disj  10490  alephexp1  10538  pwfseq  10623  addnidpi  10860  indpi  10866  nqereu  10888  ltsonq  10928  distrlem5pr  10986  addcanpr  11005  suplem1pr  11011  suplem2pr  11012  ltsrpr  11036  ltsosr  11053  sqgt0sr  11065  leltne  11273  ltnsym  11282  ltlen  11285  eqlei  11294  eqlei2  11295  infm3  12152  nnunb  12478  0mnnnnn0  12514  elnnnn0b  12526  nn0ge2m1nn  12552  nn0le2is012  12638  btwnz  12677  uz11  12865  xrleltne  13148  xltnegi  13220  xnn0lenn0nn0  13249  xnn0xadd0  13251  xmulasslem2  13286  reltxrnmnf  13347  icogelb  13401  iccleub  13406  uznfz  13616  2ffzeq  13655  elfzonlteqm1  13748  elfzo0l  13763  fzoopth  13769  elfznelfzob  13781  elfzr  13788  elfzlmr  13789  injresinjlem  13797  injresinj  13798  fleqceilz  13865  modadd1  13919  modmul1  13938  modirr  13956  addmodlteq  13960  uzrdgfni  13972  fsuppmapnn0fiub0  14007  fsuppmapnn0ub  14009  seqf1o  14057  expnngt1  14255  hashrabsn01  14387  hashrabsn1  14388  hash1snb  14433  hash1n0  14435  hashf1lem2  14470  hash2prde  14484  hash2prd  14489  hash2pwpr  14490  hashle2pr  14491  hashle2prv  14492  hashge2el2dif  14494  hashge2el2difr  14495  hash3tpde  14507  fundmge2nop0  14516  ffz0iswrd  14555  ccatrcl1  14609  pfxsuff1eqwrdeq  14713  wrdind  14736  wrd2ind  14737  swrdccatin1  14739  swrdccat3blem  14753  2cshwcshw  14839  cshwcsh2id  14842  cshimadifsn  14843  2swrd2eqwrdeq  14967  wwlktovf  14970  wwlktovfo  14972  s3sndisj  14981  s3iunsndisj  14982  relexpindlem  15077  rexico  15382  lo1le  15680  fsum2dlem  15798  ntrivcvg  15928  fprodss  15979  fprod2dlem  16011  0dvds  16311  mod2eq1n2dvds  16382  opoe  16398  omoe  16399  opeo  16400  omeo  16401  m1exp1  16411  nn0enne  16412  nn0o1gt2  16416  gcdneg  16557  dfgcd2  16581  algcvga  16614  eucalglt  16620  lcmf  16668  coprmdvds  16688  divgcdcoprmex  16701  cncongr1  16702  prm2orodd  16726  prm23lt5  16851  pockthi  16944  prmreclem5  16957  ramtcl2  17048  cshwrepswhash1  17139  f1ocpbl  17556  f1ovscpbl  17557  f1olecpbl  17558  monhom  17769  epihom  17776  inveq  17808  invcoisoid  17826  isocoinvid  17827  ciclcl  17836  cicrcl  17837  isinitoi  18033  istermoi  18034  2initoinv  18044  2termoinv  18051  setciso  18125  embedsetcestrclem  18190  ipopos  18569  mgmpropd  18686  gsumval2a  18720  ismnddef  18771  dfgrp2e  19006  symg2bas  19434  snsymgefmndeq  19436  symgvalstruct  19438  symgfix2  19457  gsmsymgreq  19473  pmtrdifellem4  19520  mndodcongi  19584  pj1eu  19737  cycsubmcmn  19930  dprd2da  20085  rngimf1o  20504  rngimrnghm  20505  c0snmgmhm  20512  0ring01eq  20580  elrngchom  20675  rnghmsubcsetclem1  20682  rnghmsubcsetclem2  20683  rngcid  20686  rngcinv  20688  rngciso  20689  funcrngcsetcALT  20692  zrinitorngc  20693  zrtermorngc  20694  elringchom  20704  rhmsubcsetclem1  20711  rhmsubcsetclem2  20712  ringcid  20715  rhmsubcrngclem1  20717  rhmsubcrngclem2  20718  ringciso  20723  zrtermoringc  20726  rhmsubclem3  20738  rhmsubclem4  20739  lmodfopnelem1  20966  lspdisjb  21197  lspsnsubn0  21211  rngqiprngfulem2  21383  irinitoringc  21532  obs2ss  21782  mamufacex  22457  mat0dim0  22528  mat0dimid  22529  mat0dimscm  22530  dmatmat  22555  scmatmat  22570  mat1scmat  22600  1mavmul  22609  mavmulsolcl  22612  gsummatr01  22720  cpmatpmat  22771  cpmadugsumlemF  22937  tg2  23026  tgcl  23030  neii1  23167  neii2  23169  neindisj2  23184  perfopn  23246  ordtbas2  23252  pnfnei  23281  mnfnei  23282  llyidm  23549  txlm  23709  qtopuni  23763  tgqtop  23773  isfild  23919  snfil  23925  fbunfip  23930  fgss2  23935  fmco  24022  fbflim2  24038  cnpflf2  24061  fcfelbas  24097  fcfneii  24098  alexsubALTlem2  24109  alexsubALT  24112  tgpconncompeqg  24173  tsmscl  24196  tngngpim  24720  tgioo  24857  xrsmopn  24874  iccntr  24883  reconnlem2  24889  addcnlem  24926  htpycn  25036  phtpyhtpy  25045  pi1blem  25102  fgcfil  25334  ioombl1lem4  25624  dyadmbl  25663  itg2gt0  25823  ditgneg  25920  dvivthlem1  26071  coeeq2  26303  aannenlem2  26394  sineq0  26590  efif1o  26612  xrlimcnp  27034  vmacl  27183  efvmacl  27185  vmalelog  27270  dchrelbasd  27304  lgsqr  27416  lgsqrmodndvds  27418  gausslemma2dlem0i  27429  2lgslem2  27460  2lgs  27472  2lgsoddprmlem3  27479  2sqnn  27504  2sqreultlem  27512  2sqreultblem  27513  2sqreunnltlem  27515  2sqreunnltblem  27516  ltsintdifex  27726  ltsres  27727  nosepnelem  27744  nolt02o  27760  ltlesnd  27840  negsprop  28129  mulsprop  28224  onnolt  28360  onlts  28361  n0subs  28457  bdaypw2n0bndlem  28557  bdaypw2n0bnd  28558  bdayfinbndlem2  28562  elntg2  29187  uhgr0vb  29274  umgrupgr  29305  umgrnloopv  29308  umgredgprv  29309  umgrislfupgrlem  29324  umgredg  29340  uspgrushgr  29379  uspgrupgr  29380  usgruspgr  29382  usgredgprvALT  29397  usgrnloopvALT  29403  uhgr2edg  29410  edg0usgr  29455  egrsubgr  29479  0uhgrsubgr  29481  uhgrspansubgrlem  29492  nbuhgr  29545  cusgrsize2inds  29655  cusgrfilem2  29658  vtxdg0v  29675  1loopgrnb0  29704  vtxdginducedm1lem4  29744  wlkvtxeledg  29825  wlkeq  29835  wlkl1loop  29839  wlk1walk  29840  upgrwlkedg  29843  uspgr2wlkeq  29847  wlkv0  29851  wlkonl1iedg  29865  wlkon2n0  29866  wlkp1lem8  29880  wlkp1  29881  lfgrwlkprop  29887  lfgrwlknloop  29889  2pthnloop  29932  upgrwlkdvde  29938  spthonepeq  29953  uhgrwkspthlem2  29955  usgr2wlkneq  29957  usgr2trlncl  29961  usgr2trlspth  29962  pthdlem2lem  29968  clwlkcompbp  29983  uspgrn2crct  30009  wwlks  30036  wwlknbp  30043  0enwwlksnge1  30065  wwlkswwlksn  30066  wlklnwwlkln1  30069  wwlksnextproplem3  30112  wwlksnextprop  30113  wspthsnonn0vne  30118  wspn0  30125  2pthon3v  30144  umgr2adedgspth  30149  rusgr0edg  30177  clwwlkccat  30193  clwlkclwwlklem2fv2  30199  clwlkclwwlklem2a4  30200  clwlkclwwlklem2  30203  clwlkclwwlkflem  30207  clwwlknp  30240  clwwlkwwlksb  30257  clwwlkext2edg  30259  erclwwlkneqlen  30271  hashecclwwlkn1  30280  umgrhashecclwwlk  30281  clwwlknonwwlknonb  30309  upgr1wlkdlem1  30348  upgr3v3e3cycl  30383  uhgr3cyclexlem  30384  1conngr  30397  conngrv2edg  30398  eupth2lem3lem4  30434  eulercrct  30445  isfrgr  30463  frgr3vlem2  30477  1to2vfriswmgr  30482  1to3vfriswmgr  30483  frgrncvvdeqlem9  30510  frgrwopreg  30526  frgr2wwlkeqm  30534  2wspmdisj  30540  numclwwlk1lem2f  30558  frgrreggt1  30596  frgrregord013  30598  frgrregord13  30599  l2p  30683  nmlno0lem  30997  normgt0  31331  ocin  31500  nmlnop0iALT  32199  nmopun  32218  cvpss  32489  cvnbtwn  32490  atcvati  32590  mdsymlem6  32612  iunrnmptss  32766  expgt0b  33020  wrdt2ind  33132  irngssv  33986  issgon  34421  mbfmcnt  34566  ballotlemfc0  34791  ballotlemfcc  34792  satfv0  35709  satfv0fun  35722  fmla1  35738  gonarlem  35745  gonar  35746  goalrlem  35747  goalr  35748  fmla0disjsuc  35749  satffunlem  35752  satffunlem1lem1  35753  satffunlem2lem1  35755  satfun  35762  satfv0fvfmla0  35764  sategoelfv  35771  mthmblem  35931  pprodss4v  36233  funpartfun  36294  funpartfv  36296  5segofs  36357  btwnxfr  36407  brofs2  36428  brifs2  36429  btwnconn1  36452  segleantisym  36466  broutsideof2  36473  outsidene1  36474  outsidene2  36475  funray  36491  lineunray  36498  cldbnd  36687  bj-imdirval3  37677  topdifinffinlem  37842  isbasisrelowllem1  37850  isbasisrelowllem2  37851  relowlpssretop  37859  inunissunidif  37870  pibt2  37912  matunitlindf  38118  poimir  38153  volsupnfl  38165  itg2addnclem  38171  cover2  38215  sdclem2  38242  fdc  38245  sstotbnd3  38276  heibor1  38310  clmgmOLD  38351  smgrpmgm  38364  smgrpassOLD  38365  dvrunz  38454  0rngo  38527  mopickr  38871  sucmapleftuniq  38990  lsatcvat  39675  lshpkrex  39743  cmtbr3N  39879  atn0  39933  atnle  39942  cvlsupr4  39970  cvlsupr5  39971  cvlsupr6  39972  cvrval4N  40039  cvratlem  40046  2llnjN  40192  2lplnj  40245  linepsubN  40377  elpaddatiN  40430  elpcliN  40518  pclcmpatN  40526  ldilval  40738  ltrnu  40746  cdleme18d  40920  tendotp  41386  tendof  41388  tendovalco  41390  diatrl  41669  diaintclN  41683  dvheveccl  41737  dibintclN  41792  dihord6apre  41881  dihmeetlem1N  41915  dihpN  41961  dihintcl  41969  dochkrshp4  42014  oexpreposd  42932  pw2f1ocnv  43615  iocinico  43790  onsucf1olem  43848  succlg  43906  oacl2g  43908  omabs2  43910  omcl2  43911  naddcnfcom  43944  naddcnfass  43947  safesnsupfidom1o  43994  infordmin  44109  pr2cv  44125  expgrowthi  44910  iotavalsb  45010  bi23imp1  45072  ioogtlb  46072  iocgtlb  46079  iocleub  46080  icoltub  46085  iooltub  46087  stoweidlem31  46606  oppr  47625  funressnfv  47638  fsetsniunop  47644  fsetsnf1  47647  eu2ndop1stv  47720  afvelrnb0  47759  otiunsndisjX  47874  el1fzopredsuc  47921  2ffzoeq  47923  uniimaprimaeqfv  47989  elsetpreimafveqfv  47999  iccpartimp  48024  iccpartrn  48037  iccpartf  48038  iccpartnel  48045  fargshiftf  48047  fargshiftfo  48049  ichnfimlem  48070  ichnfim  48071  ichreuopeq  48080  sprel  48091  sprsymrelfvlem  48097  sprsymrelfolem2  48100  prproropf1olem4  48113  prprelb  48123  poprelb  48131  fmtnofac1  48180  prmdvdsfmtnof1lem2  48195  31prm  48207  lighneallem3  48217  ppivalnnnprm  48238  nn0o1gt2ALTV  48317  nn0oALTV  48319  odd2prm2  48341  mogoldbblem  48343  fpprbasnn  48352  fpprnn  48353  sbgoldbaltlem1  48402  nnsum3primesle9  48417  bgoldbtbndlem1  48428  bgoldbtbndlem2  48429  grimedgi  48559  grtriproplem  48562  grtriprop  48564  cycl3grtrilem  48569  cycl3grtri  48570  isubgr3stgrlem8  48596  gpgvtxel2  48671  gpgedgiov  48688  gpgedg2iv  48690  gpgprismgr4cycllem7  48724  pgnbgreunbgrlem1  48736  pgnbgreunbgrlem2lem1  48737  pgnbgreunbgrlem2lem2  48738  pgnbgreunbgrlem2lem3  48739  pgnbgreunbgrlem2  48740  pgnbgreunbgrlem4  48742  pgnbgreunbgrlem5  48746  upwlkbprop  48761  clcllaw  48814  intop  48826  assintop  48832  assintopcllaw  48835  elrngchomALTV  48892  rngccatidALTV  48895  rngcinvALTV  48899  rngcisoALTV  48900  rhmsubcALTVlem3  48906  rhmsubcALTVlem4  48907  funcringcsetcALTV2lem7  48919  elringchomALTV  48926  ringccatidALTV  48929  ringcisoALTV  48934  funcringcsetclem7ALTV  48942  ztprmneprm  48970  suppmptcfin  48999  linccl  49037  linc1  49048  lincolss  49057  ldepspr  49096  nn0sumshdiglem1  49244  0aryfvalelfv  49258  rrxlines  49356  rrxsphere  49371  itsclc0yqsol  49387  itschlc0xyqsol1  49389  fdomne0  49472  f002  49476  fvconstr2  49486  fullthinc  50072