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  5238  dtruALT2  5317  opth1g  5434  sbcop1  5444  snopeqop  5462  propeqop  5463  otsndisj  5475  otiunsndisj  5476  iunopeqop  5477  po2ne  5556  soasym  5573  elreldm  5892  dfres3  5951  relcnvtrg  6233  relresfld  6242  elpredimg  6282  ordtr2  6370  ordssun  6429  funopg  6534  funimass2  6583  f1imadifssran  6586  f0dom0  6726  elfv2ex  6885  fveqdmss  7032  eldmrexrnb  7046  fvcofneq  7047  funopsn  7103  funopdmsn  7105  funsndifnop  7106  elunirn  7207  oprabidw  7399  oprabid  7400  brfvopab  7425  limuni3  7804  peano5  7845  resf1ext2b  7887  op1steq  7987  el2mpocsbcl  8037  bropopvvv  8042  bropfvvvv  8044  f1o2ndf1  8074  frxp  8078  fnwelem  8083  poxp2  8095  suppimacnv  8126  fvn0elsuppb  8133  suppfnss  8141  reldmtpos  8186  rntpos  8191  seqomlem2  8392  oaordi  8483  oa00  8496  oalimcl  8497  omeulem1  8519  nnaordi  8556  ecopovtrn  8769  undifixp  8884  mapdom2  9088  unxpdomlem3  9170  en1eqsn  9187  infssuni  9258  wdompwdom  9495  preleqg  9536  opthreg  9539  inf3lemd  9548  inf3lem2  9550  inf3lem6  9554  cnfcomlem  9620  cnfcom3  9625  karden  9819  carden2a  9890  alephdom  10003  dfac5lem4  10048  dfac5lem4OLD  10050  dfac12r  10069  kmlem2  10074  kmlem12  10084  cfslb2n  10190  alephsing  10198  fin23lem30  10264  fin1a2lem6  10327  fin1a2lem13  10334  axcc2lem  10358  domtriomlem  10364  axdc3lem2  10373  axdc4lem  10377  brdom6disj  10454  alephexp1  10502  pwfseq  10587  addnidpi  10824  indpi  10830  nqereu  10852  ltsonq  10892  distrlem5pr  10950  addcanpr  10969  suplem1pr  10975  suplem2pr  10976  ltsrpr  11000  ltsosr  11017  sqgt0sr  11029  leltne  11234  ltnsym  11243  ltlen  11246  eqlei  11255  eqlei2  11256  infm3  12113  nnunb  12409  0mnnnnn0  12445  elnnnn0b  12457  nn0ge2m1nn  12483  nn0le2is012  12568  btwnz  12607  uz11  12788  xrleltne  13071  xltnegi  13143  xnn0lenn0nn0  13172  xnn0xadd0  13174  xmulasslem2  13209  reltxrnmnf  13270  icogelb  13324  iccleub  13329  uznfz  13538  2ffzeq  13577  elfzonlteqm1  13669  elfzo0l  13684  fzoopth  13690  elfznelfzob  13702  elfzr  13709  elfzlmr  13710  injresinjlem  13718  injresinj  13719  fleqceilz  13786  modadd1  13840  modmul1  13859  modirr  13877  addmodlteq  13881  uzrdgfni  13893  fsuppmapnn0fiub0  13928  fsuppmapnn0ub  13930  seqf1o  13978  expnngt1  14176  hashrabsn01  14308  hashrabsn1  14309  hash1snb  14354  hash1n0  14356  hashf1lem2  14391  hash2prde  14405  hash2prd  14410  hash2pwpr  14411  hashle2pr  14412  hashle2prv  14413  hashge2el2dif  14415  hashge2el2difr  14416  hash3tpde  14428  fundmge2nop0  14437  ffz0iswrd  14476  ccatrcl1  14530  pfxsuff1eqwrdeq  14634  wrdind  14657  wrd2ind  14658  swrdccatin1  14660  swrdccat3blem  14674  2cshwcshw  14760  cshwcsh2id  14763  cshimadifsn  14764  2swrd2eqwrdeq  14888  wwlktovf  14891  wwlktovfo  14893  s3sndisj  14902  s3iunsndisj  14903  relexpindlem  14998  rexico  15289  lo1le  15587  fsum2dlem  15705  ntrivcvg  15832  fprodss  15883  fprod2dlem  15915  0dvds  16215  mod2eq1n2dvds  16286  opoe  16302  omoe  16303  opeo  16304  omeo  16305  m1exp1  16315  nn0enne  16316  nn0o1gt2  16320  gcdneg  16461  dfgcd2  16485  algcvga  16518  eucalglt  16524  lcmf  16572  coprmdvds  16592  divgcdcoprmex  16605  cncongr1  16606  prm2orodd  16630  prm23lt5  16754  pockthi  16847  prmreclem5  16860  ramtcl2  16951  cshwrepswhash1  17042  f1ocpbl  17458  f1ovscpbl  17459  f1olecpbl  17460  monhom  17671  epihom  17678  inveq  17710  invcoisoid  17728  isocoinvid  17729  ciclcl  17738  cicrcl  17739  isinitoi  17935  istermoi  17936  2initoinv  17946  2termoinv  17953  setciso  18027  embedsetcestrclem  18092  ipopos  18471  mgmpropd  18588  gsumval2a  18622  ismnddef  18673  dfgrp2e  18908  symg2bas  19337  snsymgefmndeq  19339  symgvalstruct  19341  symgfix2  19360  gsmsymgreq  19376  pmtrdifellem4  19423  mndodcongi  19487  pj1eu  19640  cycsubmcmn  19833  dprd2da  19988  rngimf1o  20405  rngimrnghm  20406  c0snmgmhm  20413  0ring01eq  20477  elrngchom  20572  rnghmsubcsetclem1  20579  rnghmsubcsetclem2  20580  rngcid  20583  rngcinv  20585  rngciso  20586  funcrngcsetcALT  20589  zrinitorngc  20590  zrtermorngc  20591  elringchom  20601  rhmsubcsetclem1  20608  rhmsubcsetclem2  20609  ringcid  20612  rhmsubcrngclem1  20614  rhmsubcrngclem2  20615  ringciso  20620  zrtermoringc  20623  rhmsubclem3  20635  rhmsubclem4  20636  lmodfopnelem1  20864  lspdisjb  21096  lspsnsubn0  21110  rngqiprngfulem2  21282  irinitoringc  21449  obs2ss  21699  mamufacex  22355  mat0dim0  22426  mat0dimid  22427  mat0dimscm  22428  dmatmat  22453  scmatmat  22468  mat1scmat  22498  1mavmul  22507  mavmulsolcl  22510  gsummatr01  22618  cpmatpmat  22669  cpmadugsumlemF  22835  tg2  22924  tgcl  22928  neii1  23065  neii2  23067  neindisj2  23082  perfopn  23144  ordtbas2  23150  pnfnei  23179  mnfnei  23180  llyidm  23447  txlm  23607  qtopuni  23661  tgqtop  23671  isfild  23817  snfil  23823  fbunfip  23828  fgss2  23833  fmco  23920  fbflim2  23936  cnpflf2  23959  fcfelbas  23995  fcfneii  23996  alexsubALTlem2  24007  alexsubALT  24010  tgpconncompeqg  24071  tsmscl  24094  tngngpim  24618  tgioo  24755  xrsmopn  24772  iccntr  24781  reconnlem2  24787  addcnlem  24824  htpycn  24943  phtpyhtpy  24952  pi1blem  25010  fgcfil  25242  ioombl1lem4  25533  dyadmbl  25572  itg2gt0  25732  ditgneg  25829  dvivthlem1  25984  coeeq2  26218  aannenlem2  26308  sineq0  26504  efif1o  26526  xrlimcnp  26949  vmacl  27099  efvmacl  27101  vmalelog  27187  dchrelbasd  27221  lgsqr  27333  lgsqrmodndvds  27335  gausslemma2dlem0i  27346  2lgslem2  27377  2lgs  27389  2lgsoddprmlem3  27396  2sqnn  27421  2sqreultlem  27429  2sqreultblem  27430  2sqreunnltlem  27432  2sqreunnltblem  27433  ltsintdifex  27644  ltsres  27645  nosepnelem  27662  nolt02o  27678  ltlesnd  27758  negsprop  28046  mulsprop  28141  onnolt  28277  onlts  28278  n0subs  28374  bdaypw2n0bndlem  28474  bdaypw2n0bnd  28475  bdayfinbndlem2  28479  elntg2  29074  uhgr0vb  29161  umgrupgr  29192  umgrnloopv  29195  umgredgprv  29196  umgrislfupgrlem  29211  umgredg  29227  uspgrushgr  29266  uspgrupgr  29267  usgruspgr  29269  usgredgprvALT  29284  usgrnloopvALT  29290  uhgr2edg  29297  edg0usgr  29342  egrsubgr  29366  0uhgrsubgr  29368  uhgrspansubgrlem  29379  nbuhgr  29432  cusgrsize2inds  29543  cusgrfilem2  29546  vtxdg0v  29563  1loopgrnb0  29592  vtxdginducedm1lem4  29632  wlkvtxeledg  29713  wlkeq  29723  wlkl1loop  29727  wlk1walk  29728  upgrwlkedg  29731  uspgr2wlkeq  29735  wlkv0  29739  wlkonl1iedg  29753  wlkon2n0  29754  wlkp1lem8  29768  wlkp1  29769  lfgrwlkprop  29775  lfgrwlknloop  29777  2pthnloop  29820  upgrwlkdvde  29826  spthonepeq  29841  uhgrwkspthlem2  29843  usgr2wlkneq  29845  usgr2trlncl  29849  usgr2trlspth  29850  pthdlem2lem  29856  clwlkcompbp  29871  uspgrn2crct  29897  wwlks  29924  wwlknbp  29931  0enwwlksnge1  29953  wwlkswwlksn  29954  wlklnwwlkln1  29957  wwlksnextproplem3  30000  wwlksnextprop  30001  wspthsnonn0vne  30006  wspn0  30013  2pthon3v  30032  umgr2adedgspth  30037  rusgr0edg  30065  clwwlkccat  30081  clwlkclwwlklem2fv2  30087  clwlkclwwlklem2a4  30088  clwlkclwwlklem2  30091  clwlkclwwlkflem  30095  clwwlknp  30128  clwwlkwwlksb  30145  clwwlkext2edg  30147  erclwwlkneqlen  30159  hashecclwwlkn1  30168  umgrhashecclwwlk  30169  clwwlknonwwlknonb  30197  upgr1wlkdlem1  30236  upgr3v3e3cycl  30271  uhgr3cyclexlem  30272  1conngr  30285  conngrv2edg  30286  eupth2lem3lem4  30322  eulercrct  30333  isfrgr  30351  frgr3vlem2  30365  1to2vfriswmgr  30370  1to3vfriswmgr  30371  frgrncvvdeqlem9  30398  frgrwopreg  30414  frgr2wwlkeqm  30422  2wspmdisj  30428  numclwwlk1lem2f  30446  frgrreggt1  30484  frgrregord013  30486  frgrregord13  30487  l2p  30571  nmlno0lem  30885  normgt0  31219  ocin  31388  nmlnop0iALT  32087  nmopun  32106  cvpss  32377  cvnbtwn  32378  atcvati  32478  mdsymlem6  32500  iunrnmptss  32656  expgt0b  32912  wrdt2ind  33050  irngssv  33870  issgon  34305  mbfmcnt  34450  ballotlemfc0  34675  ballotlemfcc  34676  satfv0  35578  satfv0fun  35591  fmla1  35607  gonarlem  35614  gonar  35615  goalrlem  35616  goalr  35617  fmla0disjsuc  35618  satffunlem  35621  satffunlem1lem1  35622  satffunlem2lem1  35624  satfun  35631  satfv0fvfmla0  35633  sategoelfv  35640  mthmblem  35800  pprodss4v  36102  funpartfun  36163  funpartfv  36165  5segofs  36226  btwnxfr  36276  brofs2  36297  brifs2  36298  btwnconn1  36321  segleantisym  36335  broutsideof2  36342  outsidene1  36343  outsidene2  36344  funray  36360  lineunray  36367  cldbnd  36546  bj-imdirval3  37443  topdifinffinlem  37606  isbasisrelowllem1  37614  isbasisrelowllem2  37615  relowlpssretop  37623  inunissunidif  37634  pibt2  37676  matunitlindf  37873  poimir  37908  volsupnfl  37920  itg2addnclem  37926  cover2  37970  sdclem2  37997  fdc  38000  sstotbnd3  38031  heibor1  38065  clmgmOLD  38106  smgrpmgm  38119  smgrpassOLD  38120  dvrunz  38209  0rngo  38282  mopickr  38626  sucmapleftuniq  38745  lsatcvat  39430  lshpkrex  39498  cmtbr3N  39634  atn0  39688  atnle  39697  cvlsupr4  39725  cvlsupr5  39726  cvlsupr6  39727  cvrval4N  39794  cvratlem  39801  2llnjN  39947  2lplnj  40000  linepsubN  40132  elpaddatiN  40185  elpcliN  40273  pclcmpatN  40281  ldilval  40493  ltrnu  40501  cdleme18d  40675  tendotp  41141  tendof  41143  tendovalco  41145  diatrl  41424  diaintclN  41438  dvheveccl  41492  dibintclN  41547  dihord6apre  41636  dihmeetlem1N  41670  dihpN  41716  dihintcl  41724  dochkrshp4  41769  oexpreposd  42696  pw2f1ocnv  43398  iocinico  43573  onsucf1olem  43631  succlg  43689  oacl2g  43691  omabs2  43693  omcl2  43694  naddcnfcom  43727  naddcnfass  43730  safesnsupfidom1o  43777  infordmin  43892  pr2cv  43908  expgrowthi  44693  iotavalsb  44793  bi23imp1  44855  ioogtlb  45859  iocgtlb  45866  iocleub  45867  icoltub  45872  iooltub  45874  stoweidlem31  46393  oppr  47394  funressnfv  47407  fsetsniunop  47413  fsetsnf1  47416  eu2ndop1stv  47489  afvelrnb0  47528  otiunsndisjX  47643  el1fzopredsuc  47689  2ffzoeq  47691  uniimaprimaeqfv  47746  elsetpreimafveqfv  47756  iccpartimp  47781  iccpartrn  47794  iccpartf  47795  iccpartnel  47802  fargshiftf  47804  fargshiftfo  47806  ichnfimlem  47827  ichnfim  47828  ichreuopeq  47837  sprel  47848  sprsymrelfvlem  47854  sprsymrelfolem2  47857  prproropf1olem4  47870  prprelb  47880  poprelb  47888  fmtnofac1  47934  prmdvdsfmtnof1lem2  47949  31prm  47961  lighneallem3  47971  nn0o1gt2ALTV  48058  nn0oALTV  48060  odd2prm2  48082  mogoldbblem  48084  fpprbasnn  48093  fpprnn  48094  sbgoldbaltlem1  48143  nnsum3primesle9  48158  bgoldbtbndlem1  48169  bgoldbtbndlem2  48170  grimedgi  48300  grtriproplem  48303  grtriprop  48305  cycl3grtrilem  48310  cycl3grtri  48311  isubgr3stgrlem8  48337  gpgvtxel2  48412  gpgedgiov  48429  gpgedg2iv  48431  gpgprismgr4cycllem7  48465  pgnbgreunbgrlem1  48477  pgnbgreunbgrlem2lem1  48478  pgnbgreunbgrlem2lem2  48479  pgnbgreunbgrlem2lem3  48480  pgnbgreunbgrlem2  48481  pgnbgreunbgrlem4  48483  pgnbgreunbgrlem5  48487  upwlkbprop  48502  clcllaw  48555  intop  48567  assintop  48573  assintopcllaw  48576  elrngchomALTV  48633  rngccatidALTV  48636  rngcinvALTV  48640  rngcisoALTV  48641  rhmsubcALTVlem3  48647  rhmsubcALTVlem4  48648  funcringcsetcALTV2lem7  48660  elringchomALTV  48667  ringccatidALTV  48670  ringcisoALTV  48675  funcringcsetclem7ALTV  48683  ztprmneprm  48711  suppmptcfin  48740  linccl  48778  linc1  48789  lincolss  48798  ldepspr  48837  nn0sumshdiglem1  48985  0aryfvalelfv  48999  rrxlines  49097  rrxsphere  49112  itsclc0yqsol  49128  itschlc0xyqsol1  49130  fdomne0  49213  f002  49217  fvconstr2  49227  fullthinc  49813