Theorem biimtrdi 256

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 232	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 36	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:  ax12i  1999  sb4a  2510  hbsb2  2512  dfsb2  2523  2eu2  2678  reu6  3684  nrmod  3839  2reu2  3846  disjel  4410  disjpss  4414  preq12b  4810  prneimg  4814  preqsnd  4819  elinti  4916  zfrepclf  5244  exnelv  5267  dtruALT2  5332  opth1g  5447  sbcop1  5458  snopeqop  5478  propeqop  5479  otsndisj  5492  otiunsndisj  5493  iunopeqop  5494  iunopeqopOLD  5495  po2ne  5575  soasym  5592  elrelb  5775  elreldm  5917  dfres3  5975  relcnvtrgOLD  6269  relresfldOLD  6279  elpredimg  6319  ordtr2  6408  ordssun  6467  funopg  6574  funimass2  6623  f0dom0  6766  elfv2ex  6928  fveqdmss  7078  eldmrexrnb  7092  fvcofneq  7093  funopsn  7151  funopsnOLD  7152  funopdmsn  7154  funsndifnop  7155  elunirn  7255  oprabidw  7451  oprabid  7452  brfvopab  7477  limuni3  7863  peano5  7905  resf1ext2b  7947  op1steq  8045  el2mpocsbcl  8096  bropopvvv  8101  bropfvvvv  8103  f1o2ndf1  8133  frxp  8138  fnwelem  8143  poxp2  8160  suppimacnv  8191  fvn0elsuppb  8198  suppfnss  8206  reldmtpos  8251  rntpos  8256  seqomlem2  8461  oaordi  8554  oa00  8567  oalimcl  8568  omeulem1  8590  nnaordi  8627  ecopovtrn  8841  undifixp  8962  mapdom2  9167  unxpdomlem3  9249  en1eqsn  9266  infssuni  9335  wdompwdom  9572  preleqg  9616  opthreg  9619  inf3lemd  9628  inf3lem2  9630  inf3lem6  9634  cnfcomlem  9700  cnfcom3  9705  karden  9959  kardenOLD  9960  carden2a  10047  alephdom  10160  dfac5lem4  10205  dfac12r  10225  kmlem2  10230  kmlem12  10240  cfslb2n  10346  alephsing  10354  fin23lem30  10420  fin1a2lem6  10483  fin1a2lem13  10490  axcc2lem  10514  domtriomlem  10520  axdc3lem2  10529  axdc4lem  10533  brdom6disj  10611  alephexp1  10664  pwfseq  10749  addnidpi  10986  indpi  10992  nqereu  11014  ltsonq  11054  distrlem5pr  11112  addcanpr  11131  suplem1pr  11137  suplem2pr  11138  ltsrpr  11162  ltsosr  11179  sqgt0sr  11191  leltne  11399  ltnsym  11408  ltlen  11411  eqlei  11420  eqlei2  11421  infm3  12276  nnunb  12602  0mnnnnn0  12638  elnnnn0b  12650  nn0ge2m1nn  12676  nn0le2is012  12763  btwnz  12802  uz11  12990  xrleltne  13274  xltnegi  13346  xnn0lenn0nn0  13375  xnn0xadd0  13377  xmulasslem2  13412  reltxrnmnf  13473  icogelb  13527  iccleub  13532  uznfz  13744  2ffzeq  13783  elfzonlteqm1  13876  elfzo0l  13891  fzoopth  13897  elfznelfzob  13909  elfzr  13916  elfzlmr  13917  injresinjlem  13925  injresinj  13926  fleqceilz  13994  modadd1  14048  modmul1  14067  modirr  14085  addmodlteq  14089  uzrdgfni  14101  fsuppmapnn0fiub0  14136  fsuppmapnn0ub  14138  seqf1o  14186  expnngt1  14385  hashrabsn01  14517  hashrabsn1  14518  hash1snb  14564  hash1n0  14566  hashf1lem2  14601  hash2prde  14615  hash2prd  14620  hash2pwpr  14621  hashle2pr  14622  hashle2prv  14623  hashge2el2dif  14625  hashge2el2difr  14626  hash3tpde  14638  fundmge2nop0  14647  ffz0iswrd  14686  ccatrcl1  14741  pfxsuff1eqwrdeq  14848  wrdind  14871  wrd2ind  14872  swrdccatin1  14874  swrdccat3blem  14888  2cshwcshw  14976  cshwcsh2id  14979  cshimadifsn  14980  2swrd2eqwrdeq  15106  wwlktovf  15109  wwlktovfo  15111  s3sndisj  15120  s3iunsndisj  15121  relexpindlem  15216  rexico  15521  lo1le  15819  fsum2dlem  15936  ntrivcvg  16066  fprodss  16115  fprod2dlem  16147  0dvds  16446  mod2eq1n2dvds  16517  opoe  16533  omoe  16534  opeo  16535  omeo  16536  m1exp1  16546  nn0enne  16547  nn0o1gt2  16551  gcdneg  16694  dfgcd2  16719  algcvga  16754  eucalglt  16760  lcmf  16808  coprmdvds  16828  divgcdcoprmex  16841  cncongr1  16842  prm2orodd  16866  prm23lt5  16992  pockthi  17085  prmreclem5  17098  ramtcl2  17189  cshwrepswhash1  17280  f1ocpbl  17697  f1ovscpbl  17698  f1olecpbl  17699  monhom  17910  epihom  17917  inveq  17949  invcoisoid  17967  isocoinvid  17968  ciclcl  17977  cicrcl  17978  isinitoi  18174  istermoi  18175  2initoinv  18185  2termoinv  18192  setciso  18266  embedsetcestrclem  18331  ipopos  18710  mgmpropd  18829  gsumval2a  18874  ismnddef  18925  dfgrp2e  19174  symg2bas  19607  snsymgefmndeq  19609  symgvalstruct  19611  symgfix2  19630  gsmsymgreq  19646  pmtrdifellem4  19693  mndodcongi  19757  pj1eu  19910  cycsubmcmn  20103  dprd2da  20258  rngimf1o  20684  rngimrnghm  20685  c0snmgmhm  20692  0ring01eq  20780  elrngchom  20876  rnghmsubcsetclem1  20883  rnghmsubcsetclem2  20884  rngcid  20887  rngcinv  20889  rngciso  20890  funcrngcsetcALT  20893  zrinitorngc  20894  zrtermorngc  20895  elringchom  20905  rhmsubcsetclem1  20912  rhmsubcsetclem2  20913  ringcid  20916  rhmsubcrngclem1  20918  rhmsubcrngclem2  20919  ringciso  20924  zrtermoringc  20927  rhmsubclem3  20939  rhmsubclem4  20940  lmodfopnelem1  21173  lspdisjb  21404  lspsnsubn0  21418  rngqiprngfulem2  21608  irinitoringc  21785  obs2ss  22035  mamufacex  22711  mat0dim0  22782  mat0dimid  22783  mat0dimscm  22784  dmatmat  22809  scmatmat  22824  mat1scmat  22854  1mavmul  22863  mavmulsolcl  22866  gsummatr01  22974  matunitlindf  22996  cpmatpmat  23028  cpmadugsumlemF  23194  tg2  23283  tgcl  23287  neii1  23424  neii2  23426  neindisj2  23441  perfopn  23503  ordtbas2  23509  pnfnei  23538  mnfnei  23539  llyidm  23807  txlm  23967  qtopuni  24021  tgqtop  24031  isfild  24177  snfil  24183  fbunfip  24188  fgss2  24193  fmco  24280  fbflim2  24296  cnpflf2  24319  fcfelbas  24355  fcfneii  24356  alexsubALTlem2  24367  alexsubALT  24370  tgpconncompeqg  24431  tsmscl  24454  tngngpim  24978  tgioo  25115  xrsmopn  25132  iccntr  25141  reconnlem2  25147  addcnlem  25184  htpycn  25294  phtpyhtpy  25303  pi1blem  25360  fgcfil  25592  ioombl1lem4  25882  dyadmbl  25921  itg2gt0  26081  ditgneg  26177  dvivthlem1  26328  coeeq2  26561  aannenlem2  26656  sineq0  26852  efif1o  26874  xrlimcnp  27296  vmacl  27445  efvmacl  27447  vmalelog  27532  dchrelbasd  27566  lgsqr  27678  lgsqrmodndvds  27680  gausslemma2dlem0i  27691  2lgslem2  27722  2lgs  27734  2lgsoddprmlem3  27741  2sqnn  27766  2sqreultlem  27774  2sqreultblem  27775  2sqreunnltlem  27777  2sqreunnltblem  27778  ltsintdifex  28018  ltsres  28019  nosepnelem  28036  nolt02o  28052  ltlesnd  28132  negsprop  28421  mulsprop  28516  onnolt  28652  onlts  28653  n0subs  28749  bdaypw2n0bndlem  28849  bdaypw2n0bnd  28850  bdayfinbndlem2  28854  elntg2  29563  uhgr0vb  29650  umgrupgr  29681  umgrnloopv  29684  umgredgprv  29685  umgrislfupgrlem  29700  umgredg  29716  uspgrushgr  29758  uspgrupgr  29759  usgruspgr  29761  usgredgprvALT  29776  usgrnloopvALT  29782  uhgr2edg  29789  edg0usgr  29834  egrsubgr  29858  0uhgrsubgr  29860  uhgrspansubgrlem  29871  nbuhgr  29924  cusgrsize2inds  30034  cusgrfilem2  30037  vtxdg0v  30054  1loopgrnb0  30083  vtxdginducedm1lem4  30123  wlkvtxeledg  30204  wlkeq  30214  wlkl1loop  30218  wlk1walk  30219  upgrwlkedg  30222  uspgr2wlkeq  30226  wlkv0  30230  wlkonl1iedg  30244  wlkon2n0  30245  wlkp1lem8  30259  wlkp1  30260  lfgrwlkprop  30270  lfgrwlknloop  30272  2pthnloop  30317  upgrwlkdvde  30323  spthonepeq  30338  uhgrwkspthlem2  30340  usgr2wlkneq  30342  usgr2trlncl  30346  usgr2trlspth  30347  pthdlem2lem  30353  clwlkcompbp  30369  uspgrn2crct  30397  wwlks  30424  wwlknbp  30431  0enwwlksnge1  30453  wwlkswwlksn  30454  wlklnwwlkln1  30457  wwlksnextproplem3  30500  wwlksnextprop  30501  wspthsnonn0vne  30506  wspn0  30513  2pthon3v  30532  umgr2adedgspth  30537  rusgr0edg  30565  clwwlkccat  30581  clwlkclwwlklem2fv2  30587  clwlkclwwlklem2a4  30588  clwlkclwwlklem2  30591  clwlkclwwlkflem  30595  clwwlknp  30628  clwwlkwwlksb  30645  clwwlkext2edg  30647  erclwwlkneqlen  30659  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  clwwlknonwwlknonb  30697  upgr1wlkdlem1  30736  upgr3v3e3cycl  30781  uhgr3cyclexlem  30782  1conngr  30795  conngrv2edg  30796  eupth2lem3lem4  30832  eulercrct  30843  isfrgr  30861  frgr3vlem2  30875  1to2vfriswmgr  30880  1to3vfriswmgr  30881  frgrncvvdeqlem9  30908  frgrwopreg  30924  frgr2wwlkeqm  30932  2wspmdisj  30938  numclwwlk1lem2f  30956  frgrreggt1  30994  frgrregord013  30996  frgrregord13  30997  l2p  31081  nmlno0lem  31395  normgt0  31729  ocin  31898  nmlnop0iALT  32597  nmopun  32616  cvpss  32887  cvnbtwn  32888  atcvati  32988  mdsymlem6  33010  iunrnmptss  33159  expgt0b  33408  wrdt2ind  33516  irngssv  34320  issgon  34755  mbfmcnt  34900  ballotlemfc0  35125  ballotlemfcc  35126  jaeqifi  35710  kardcard2b  35833  satfv0  36123  satfv0fun  36136  fmla1  36152  gonarlem  36159  gonar  36160  goalrlem  36161  goalr  36162  fmla0disjsuc  36163  satffunlem  36166  satffunlem1lem1  36167  satffunlem2lem1  36169  satfun  36176  satfv0fvfmla0  36178  sategoelfv  36185  mthmblem  36345  pprodss4v  36646  funpartfun  36707  funpartfv  36709  5segofs  36771  btwnxfr  36821  brofs2  36842  brifs2  36843  btwnconn1  36866  segleantisym  36880  broutsideof2  36887  outsidene1  36888  outsidene2  36889  funray  36905  lineunray  36912  cldbnd  37114  bj-imdirval3  38105  topdifinffinlem  38270  isbasisrelowllem1  38278  isbasisrelowllem2  38279  relowlpssretop  38287  inunissunidif  38298  pibt2  38340  poimir  38571  volsupnfl  38583  itg2addnclem  38589  findcard4  38632  cover2  38649  sdclem2  38676  fdc  38679  sstotbnd3  38710  heibor1  38744  clmgmOLD  38785  smgrpmgm  38798  smgrpassOLD  38799  dvrunz  38888  0rngo  38961  mopickr  39303  sucmapleftuniq  39422  lsatcvat  40107  lshpkrex  40175  cmtbr3N  40311  atn0  40365  atnle  40374  cvlsupr4  40402  cvlsupr5  40403  cvlsupr6  40404  cvrval4N  40471  cvratlem  40478  2llnjN  40624  2lplnj  40677  linepsubN  40809  elpaddatiN  40862  elpcliN  40950  pclcmpatN  40958  ldilval  41170  ltrnu  41178  cdleme18d  41352  tendotp  41818  tendof  41820  tendovalco  41822  diatrl  42101  diaintclN  42115  dvheveccl  42169  dibintclN  42224  dihord6apre  42313  dihmeetlem1N  42347  dihpN  42393  dihintcl  42401  dochkrshp4  42446  oexpreposd  43379  pw2f1ocnv  44043  iocinico  44213  onsucf1olem  44271  succlg  44329  oacl2g  44331  omabs2  44333  omcl2  44334  naddcnfcom  44367  naddcnfass  44370  safesnsupfidom1o  44417  infordmin  44532  pr2cv  44548  expgrowthi  45316  iotavalsb  45416  bi23imp1  45477  ioogtlb  46506  iocgtlb  46513  iocleub  46514  icoltub  46519  iooltub  46521  stoweidlem31  47040  oppr  48099  funressnfv  48112  fsetsniunop  48118  fsetsnf1  48121  eu2ndop1stv  48194  afvelrnb0  48233  otiunsndisjX  48348  el1fzopredsuc  48395  2ffzoeq  48397  uniimaprimaeqfv  48463  elsetpreimafveqfv  48473  iccpartimp  48498  iccpartrn  48511  iccpartf  48512  iccpartnel  48519  fargshiftf  48521  fargshiftfo  48523  ichnfimlem  48544  ichnfim  48545  ichreuopeq  48554  sprel  48565  sprsymrelfvlem  48571  sprsymrelfolem2  48574  prproropf1olem4  48587  prprelb  48597  poprelb  48605  fmtnofac1  48654  prmdvdsfmtnof1lem2  48669  31prm  48681  lighneallem3  48691  ppivalnnnprm  48712  nn0o1gt2ALTV  48791  nn0oALTV  48793  odd2prm2  48815  mogoldbblem  48817  fpprbasnn  48826  fpprnn  48827  sbgoldbaltlem1  48876  nnsum3primesle9  48891  bgoldbtbndlem1  48902  bgoldbtbndlem2  48903  elclnbgrelnbgr  48922  grimedgi  49033  grtriproplem  49036  grtriprop  49038  cycl3grtrilem  49043  cycl3grtri  49044  isubgr3stgrlem8  49070  gpgvtxel2  49145  gpgedgiov  49162  gpgedg2iv  49164  gpgprismgr4cycllem7  49198  pgnbgreunbgrlem1  49210  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  pgnbgreunbgrlem2lem3  49213  pgnbgreunbgrlem2  49214  pgnbgreunbgrlem4  49216  pgnbgreunbgrlem5  49220  upwlkbprop  49235  clcllaw  49287  intop  49299  assintop  49305  assintopcllaw  49308  elrngchomALTV  49365  rngccatidALTV  49368  rngcinvALTV  49372  rngcisoALTV  49373  rhmsubcALTVlem3  49379  rhmsubcALTVlem4  49380  funcringcsetcALTV2lem7  49392  elringchomALTV  49399  ringccatidALTV  49402  ringcisoALTV  49407  funcringcsetclem7ALTV  49415  prmringnzring  49433  ztprmneprm  49458  suppmptcfin  49487  linccl  49525  linc1  49536  lincolss  49545  ldepspr  49584  nn0sumshdiglem1  49732  0aryfvalelfv  49746  rrxlines  49844  rrxsphere  49859  itsclc0yqsol  49875  itschlc0xyqsol1  49877  fdomne0  49959  f002  49963  elovconstbrd  49973  fullthinc  50557