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  2480  hbsb2  2482  dfsb2  2493  2eu2  2648  reu6  3680  2reu2  3844  sseq0  4350  disjel  4404  disjpss  4408  preq12b  4799  prneimg  4803  preqsnd  4808  elinti  4904  zfrepclf  5227  dtruALT2  5306  opth1g  5416  sbcop1  5426  snopeqop  5444  propeqop  5445  otsndisj  5457  otiunsndisj  5458  iunopeqop  5459  po2ne  5538  soasym  5555  elreldm  5874  dfres3  5932  relcnvtrg  6214  relresfld  6223  elpredimg  6263  ordtr2  6351  ordssun  6410  funopg  6515  funimass2  6564  f1imadifssran  6567  f0dom0  6707  elfv2ex  6865  fveqdmss  7011  eldmrexrnb  7025  fvcofneq  7026  funopsn  7081  funopdmsn  7083  funsndifnop  7084  elunirn  7185  oprabidw  7377  oprabid  7378  brfvopab  7403  limuni3  7782  peano5  7823  resf1ext2b  7865  op1steq  7965  el2mpocsbcl  8015  bropopvvv  8020  bropfvvvv  8022  f1o2ndf1  8052  frxp  8056  fnwelem  8061  poxp2  8073  suppimacnv  8104  fvn0elsuppb  8111  suppfnss  8119  reldmtpos  8164  rntpos  8169  seqomlem2  8370  oaordi  8461  oa00  8474  oalimcl  8475  omeulem1  8497  nnaordi  8533  ecopovtrn  8744  undifixp  8858  mapdom2  9061  unxpdomlem3  9142  en1eqsn  9159  infssuni  9230  wdompwdom  9464  preleqg  9505  opthreg  9508  inf3lemd  9517  inf3lem2  9519  inf3lem6  9523  cnfcomlem  9589  cnfcom3  9594  karden  9788  carden2a  9859  alephdom  9972  dfac5lem4  10017  dfac5lem4OLD  10019  dfac12r  10038  kmlem2  10043  kmlem12  10053  cfslb2n  10159  alephsing  10167  fin23lem30  10233  fin1a2lem6  10296  fin1a2lem13  10303  axcc2lem  10327  domtriomlem  10333  axdc3lem2  10342  axdc4lem  10346  brdom6disj  10423  alephexp1  10470  pwfseq  10555  addnidpi  10792  indpi  10798  nqereu  10820  ltsonq  10860  distrlem5pr  10918  addcanpr  10937  suplem1pr  10943  suplem2pr  10944  ltsrpr  10968  ltsosr  10985  sqgt0sr  10997  leltne  11202  ltnsym  11211  ltlen  11214  eqlei  11223  eqlei2  11224  infm3  12081  nnunb  12377  0mnnnnn0  12413  elnnnn0b  12425  nn0ge2m1nn  12451  nn0le2is012  12537  btwnz  12576  uz11  12757  xrleltne  13044  xltnegi  13115  xnn0lenn0nn0  13144  xnn0xadd0  13146  xmulasslem2  13181  reltxrnmnf  13242  icogelb  13296  iccleub  13301  uznfz  13510  2ffzeq  13549  elfzonlteqm1  13641  elfzo0l  13656  fzoopth  13662  elfznelfzob  13674  elfzr  13681  elfzlmr  13682  injresinjlem  13690  injresinj  13691  fleqceilz  13758  modadd1  13812  modmul1  13831  modirr  13849  addmodlteq  13853  uzrdgfni  13865  fsuppmapnn0fiub0  13900  fsuppmapnn0ub  13902  seqf1o  13950  expnngt1  14148  hashrabsn01  14280  hashrabsn1  14281  hash1snb  14326  hash1n0  14328  hashf1lem2  14363  hash2prde  14377  hash2prd  14382  hash2pwpr  14383  hashle2pr  14384  hashle2prv  14385  hashge2el2dif  14387  hashge2el2difr  14388  hash3tpde  14400  fundmge2nop0  14409  ffz0iswrd  14448  ccatrcl1  14502  pfxsuff1eqwrdeq  14606  wrdind  14629  wrd2ind  14630  swrdccatin1  14632  swrdccat3blem  14646  2cshwcshw  14732  cshwcsh2id  14735  cshimadifsn  14736  2swrd2eqwrdeq  14860  wwlktovf  14863  wwlktovfo  14865  s3sndisj  14874  s3iunsndisj  14875  relexpindlem  14970  rexico  15261  lo1le  15559  fsum2dlem  15677  ntrivcvg  15804  fprodss  15855  fprod2dlem  15887  0dvds  16187  mod2eq1n2dvds  16258  opoe  16274  omoe  16275  opeo  16276  omeo  16277  m1exp1  16287  nn0enne  16288  nn0o1gt2  16292  gcdneg  16433  dfgcd2  16457  algcvga  16490  eucalglt  16496  lcmf  16544  coprmdvds  16564  divgcdcoprmex  16577  cncongr1  16578  prm2orodd  16602  prm23lt5  16726  pockthi  16819  prmreclem5  16832  ramtcl2  16923  cshwrepswhash1  17014  f1ocpbl  17429  f1ovscpbl  17430  f1olecpbl  17431  monhom  17642  epihom  17649  inveq  17681  invcoisoid  17699  isocoinvid  17700  ciclcl  17709  cicrcl  17710  isinitoi  17906  istermoi  17907  2initoinv  17917  2termoinv  17924  setciso  17998  embedsetcestrclem  18063  ipopos  18442  mgmpropd  18559  gsumval2a  18593  ismnddef  18644  dfgrp2e  18876  symg2bas  19305  snsymgefmndeq  19307  symgvalstruct  19309  symgfix2  19328  gsmsymgreq  19344  pmtrdifellem4  19391  mndodcongi  19455  pj1eu  19608  cycsubmcmn  19801  dprd2da  19956  rngimf1o  20372  rngimrnghm  20373  c0snmgmhm  20380  0ring01eq  20444  elrngchom  20539  rnghmsubcsetclem1  20546  rnghmsubcsetclem2  20547  rngcid  20550  rngcinv  20552  rngciso  20553  funcrngcsetcALT  20556  zrinitorngc  20557  zrtermorngc  20558  elringchom  20568  rhmsubcsetclem1  20575  rhmsubcsetclem2  20576  ringcid  20579  rhmsubcrngclem1  20581  rhmsubcrngclem2  20582  ringciso  20587  zrtermoringc  20590  rhmsubclem3  20602  rhmsubclem4  20603  lmodfopnelem1  20831  lspdisjb  21063  lspsnsubn0  21077  rngqiprngfulem2  21249  irinitoringc  21416  obs2ss  21666  mamufacex  22311  mat0dim0  22382  mat0dimid  22383  mat0dimscm  22384  dmatmat  22409  scmatmat  22424  mat1scmat  22454  1mavmul  22463  mavmulsolcl  22466  gsummatr01  22574  cpmatpmat  22625  cpmadugsumlemF  22791  tg2  22880  tgcl  22884  neii1  23021  neii2  23023  neindisj2  23038  perfopn  23100  ordtbas2  23106  pnfnei  23135  mnfnei  23136  llyidm  23403  txlm  23563  qtopuni  23617  tgqtop  23627  isfild  23773  snfil  23779  fbunfip  23784  fgss2  23789  fmco  23876  fbflim2  23892  cnpflf2  23915  fcfelbas  23951  fcfneii  23952  alexsubALTlem2  23963  alexsubALT  23966  tgpconncompeqg  24027  tsmscl  24050  tngngpim  24574  tgioo  24711  xrsmopn  24728  iccntr  24737  reconnlem2  24743  addcnlem  24780  htpycn  24899  phtpyhtpy  24908  pi1blem  24966  fgcfil  25198  ioombl1lem4  25489  dyadmbl  25528  itg2gt0  25688  ditgneg  25785  dvivthlem1  25940  coeeq2  26174  aannenlem2  26264  sineq0  26460  efif1o  26482  xrlimcnp  26905  vmacl  27055  efvmacl  27057  vmalelog  27143  dchrelbasd  27177  lgsqr  27289  lgsqrmodndvds  27291  gausslemma2dlem0i  27302  2lgslem2  27333  2lgs  27345  2lgsoddprmlem3  27352  2sqnn  27377  2sqreultlem  27385  2sqreultblem  27386  2sqreunnltlem  27388  2sqreunnltblem  27389  sltintdifex  27600  sltres  27601  nosepnelem  27618  nolt02o  27634  sltlend  27710  negsprop  27977  mulsprop  28069  onnolt  28203  onslt  28204  n0subs  28289  elntg2  28963  uhgr0vb  29050  umgrupgr  29081  umgrnloopv  29084  umgredgprv  29085  umgrislfupgrlem  29100  umgredg  29116  uspgrushgr  29155  uspgrupgr  29156  usgruspgr  29158  usgredgprvALT  29173  usgrnloopvALT  29179  uhgr2edg  29186  edg0usgr  29231  egrsubgr  29255  0uhgrsubgr  29257  uhgrspansubgrlem  29268  nbuhgr  29321  cusgrsize2inds  29432  cusgrfilem2  29435  vtxdg0v  29452  1loopgrnb0  29481  vtxdginducedm1lem4  29521  wlkvtxeledg  29602  wlkeq  29612  wlkl1loop  29616  wlk1walk  29617  upgrwlkedg  29620  uspgr2wlkeq  29624  wlkv0  29628  wlkonl1iedg  29642  wlkon2n0  29643  wlkp1lem8  29657  wlkp1  29658  lfgrwlkprop  29664  lfgrwlknloop  29666  2pthnloop  29709  upgrwlkdvde  29715  spthonepeq  29730  uhgrwkspthlem2  29732  usgr2wlkneq  29734  usgr2trlncl  29738  usgr2trlspth  29739  pthdlem2lem  29745  clwlkcompbp  29760  uspgrn2crct  29786  wwlks  29813  wwlknbp  29820  0enwwlksnge1  29842  wwlkswwlksn  29843  wlklnwwlkln1  29846  wwlksnextproplem3  29889  wwlksnextprop  29890  wspthsnonn0vne  29895  wspn0  29902  2pthon3v  29921  umgr2adedgspth  29926  rusgr0edg  29954  clwwlkccat  29970  clwlkclwwlklem2fv2  29976  clwlkclwwlklem2a4  29977  clwlkclwwlklem2  29980  clwlkclwwlkflem  29984  clwwlknp  30017  clwwlkwwlksb  30034  clwwlkext2edg  30036  erclwwlkneqlen  30048  hashecclwwlkn1  30057  umgrhashecclwwlk  30058  clwwlknonwwlknonb  30086  upgr1wlkdlem1  30125  upgr3v3e3cycl  30160  uhgr3cyclexlem  30161  1conngr  30174  conngrv2edg  30175  eupth2lem3lem4  30211  eulercrct  30222  isfrgr  30240  frgr3vlem2  30254  1to2vfriswmgr  30259  1to3vfriswmgr  30260  frgrncvvdeqlem9  30287  frgrwopreg  30303  frgr2wwlkeqm  30311  2wspmdisj  30317  numclwwlk1lem2f  30335  frgrreggt1  30373  frgrregord013  30375  frgrregord13  30376  l2p  30459  nmlno0lem  30773  normgt0  31107  ocin  31276  nmlnop0iALT  31975  nmopun  31994  cvpss  32265  cvnbtwn  32266  atcvati  32366  mdsymlem6  32388  iunrnmptss  32545  expgt0b  32799  wrdt2ind  32934  irngssv  33701  issgon  34136  mbfmcnt  34281  ballotlemfc0  34506  ballotlemfcc  34507  satfv0  35402  satfv0fun  35415  fmla1  35431  gonarlem  35438  gonar  35439  goalrlem  35440  goalr  35441  fmla0disjsuc  35442  satffunlem  35445  satffunlem1lem1  35446  satffunlem2lem1  35448  satfun  35455  satfv0fvfmla0  35457  sategoelfv  35464  mthmblem  35624  pprodss4v  35926  funpartfun  35987  funpartfv  35989  5segofs  36050  btwnxfr  36100  brofs2  36121  brifs2  36122  btwnconn1  36145  segleantisym  36159  broutsideof2  36166  outsidene1  36167  outsidene2  36168  funray  36184  lineunray  36191  cldbnd  36370  bj-imdirval3  37228  topdifinffinlem  37391  isbasisrelowllem1  37399  isbasisrelowllem2  37400  relowlpssretop  37408  inunissunidif  37419  pibt2  37461  matunitlindf  37668  poimir  37703  volsupnfl  37715  itg2addnclem  37721  cover2  37765  sdclem2  37792  fdc  37795  sstotbnd3  37826  heibor1  37860  clmgmOLD  37901  smgrpmgm  37914  smgrpassOLD  37915  dvrunz  38004  0rngo  38077  mopickr  38405  sucmapleftuniq  38512  lsatcvat  39159  lshpkrex  39227  cmtbr3N  39363  atn0  39417  atnle  39426  cvlsupr4  39454  cvlsupr5  39455  cvlsupr6  39456  cvrval4N  39523  cvratlem  39530  2llnjN  39676  2lplnj  39729  linepsubN  39861  elpaddatiN  39914  elpcliN  40002  pclcmpatN  40010  ldilval  40222  ltrnu  40230  cdleme18d  40404  tendotp  40870  tendof  40872  tendovalco  40874  diatrl  41153  diaintclN  41167  dvheveccl  41221  dibintclN  41276  dihord6apre  41365  dihmeetlem1N  41399  dihpN  41445  dihintcl  41453  dochkrshp4  41498  oexpreposd  42425  pw2f1ocnv  43140  iocinico  43315  onsucf1olem  43373  succlg  43431  oacl2g  43433  omabs2  43435  omcl2  43436  naddcnfcom  43469  naddcnfass  43472  safesnsupfidom1o  43520  infordmin  43635  pr2cv  43651  expgrowthi  44436  iotavalsb  44536  bi23imp1  44598  ioogtlb  45605  iocgtlb  45612  iocleub  45613  icoltub  45618  iooltub  45620  stoweidlem31  46139  oppr  47140  funressnfv  47153  fsetsniunop  47159  fsetsnf1  47162  eu2ndop1stv  47235  afvelrnb0  47274  otiunsndisjX  47389  el1fzopredsuc  47435  2ffzoeq  47437  uniimaprimaeqfv  47492  elsetpreimafveqfv  47502  iccpartimp  47527  iccpartrn  47540  iccpartf  47541  iccpartnel  47548  fargshiftf  47550  fargshiftfo  47552  ichnfimlem  47573  ichnfim  47574  ichreuopeq  47583  sprel  47594  sprsymrelfvlem  47600  sprsymrelfolem2  47603  prproropf1olem4  47616  prprelb  47626  poprelb  47634  fmtnofac1  47680  prmdvdsfmtnof1lem2  47695  31prm  47707  lighneallem3  47717  nn0o1gt2ALTV  47804  nn0oALTV  47806  odd2prm2  47828  mogoldbblem  47830  fpprbasnn  47839  fpprnn  47840  sbgoldbaltlem1  47889  nnsum3primesle9  47904  bgoldbtbndlem1  47915  bgoldbtbndlem2  47916  grimedgi  48046  grtriproplem  48049  grtriprop  48051  cycl3grtrilem  48056  cycl3grtri  48057  isubgr3stgrlem8  48083  gpgvtxel2  48158  gpgedgiov  48175  gpgedg2iv  48177  gpgprismgr4cycllem7  48211  pgnbgreunbgrlem1  48223  pgnbgreunbgrlem2lem1  48224  pgnbgreunbgrlem2lem2  48225  pgnbgreunbgrlem2lem3  48226  pgnbgreunbgrlem2  48227  pgnbgreunbgrlem4  48229  pgnbgreunbgrlem5  48233  upwlkbprop  48248  clcllaw  48301  intop  48313  assintop  48319  assintopcllaw  48322  elrngchomALTV  48379  rngccatidALTV  48382  rngcinvALTV  48386  rngcisoALTV  48387  rhmsubcALTVlem3  48393  rhmsubcALTVlem4  48394  funcringcsetcALTV2lem7  48406  elringchomALTV  48413  ringccatidALTV  48416  ringcisoALTV  48421  funcringcsetclem7ALTV  48429  ztprmneprm  48457  suppmptcfin  48486  linccl  48525  linc1  48536  lincolss  48545  ldepspr  48584  nn0sumshdiglem1  48732  0aryfvalelfv  48746  rrxlines  48844  rrxsphere  48859  itsclc0yqsol  48875  itschlc0xyqsol1  48877  fdomne0  48960  f002  48964  fvconstr2  48974  fullthinc  49561