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  1966  sb4a  2479  hbsb2  2481  dfsb2  2492  2eu2  2647  reu6  3700  2reu2  3864  sseq0  4369  disjel  4423  disjpss  4427  preq12b  4817  prneimg  4821  preqsnd  4826  elinti  4922  zfrepclf  5249  dtruALT2  5328  dtruOLD  5404  opth1g  5441  sbcop1  5451  snopeqop  5469  propeqop  5470  otsndisj  5482  otiunsndisj  5483  iunopeqop  5484  po2ne  5565  soasym  5582  elreldm  5902  dfres3  5958  relcnvtrg  6242  relresfld  6252  elpredimg  6292  ordtr2  6380  ordssun  6439  funopg  6553  funimass2  6602  f1imadifssran  6605  f0dom0  6747  elfv2ex  6907  fveqdmss  7053  eldmrexrnb  7067  fvcofneq  7068  funopsn  7123  funopdmsn  7125  funsndifnop  7126  elunirn  7228  oprabidw  7421  oprabid  7422  brfvopab  7449  limuni3  7831  peano5  7872  resf1ext2b  7914  op1steq  8015  el2mpocsbcl  8067  bropopvvv  8072  bropfvvvv  8074  f1o2ndf1  8104  frxp  8108  fnwelem  8113  poxp2  8125  suppimacnv  8156  fvn0elsuppb  8163  suppfnss  8171  reldmtpos  8216  rntpos  8221  seqomlem2  8422  oaordi  8513  oa00  8526  oalimcl  8527  omeulem1  8549  nnaordi  8585  ecopovtrn  8796  undifixp  8910  mapdom2  9118  unxpdomlem3  9206  en1eqsn  9226  enp1iOLD  9232  infssuni  9304  wdompwdom  9538  preleqg  9575  opthreg  9578  inf3lemd  9587  inf3lem2  9589  inf3lem6  9593  cnfcomlem  9659  cnfcom3  9664  karden  9855  carden2a  9926  alephdom  10041  dfac5lem4  10086  dfac5lem4OLD  10088  dfac12r  10107  kmlem2  10112  kmlem12  10122  cfslb2n  10228  alephsing  10236  fin23lem30  10302  fin1a2lem6  10365  fin1a2lem13  10372  axcc2lem  10396  domtriomlem  10402  axdc3lem2  10411  axdc4lem  10415  brdom6disj  10492  alephexp1  10539  pwfseq  10624  addnidpi  10861  indpi  10867  nqereu  10889  ltsonq  10929  distrlem5pr  10987  addcanpr  11006  suplem1pr  11012  suplem2pr  11013  ltsrpr  11037  ltsosr  11054  sqgt0sr  11066  leltne  11270  ltnsym  11279  ltlen  11282  eqlei  11291  eqlei2  11292  infm3  12149  nnunb  12445  0mnnnnn0  12481  elnnnn0b  12493  nn0ge2m1nn  12519  nn0le2is012  12605  btwnz  12644  uz11  12825  xrleltne  13112  xltnegi  13183  xnn0lenn0nn0  13212  xnn0xadd0  13214  xmulasslem2  13249  reltxrnmnf  13310  icogelb  13364  iccleub  13369  uznfz  13578  2ffzeq  13617  elfzonlteqm1  13709  elfzo0l  13724  fzoopth  13730  elfznelfzob  13741  elfzr  13748  elfzlmr  13749  injresinjlem  13755  injresinj  13756  fleqceilz  13823  modadd1  13877  modmul1  13896  modirr  13914  addmodlteq  13918  uzrdgfni  13930  fsuppmapnn0fiub0  13965  fsuppmapnn0ub  13967  seqf1o  14015  expnngt1  14213  hashrabsn01  14345  hashrabsn1  14346  hash1snb  14391  hash1n0  14393  hashf1lem2  14428  hash2prde  14442  hash2prd  14447  hash2pwpr  14448  hashle2pr  14449  hashle2prv  14450  hashge2el2dif  14452  hashge2el2difr  14453  hash3tpde  14465  fundmge2nop0  14474  ffz0iswrd  14513  ccatrcl1  14566  pfxsuff1eqwrdeq  14671  wrdind  14694  wrd2ind  14695  swrdccatin1  14697  swrdccat3blem  14711  2cshwcshw  14798  cshwcsh2id  14801  cshimadifsn  14802  2swrd2eqwrdeq  14926  wwlktovf  14929  wwlktovfo  14931  s3sndisj  14940  s3iunsndisj  14941  relexpindlem  15036  rexico  15327  lo1le  15625  fsum2dlem  15743  ntrivcvg  15870  fprodss  15921  fprod2dlem  15953  0dvds  16253  mod2eq1n2dvds  16324  opoe  16340  omoe  16341  opeo  16342  omeo  16343  m1exp1  16353  nn0enne  16354  nn0o1gt2  16358  gcdneg  16499  dfgcd2  16523  algcvga  16556  eucalglt  16562  lcmf  16610  coprmdvds  16630  divgcdcoprmex  16643  cncongr1  16644  prm2orodd  16668  prm23lt5  16792  pockthi  16885  prmreclem5  16898  ramtcl2  16989  cshwrepswhash1  17080  f1ocpbl  17495  f1ovscpbl  17496  f1olecpbl  17497  monhom  17704  epihom  17711  inveq  17743  invcoisoid  17761  isocoinvid  17762  ciclcl  17771  cicrcl  17772  isinitoi  17968  istermoi  17969  2initoinv  17979  2termoinv  17986  setciso  18060  embedsetcestrclem  18125  ipopos  18502  mgmpropd  18585  gsumval2a  18619  ismnddef  18670  dfgrp2e  18902  symg2bas  19330  snsymgefmndeq  19332  symgvalstruct  19334  symgfix2  19353  gsmsymgreq  19369  pmtrdifellem4  19416  mndodcongi  19480  pj1eu  19633  cycsubmcmn  19826  dprd2da  19981  rngimf1o  20370  rngimrnghm  20371  c0snmgmhm  20378  0ring01eq  20445  elrngchom  20540  rnghmsubcsetclem1  20547  rnghmsubcsetclem2  20548  rngcid  20551  rngcinv  20553  rngciso  20554  funcrngcsetcALT  20557  zrinitorngc  20558  zrtermorngc  20559  elringchom  20569  rhmsubcsetclem1  20576  rhmsubcsetclem2  20577  ringcid  20580  rhmsubcrngclem1  20582  rhmsubcrngclem2  20583  ringciso  20588  zrtermoringc  20591  rhmsubclem3  20603  rhmsubclem4  20604  lmodfopnelem1  20811  lspdisjb  21043  lspsnsubn0  21057  rngqiprngfulem2  21229  irinitoringc  21396  obs2ss  21645  mamufacex  22290  mat0dim0  22361  mat0dimid  22362  mat0dimscm  22363  dmatmat  22388  scmatmat  22403  mat1scmat  22433  1mavmul  22442  mavmulsolcl  22445  gsummatr01  22553  cpmatpmat  22604  cpmadugsumlemF  22770  tg2  22859  tgcl  22863  neii1  23000  neii2  23002  neindisj2  23017  perfopn  23079  ordtbas2  23085  pnfnei  23114  mnfnei  23115  llyidm  23382  txlm  23542  qtopuni  23596  tgqtop  23606  isfild  23752  snfil  23758  fbunfip  23763  fgss2  23768  fmco  23855  fbflim2  23871  cnpflf2  23894  fcfelbas  23930  fcfneii  23931  alexsubALTlem2  23942  alexsubALT  23945  tgpconncompeqg  24006  tsmscl  24029  tngngpim  24554  tgioo  24691  xrsmopn  24708  iccntr  24717  reconnlem2  24723  addcnlem  24760  htpycn  24879  phtpyhtpy  24888  pi1blem  24946  fgcfil  25178  ioombl1lem4  25469  dyadmbl  25508  itg2gt0  25668  ditgneg  25765  dvivthlem1  25920  coeeq2  26154  aannenlem2  26244  sineq0  26440  efif1o  26462  xrlimcnp  26885  vmacl  27035  efvmacl  27037  vmalelog  27123  dchrelbasd  27157  lgsqr  27269  lgsqrmodndvds  27271  gausslemma2dlem0i  27282  2lgslem2  27313  2lgs  27325  2lgsoddprmlem3  27332  2sqnn  27357  2sqreultlem  27365  2sqreultblem  27366  2sqreunnltlem  27368  2sqreunnltblem  27369  sltintdifex  27580  sltres  27581  nosepnelem  27598  nolt02o  27614  sltlend  27690  negsprop  27948  mulsprop  28040  onnolt  28174  onslt  28175  n0subs  28260  elntg2  28919  uhgr0vb  29006  umgrupgr  29037  umgrnloopv  29040  umgredgprv  29041  umgrislfupgrlem  29056  umgredg  29072  uspgrushgr  29111  uspgrupgr  29112  usgruspgr  29114  usgredgprvALT  29129  usgrnloopvALT  29135  uhgr2edg  29142  edg0usgr  29187  egrsubgr  29211  0uhgrsubgr  29213  uhgrspansubgrlem  29224  nbuhgr  29277  cusgrsize2inds  29388  cusgrfilem2  29391  vtxdg0v  29408  1loopgrnb0  29437  vtxdginducedm1lem4  29477  wlkvtxeledg  29559  wlkeq  29569  wlkl1loop  29573  wlk1walk  29574  upgrwlkedg  29577  uspgr2wlkeq  29581  wlkv0  29586  wlkonl1iedg  29600  wlkon2n0  29601  wlkp1lem8  29615  wlkp1  29616  lfgrwlkprop  29622  lfgrwlknloop  29624  2pthnloop  29668  upgrwlkdvde  29674  spthonepeq  29689  uhgrwkspthlem2  29691  usgr2wlkneq  29693  usgr2trlncl  29697  usgr2trlspth  29698  pthdlem2lem  29704  clwlkcompbp  29719  uspgrn2crct  29745  wwlks  29772  wwlknbp  29779  0enwwlksnge1  29801  wwlkswwlksn  29802  wlklnwwlkln1  29805  wwlksnextproplem3  29848  wwlksnextprop  29849  wspthsnonn0vne  29854  wspn0  29861  2pthon3v  29880  umgr2adedgspth  29885  rusgr0edg  29910  clwwlkccat  29926  clwlkclwwlklem2fv2  29932  clwlkclwwlklem2a4  29933  clwlkclwwlklem2  29936  clwlkclwwlkflem  29940  clwwlknp  29973  clwwlkwwlksb  29990  clwwlkext2edg  29992  erclwwlkneqlen  30004  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  clwwlknonwwlknonb  30042  upgr1wlkdlem1  30081  upgr3v3e3cycl  30116  uhgr3cyclexlem  30117  1conngr  30130  conngrv2edg  30131  eupth2lem3lem4  30167  eulercrct  30178  isfrgr  30196  frgr3vlem2  30210  1to2vfriswmgr  30215  1to3vfriswmgr  30216  frgrncvvdeqlem9  30243  frgrwopreg  30259  frgr2wwlkeqm  30267  2wspmdisj  30273  numclwwlk1lem2f  30291  frgrreggt1  30329  frgrregord013  30331  frgrregord13  30332  l2p  30415  nmlno0lem  30729  normgt0  31063  ocin  31232  nmlnop0iALT  31931  nmopun  31950  cvpss  32221  cvnbtwn  32222  atcvati  32322  mdsymlem6  32344  iunrnmptss  32501  expgt0b  32748  wrdt2ind  32882  irngssv  33690  issgon  34120  mbfmcnt  34266  ballotlemfc0  34491  ballotlemfcc  34492  satfv0  35352  satfv0fun  35365  fmla1  35381  gonarlem  35388  gonar  35389  goalrlem  35390  goalr  35391  fmla0disjsuc  35392  satffunlem  35395  satffunlem1lem1  35396  satffunlem2lem1  35398  satfun  35405  satfv0fvfmla0  35407  sategoelfv  35414  mthmblem  35574  pprodss4v  35879  funpartfun  35938  funpartfv  35940  5segofs  36001  btwnxfr  36051  brofs2  36072  brifs2  36073  btwnconn1  36096  segleantisym  36110  broutsideof2  36117  outsidene1  36118  outsidene2  36119  funray  36135  lineunray  36142  cldbnd  36321  bj-imdirval3  37179  topdifinffinlem  37342  isbasisrelowllem1  37350  isbasisrelowllem2  37351  relowlpssretop  37359  inunissunidif  37370  pibt2  37412  matunitlindf  37619  poimir  37654  volsupnfl  37666  itg2addnclem  37672  cover2  37716  sdclem2  37743  fdc  37746  sstotbnd3  37777  heibor1  37811  clmgmOLD  37852  smgrpmgm  37865  smgrpassOLD  37866  dvrunz  37955  0rngo  38028  mopickr  38352  lsatcvat  39050  lshpkrex  39118  cmtbr3N  39254  atn0  39308  atnle  39317  cvlsupr4  39345  cvlsupr5  39346  cvlsupr6  39347  cvrval4N  39415  cvratlem  39422  2llnjN  39568  2lplnj  39621  linepsubN  39753  elpaddatiN  39806  elpcliN  39894  pclcmpatN  39902  ldilval  40114  ltrnu  40122  cdleme18d  40296  tendotp  40762  tendof  40764  tendovalco  40766  diatrl  41045  diaintclN  41059  dvheveccl  41113  dibintclN  41168  dihord6apre  41257  dihmeetlem1N  41291  dihpN  41337  dihintcl  41345  dochkrshp4  41390  oexpreposd  42317  pw2f1ocnv  43033  iocinico  43208  onsucf1olem  43266  succlg  43324  oacl2g  43326  omabs2  43328  omcl2  43329  naddcnfcom  43362  naddcnfass  43365  safesnsupfidom1o  43413  infordmin  43528  pr2cv  43544  expgrowthi  44329  iotavalsb  44429  bi23imp1  44492  ioogtlb  45500  iocgtlb  45507  iocleub  45508  icoltub  45513  iooltub  45515  stoweidlem31  46036  oppr  47035  funressnfv  47048  fsetsniunop  47054  fsetsnf1  47057  eu2ndop1stv  47130  afvelrnb0  47169  otiunsndisjX  47284  el1fzopredsuc  47330  2ffzoeq  47332  uniimaprimaeqfv  47387  elsetpreimafveqfv  47397  iccpartimp  47422  iccpartrn  47435  iccpartf  47436  iccpartnel  47443  fargshiftf  47445  fargshiftfo  47447  ichnfimlem  47468  ichnfim  47469  ichreuopeq  47478  sprel  47489  sprsymrelfvlem  47495  sprsymrelfolem2  47498  prproropf1olem4  47511  prprelb  47521  poprelb  47529  fmtnofac1  47575  prmdvdsfmtnof1lem2  47590  31prm  47602  lighneallem3  47612  nn0o1gt2ALTV  47699  nn0oALTV  47701  odd2prm2  47723  mogoldbblem  47725  fpprbasnn  47734  fpprnn  47735  sbgoldbaltlem1  47784  nnsum3primesle9  47799  bgoldbtbndlem1  47810  bgoldbtbndlem2  47811  grtriproplem  47942  grtriprop  47944  cycl3grtrilem  47949  cycl3grtri  47950  isubgr3stgrlem8  47976  gpgvtxel2  48043  gpgedgiov  48060  gpgedg2iv  48062  gpgprismgr4cycllem7  48095  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5  48117  upwlkbprop  48130  clcllaw  48183  intop  48195  assintop  48201  assintopcllaw  48204  elrngchomALTV  48261  rngccatidALTV  48264  rngcinvALTV  48268  rngcisoALTV  48269  rhmsubcALTVlem3  48275  rhmsubcALTVlem4  48276  funcringcsetcALTV2lem7  48288  elringchomALTV  48295  ringccatidALTV  48298  ringcisoALTV  48303  funcringcsetclem7ALTV  48311  ztprmneprm  48339  suppmptcfin  48368  linccl  48407  linc1  48418  lincolss  48427  ldepspr  48466  nn0sumshdiglem1  48614  0aryfvalelfv  48628  rrxlines  48726  rrxsphere  48741  itsclc0yqsol  48757  itschlc0xyqsol1  48759  fdomne0  48842  f002  48846  fvconstr2  48856  fullthinc  49443