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  2485  hbsb2  2487  dfsb2  2498  2eu2  2654  reu6  3686  2reu2  3850  sseq0  4357  disjel  4411  disjpss  4415  preq12b  4808  prneimg  4812  preqsnd  4817  elinti  4913  zfrepclf  5240  dtruALT2  5319  opth1g  5436  sbcop1  5446  snopeqop  5464  propeqop  5465  otsndisj  5477  otiunsndisj  5478  iunopeqop  5479  po2ne  5558  soasym  5575  elreldm  5894  dfres3  5953  relcnvtrg  6235  relresfld  6244  elpredimg  6284  ordtr2  6372  ordssun  6431  funopg  6536  funimass2  6585  f1imadifssran  6588  f0dom0  6728  elfv2ex  6887  fveqdmss  7034  eldmrexrnb  7048  fvcofneq  7049  funopsn  7105  funopdmsn  7107  funsndifnop  7108  elunirn  7209  oprabidw  7401  oprabid  7402  brfvopab  7427  limuni3  7806  peano5  7847  resf1ext2b  7889  op1steq  7989  el2mpocsbcl  8039  bropopvvv  8044  bropfvvvv  8046  f1o2ndf1  8076  frxp  8080  fnwelem  8085  poxp2  8097  suppimacnv  8128  fvn0elsuppb  8135  suppfnss  8143  reldmtpos  8188  rntpos  8193  seqomlem2  8394  oaordi  8485  oa00  8498  oalimcl  8499  omeulem1  8521  nnaordi  8558  ecopovtrn  8771  undifixp  8886  mapdom2  9090  unxpdomlem3  9172  en1eqsn  9189  infssuni  9260  wdompwdom  9497  preleqg  9538  opthreg  9541  inf3lemd  9550  inf3lem2  9552  inf3lem6  9556  cnfcomlem  9622  cnfcom3  9627  karden  9821  carden2a  9892  alephdom  10005  dfac5lem4  10050  dfac5lem4OLD  10052  dfac12r  10071  kmlem2  10076  kmlem12  10086  cfslb2n  10192  alephsing  10200  fin23lem30  10266  fin1a2lem6  10329  fin1a2lem13  10336  axcc2lem  10360  domtriomlem  10366  axdc3lem2  10375  axdc4lem  10379  brdom6disj  10456  alephexp1  10504  pwfseq  10589  addnidpi  10826  indpi  10832  nqereu  10854  ltsonq  10894  distrlem5pr  10952  addcanpr  10971  suplem1pr  10977  suplem2pr  10978  ltsrpr  11002  ltsosr  11019  sqgt0sr  11031  leltne  11236  ltnsym  11245  ltlen  11248  eqlei  11257  eqlei2  11258  infm3  12115  nnunb  12411  0mnnnnn0  12447  elnnnn0b  12459  nn0ge2m1nn  12485  nn0le2is012  12570  btwnz  12609  uz11  12790  xrleltne  13073  xltnegi  13145  xnn0lenn0nn0  13174  xnn0xadd0  13176  xmulasslem2  13211  reltxrnmnf  13272  icogelb  13326  iccleub  13331  uznfz  13540  2ffzeq  13579  elfzonlteqm1  13671  elfzo0l  13686  fzoopth  13692  elfznelfzob  13704  elfzr  13711  elfzlmr  13712  injresinjlem  13720  injresinj  13721  fleqceilz  13788  modadd1  13842  modmul1  13861  modirr  13879  addmodlteq  13883  uzrdgfni  13895  fsuppmapnn0fiub0  13930  fsuppmapnn0ub  13932  seqf1o  13980  expnngt1  14178  hashrabsn01  14310  hashrabsn1  14311  hash1snb  14356  hash1n0  14358  hashf1lem2  14393  hash2prde  14407  hash2prd  14412  hash2pwpr  14413  hashle2pr  14414  hashle2prv  14415  hashge2el2dif  14417  hashge2el2difr  14418  hash3tpde  14430  fundmge2nop0  14439  ffz0iswrd  14478  ccatrcl1  14532  pfxsuff1eqwrdeq  14636  wrdind  14659  wrd2ind  14660  swrdccatin1  14662  swrdccat3blem  14676  2cshwcshw  14762  cshwcsh2id  14765  cshimadifsn  14766  2swrd2eqwrdeq  14890  wwlktovf  14893  wwlktovfo  14895  s3sndisj  14904  s3iunsndisj  14905  relexpindlem  15000  rexico  15291  lo1le  15589  fsum2dlem  15707  ntrivcvg  15834  fprodss  15885  fprod2dlem  15917  0dvds  16217  mod2eq1n2dvds  16288  opoe  16304  omoe  16305  opeo  16306  omeo  16307  m1exp1  16317  nn0enne  16318  nn0o1gt2  16322  gcdneg  16463  dfgcd2  16487  algcvga  16520  eucalglt  16526  lcmf  16574  coprmdvds  16594  divgcdcoprmex  16607  cncongr1  16608  prm2orodd  16632  prm23lt5  16756  pockthi  16849  prmreclem5  16862  ramtcl2  16953  cshwrepswhash1  17044  f1ocpbl  17460  f1ovscpbl  17461  f1olecpbl  17462  monhom  17673  epihom  17680  inveq  17712  invcoisoid  17730  isocoinvid  17731  ciclcl  17740  cicrcl  17741  isinitoi  17937  istermoi  17938  2initoinv  17948  2termoinv  17955  setciso  18029  embedsetcestrclem  18094  ipopos  18473  mgmpropd  18590  gsumval2a  18624  ismnddef  18675  dfgrp2e  18910  symg2bas  19339  snsymgefmndeq  19341  symgvalstruct  19343  symgfix2  19362  gsmsymgreq  19378  pmtrdifellem4  19425  mndodcongi  19489  pj1eu  19642  cycsubmcmn  19835  dprd2da  19990  rngimf1o  20407  rngimrnghm  20408  c0snmgmhm  20415  0ring01eq  20479  elrngchom  20574  rnghmsubcsetclem1  20581  rnghmsubcsetclem2  20582  rngcid  20585  rngcinv  20587  rngciso  20588  funcrngcsetcALT  20591  zrinitorngc  20592  zrtermorngc  20593  elringchom  20603  rhmsubcsetclem1  20610  rhmsubcsetclem2  20611  ringcid  20614  rhmsubcrngclem1  20616  rhmsubcrngclem2  20617  ringciso  20622  zrtermoringc  20625  rhmsubclem3  20637  rhmsubclem4  20638  lmodfopnelem1  20866  lspdisjb  21098  lspsnsubn0  21112  rngqiprngfulem2  21284  irinitoringc  21451  obs2ss  21701  mamufacex  22357  mat0dim0  22428  mat0dimid  22429  mat0dimscm  22430  dmatmat  22455  scmatmat  22470  mat1scmat  22500  1mavmul  22509  mavmulsolcl  22512  gsummatr01  22620  cpmatpmat  22671  cpmadugsumlemF  22837  tg2  22926  tgcl  22930  neii1  23067  neii2  23069  neindisj2  23084  perfopn  23146  ordtbas2  23152  pnfnei  23181  mnfnei  23182  llyidm  23449  txlm  23609  qtopuni  23663  tgqtop  23673  isfild  23819  snfil  23825  fbunfip  23830  fgss2  23835  fmco  23922  fbflim2  23938  cnpflf2  23961  fcfelbas  23997  fcfneii  23998  alexsubALTlem2  24009  alexsubALT  24012  tgpconncompeqg  24073  tsmscl  24096  tngngpim  24620  tgioo  24757  xrsmopn  24774  iccntr  24783  reconnlem2  24789  addcnlem  24826  htpycn  24945  phtpyhtpy  24954  pi1blem  25012  fgcfil  25244  ioombl1lem4  25535  dyadmbl  25574  itg2gt0  25734  ditgneg  25831  dvivthlem1  25986  coeeq2  26220  aannenlem2  26310  sineq0  26506  efif1o  26528  xrlimcnp  26951  vmacl  27101  efvmacl  27103  vmalelog  27189  dchrelbasd  27223  lgsqr  27335  lgsqrmodndvds  27337  gausslemma2dlem0i  27348  2lgslem2  27379  2lgs  27391  2lgsoddprmlem3  27398  2sqnn  27423  2sqreultlem  27431  2sqreultblem  27432  2sqreunnltlem  27434  2sqreunnltblem  27435  ltsintdifex  27646  ltsres  27647  nosepnelem  27664  nolt02o  27680  ltlesnd  27760  negsprop  28048  mulsprop  28143  onnolt  28279  onlts  28280  n0subs  28376  bdaypw2n0bndlem  28476  bdaypw2n0bnd  28477  bdayfinbndlem2  28481  elntg2  29076  uhgr0vb  29163  umgrupgr  29194  umgrnloopv  29197  umgredgprv  29198  umgrislfupgrlem  29213  umgredg  29229  uspgrushgr  29268  uspgrupgr  29269  usgruspgr  29271  usgredgprvALT  29286  usgrnloopvALT  29292  uhgr2edg  29299  edg0usgr  29344  egrsubgr  29368  0uhgrsubgr  29370  uhgrspansubgrlem  29381  nbuhgr  29434  cusgrsize2inds  29545  cusgrfilem2  29548  vtxdg0v  29565  1loopgrnb0  29594  vtxdginducedm1lem4  29634  wlkvtxeledg  29715  wlkeq  29725  wlkl1loop  29729  wlk1walk  29730  upgrwlkedg  29733  uspgr2wlkeq  29737  wlkv0  29741  wlkonl1iedg  29755  wlkon2n0  29756  wlkp1lem8  29770  wlkp1  29771  lfgrwlkprop  29777  lfgrwlknloop  29779  2pthnloop  29822  upgrwlkdvde  29828  spthonepeq  29843  uhgrwkspthlem2  29845  usgr2wlkneq  29847  usgr2trlncl  29851  usgr2trlspth  29852  pthdlem2lem  29858  clwlkcompbp  29873  uspgrn2crct  29899  wwlks  29926  wwlknbp  29933  0enwwlksnge1  29955  wwlkswwlksn  29956  wlklnwwlkln1  29959  wwlksnextproplem3  30002  wwlksnextprop  30003  wspthsnonn0vne  30008  wspn0  30015  2pthon3v  30034  umgr2adedgspth  30039  rusgr0edg  30067  clwwlkccat  30083  clwlkclwwlklem2fv2  30089  clwlkclwwlklem2a4  30090  clwlkclwwlklem2  30093  clwlkclwwlkflem  30097  clwwlknp  30130  clwwlkwwlksb  30147  clwwlkext2edg  30149  erclwwlkneqlen  30161  hashecclwwlkn1  30170  umgrhashecclwwlk  30171  clwwlknonwwlknonb  30199  upgr1wlkdlem1  30238  upgr3v3e3cycl  30273  uhgr3cyclexlem  30274  1conngr  30287  conngrv2edg  30288  eupth2lem3lem4  30324  eulercrct  30335  isfrgr  30353  frgr3vlem2  30367  1to2vfriswmgr  30372  1to3vfriswmgr  30373  frgrncvvdeqlem9  30400  frgrwopreg  30416  frgr2wwlkeqm  30424  2wspmdisj  30430  numclwwlk1lem2f  30448  frgrreggt1  30486  frgrregord013  30488  frgrregord13  30489  l2p  30573  nmlno0lem  30887  normgt0  31221  ocin  31390  nmlnop0iALT  32089  nmopun  32108  cvpss  32379  cvnbtwn  32380  atcvati  32480  mdsymlem6  32502  iunrnmptss  32658  expgt0b  32914  wrdt2ind  33052  irngssv  33872  issgon  34307  mbfmcnt  34452  ballotlemfc0  34677  ballotlemfcc  34678  satfv0  35580  satfv0fun  35593  fmla1  35609  gonarlem  35616  gonar  35617  goalrlem  35618  goalr  35619  fmla0disjsuc  35620  satffunlem  35623  satffunlem1lem1  35624  satffunlem2lem1  35626  satfun  35633  satfv0fvfmla0  35635  sategoelfv  35642  mthmblem  35802  pprodss4v  36104  funpartfun  36165  funpartfv  36167  5segofs  36228  btwnxfr  36278  brofs2  36299  brifs2  36300  btwnconn1  36323  segleantisym  36337  broutsideof2  36344  outsidene1  36345  outsidene2  36346  funray  36362  lineunray  36369  cldbnd  36548  bj-imdirval3  37466  topdifinffinlem  37629  isbasisrelowllem1  37637  isbasisrelowllem2  37638  relowlpssretop  37646  inunissunidif  37657  pibt2  37699  matunitlindf  37898  poimir  37933  volsupnfl  37945  itg2addnclem  37951  cover2  37995  sdclem2  38022  fdc  38025  sstotbnd3  38056  heibor1  38090  clmgmOLD  38131  smgrpmgm  38144  smgrpassOLD  38145  dvrunz  38234  0rngo  38307  mopickr  38651  sucmapleftuniq  38770  lsatcvat  39455  lshpkrex  39523  cmtbr3N  39659  atn0  39713  atnle  39722  cvlsupr4  39750  cvlsupr5  39751  cvlsupr6  39752  cvrval4N  39819  cvratlem  39826  2llnjN  39972  2lplnj  40025  linepsubN  40157  elpaddatiN  40210  elpcliN  40298  pclcmpatN  40306  ldilval  40518  ltrnu  40526  cdleme18d  40700  tendotp  41166  tendof  41168  tendovalco  41170  diatrl  41449  diaintclN  41463  dvheveccl  41517  dibintclN  41572  dihord6apre  41661  dihmeetlem1N  41695  dihpN  41741  dihintcl  41749  dochkrshp4  41794  oexpreposd  42721  pw2f1ocnv  43423  iocinico  43598  onsucf1olem  43656  succlg  43714  oacl2g  43716  omabs2  43718  omcl2  43719  naddcnfcom  43752  naddcnfass  43755  safesnsupfidom1o  43802  infordmin  43917  pr2cv  43933  expgrowthi  44718  iotavalsb  44818  bi23imp1  44880  ioogtlb  45884  iocgtlb  45891  iocleub  45892  icoltub  45897  iooltub  45899  stoweidlem31  46418  oppr  47419  funressnfv  47432  fsetsniunop  47438  fsetsnf1  47441  eu2ndop1stv  47514  afvelrnb0  47553  otiunsndisjX  47668  el1fzopredsuc  47714  2ffzoeq  47716  uniimaprimaeqfv  47771  elsetpreimafveqfv  47781  iccpartimp  47806  iccpartrn  47819  iccpartf  47820  iccpartnel  47827  fargshiftf  47829  fargshiftfo  47831  ichnfimlem  47852  ichnfim  47853  ichreuopeq  47862  sprel  47873  sprsymrelfvlem  47879  sprsymrelfolem2  47882  prproropf1olem4  47895  prprelb  47905  poprelb  47913  fmtnofac1  47959  prmdvdsfmtnof1lem2  47974  31prm  47986  lighneallem3  47996  nn0o1gt2ALTV  48083  nn0oALTV  48085  odd2prm2  48107  mogoldbblem  48109  fpprbasnn  48118  fpprnn  48119  sbgoldbaltlem1  48168  nnsum3primesle9  48183  bgoldbtbndlem1  48194  bgoldbtbndlem2  48195  grimedgi  48325  grtriproplem  48328  grtriprop  48330  cycl3grtrilem  48335  cycl3grtri  48336  isubgr3stgrlem8  48362  gpgvtxel2  48437  gpgedgiov  48454  gpgedg2iv  48456  gpgprismgr4cycllem7  48490  pgnbgreunbgrlem1  48502  pgnbgreunbgrlem2lem1  48503  pgnbgreunbgrlem2lem2  48504  pgnbgreunbgrlem2lem3  48505  pgnbgreunbgrlem2  48506  pgnbgreunbgrlem4  48508  pgnbgreunbgrlem5  48512  upwlkbprop  48527  clcllaw  48580  intop  48592  assintop  48598  assintopcllaw  48601  elrngchomALTV  48658  rngccatidALTV  48661  rngcinvALTV  48665  rngcisoALTV  48666  rhmsubcALTVlem3  48672  rhmsubcALTVlem4  48673  funcringcsetcALTV2lem7  48685  elringchomALTV  48692  ringccatidALTV  48695  ringcisoALTV  48700  funcringcsetclem7ALTV  48708  ztprmneprm  48736  suppmptcfin  48765  linccl  48803  linc1  48814  lincolss  48823  ldepspr  48862  nn0sumshdiglem1  49010  0aryfvalelfv  49024  rrxlines  49122  rrxsphere  49137  itsclc0yqsol  49153  itschlc0xyqsol1  49155  fdomne0  49238  f002  49242  fvconstr2  49252  fullthinc  49838