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  2478  hbsb2  2480  dfsb2  2491  2eu2  2646  reu6  3697  2reu2  3861  sseq0  4366  disjel  4420  disjpss  4424  preq12b  4814  prneimg  4818  preqsnd  4823  elinti  4919  zfrepclf  5246  dtruALT2  5325  dtruOLD  5401  opth1g  5438  sbcop1  5448  snopeqop  5466  propeqop  5467  otsndisj  5479  otiunsndisj  5480  iunopeqop  5481  po2ne  5562  soasym  5579  elreldm  5899  dfres3  5955  relcnvtrg  6239  relresfld  6249  elpredimg  6289  ordtr2  6377  ordssun  6436  funopg  6550  funimass2  6599  f1imadifssran  6602  f0dom0  6744  elfv2ex  6904  fveqdmss  7050  eldmrexrnb  7064  fvcofneq  7065  funopsn  7120  funopdmsn  7122  funsndifnop  7123  elunirn  7225  oprabidw  7418  oprabid  7419  brfvopab  7446  limuni3  7828  peano5  7869  resf1ext2b  7911  op1steq  8012  el2mpocsbcl  8064  bropopvvv  8069  bropfvvvv  8071  f1o2ndf1  8101  frxp  8105  fnwelem  8110  poxp2  8122  suppimacnv  8153  fvn0elsuppb  8160  suppfnss  8168  reldmtpos  8213  rntpos  8218  seqomlem2  8419  oaordi  8510  oa00  8523  oalimcl  8524  omeulem1  8546  nnaordi  8582  ecopovtrn  8793  undifixp  8907  mapdom2  9112  unxpdomlem3  9199  en1eqsn  9219  enp1iOLD  9225  infssuni  9297  wdompwdom  9531  preleqg  9568  opthreg  9571  inf3lemd  9580  inf3lem2  9582  inf3lem6  9586  cnfcomlem  9652  cnfcom3  9657  karden  9848  carden2a  9919  alephdom  10034  dfac5lem4  10079  dfac5lem4OLD  10081  dfac12r  10100  kmlem2  10105  kmlem12  10115  cfslb2n  10221  alephsing  10229  fin23lem30  10295  fin1a2lem6  10358  fin1a2lem13  10365  axcc2lem  10389  domtriomlem  10395  axdc3lem2  10404  axdc4lem  10408  brdom6disj  10485  alephexp1  10532  pwfseq  10617  addnidpi  10854  indpi  10860  nqereu  10882  ltsonq  10922  distrlem5pr  10980  addcanpr  10999  suplem1pr  11005  suplem2pr  11006  ltsrpr  11030  ltsosr  11047  sqgt0sr  11059  leltne  11263  ltnsym  11272  ltlen  11275  eqlei  11284  eqlei2  11285  infm3  12142  nnunb  12438  0mnnnnn0  12474  elnnnn0b  12486  nn0ge2m1nn  12512  nn0le2is012  12598  btwnz  12637  uz11  12818  xrleltne  13105  xltnegi  13176  xnn0lenn0nn0  13205  xnn0xadd0  13207  xmulasslem2  13242  reltxrnmnf  13303  icogelb  13357  iccleub  13362  uznfz  13571  2ffzeq  13610  elfzonlteqm1  13702  elfzo0l  13717  fzoopth  13723  elfznelfzob  13734  elfzr  13741  elfzlmr  13742  injresinjlem  13748  injresinj  13749  fleqceilz  13816  modadd1  13870  modmul1  13889  modirr  13907  addmodlteq  13911  uzrdgfni  13923  fsuppmapnn0fiub0  13958  fsuppmapnn0ub  13960  seqf1o  14008  expnngt1  14206  hashrabsn01  14338  hashrabsn1  14339  hash1snb  14384  hash1n0  14386  hashf1lem2  14421  hash2prde  14435  hash2prd  14440  hash2pwpr  14441  hashle2pr  14442  hashle2prv  14443  hashge2el2dif  14445  hashge2el2difr  14446  hash3tpde  14458  fundmge2nop0  14467  ffz0iswrd  14506  ccatrcl1  14559  pfxsuff1eqwrdeq  14664  wrdind  14687  wrd2ind  14688  swrdccatin1  14690  swrdccat3blem  14704  2cshwcshw  14791  cshwcsh2id  14794  cshimadifsn  14795  2swrd2eqwrdeq  14919  wwlktovf  14922  wwlktovfo  14924  s3sndisj  14933  s3iunsndisj  14934  relexpindlem  15029  rexico  15320  lo1le  15618  fsum2dlem  15736  ntrivcvg  15863  fprodss  15914  fprod2dlem  15946  0dvds  16246  mod2eq1n2dvds  16317  opoe  16333  omoe  16334  opeo  16335  omeo  16336  m1exp1  16346  nn0enne  16347  nn0o1gt2  16351  gcdneg  16492  dfgcd2  16516  algcvga  16549  eucalglt  16555  lcmf  16603  coprmdvds  16623  divgcdcoprmex  16636  cncongr1  16637  prm2orodd  16661  prm23lt5  16785  pockthi  16878  prmreclem5  16891  ramtcl2  16982  cshwrepswhash1  17073  f1ocpbl  17488  f1ovscpbl  17489  f1olecpbl  17490  monhom  17697  epihom  17704  inveq  17736  invcoisoid  17754  isocoinvid  17755  ciclcl  17764  cicrcl  17765  isinitoi  17961  istermoi  17962  2initoinv  17972  2termoinv  17979  setciso  18053  embedsetcestrclem  18118  ipopos  18495  mgmpropd  18578  gsumval2a  18612  ismnddef  18663  dfgrp2e  18895  symg2bas  19323  snsymgefmndeq  19325  symgvalstruct  19327  symgfix2  19346  gsmsymgreq  19362  pmtrdifellem4  19409  mndodcongi  19473  pj1eu  19626  cycsubmcmn  19819  dprd2da  19974  rngimf1o  20363  rngimrnghm  20364  c0snmgmhm  20371  0ring01eq  20438  elrngchom  20533  rnghmsubcsetclem1  20540  rnghmsubcsetclem2  20541  rngcid  20544  rngcinv  20546  rngciso  20547  funcrngcsetcALT  20550  zrinitorngc  20551  zrtermorngc  20552  elringchom  20562  rhmsubcsetclem1  20569  rhmsubcsetclem2  20570  ringcid  20573  rhmsubcrngclem1  20575  rhmsubcrngclem2  20576  ringciso  20581  zrtermoringc  20584  rhmsubclem3  20596  rhmsubclem4  20597  lmodfopnelem1  20804  lspdisjb  21036  lspsnsubn0  21050  rngqiprngfulem2  21222  irinitoringc  21389  obs2ss  21638  mamufacex  22283  mat0dim0  22354  mat0dimid  22355  mat0dimscm  22356  dmatmat  22381  scmatmat  22396  mat1scmat  22426  1mavmul  22435  mavmulsolcl  22438  gsummatr01  22546  cpmatpmat  22597  cpmadugsumlemF  22763  tg2  22852  tgcl  22856  neii1  22993  neii2  22995  neindisj2  23010  perfopn  23072  ordtbas2  23078  pnfnei  23107  mnfnei  23108  llyidm  23375  txlm  23535  qtopuni  23589  tgqtop  23599  isfild  23745  snfil  23751  fbunfip  23756  fgss2  23761  fmco  23848  fbflim2  23864  cnpflf2  23887  fcfelbas  23923  fcfneii  23924  alexsubALTlem2  23935  alexsubALT  23938  tgpconncompeqg  23999  tsmscl  24022  tngngpim  24547  tgioo  24684  xrsmopn  24701  iccntr  24710  reconnlem2  24716  addcnlem  24753  htpycn  24872  phtpyhtpy  24881  pi1blem  24939  fgcfil  25171  ioombl1lem4  25462  dyadmbl  25501  itg2gt0  25661  ditgneg  25758  dvivthlem1  25913  coeeq2  26147  aannenlem2  26237  sineq0  26433  efif1o  26455  xrlimcnp  26878  vmacl  27028  efvmacl  27030  vmalelog  27116  dchrelbasd  27150  lgsqr  27262  lgsqrmodndvds  27264  gausslemma2dlem0i  27275  2lgslem2  27306  2lgs  27318  2lgsoddprmlem3  27325  2sqnn  27350  2sqreultlem  27358  2sqreultblem  27359  2sqreunnltlem  27361  2sqreunnltblem  27362  sltintdifex  27573  sltres  27574  nosepnelem  27591  nolt02o  27607  sltlend  27683  negsprop  27941  mulsprop  28033  onnolt  28167  onslt  28168  n0subs  28253  elntg2  28912  uhgr0vb  28999  umgrupgr  29030  umgrnloopv  29033  umgredgprv  29034  umgrislfupgrlem  29049  umgredg  29065  uspgrushgr  29104  uspgrupgr  29105  usgruspgr  29107  usgredgprvALT  29122  usgrnloopvALT  29128  uhgr2edg  29135  edg0usgr  29180  egrsubgr  29204  0uhgrsubgr  29206  uhgrspansubgrlem  29217  nbuhgr  29270  cusgrsize2inds  29381  cusgrfilem2  29384  vtxdg0v  29401  1loopgrnb0  29430  vtxdginducedm1lem4  29470  wlkvtxeledg  29552  wlkeq  29562  wlkl1loop  29566  wlk1walk  29567  upgrwlkedg  29570  uspgr2wlkeq  29574  wlkv0  29579  wlkonl1iedg  29593  wlkon2n0  29594  wlkp1lem8  29608  wlkp1  29609  lfgrwlkprop  29615  lfgrwlknloop  29617  2pthnloop  29661  upgrwlkdvde  29667  spthonepeq  29682  uhgrwkspthlem2  29684  usgr2wlkneq  29686  usgr2trlncl  29690  usgr2trlspth  29691  pthdlem2lem  29697  clwlkcompbp  29712  uspgrn2crct  29738  wwlks  29765  wwlknbp  29772  0enwwlksnge1  29794  wwlkswwlksn  29795  wlklnwwlkln1  29798  wwlksnextproplem3  29841  wwlksnextprop  29842  wspthsnonn0vne  29847  wspn0  29854  2pthon3v  29873  umgr2adedgspth  29878  rusgr0edg  29903  clwwlkccat  29919  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2a4  29926  clwlkclwwlklem2  29929  clwlkclwwlkflem  29933  clwwlknp  29966  clwwlkwwlksb  29983  clwwlkext2edg  29985  erclwwlkneqlen  29997  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  clwwlknonwwlknonb  30035  upgr1wlkdlem1  30074  upgr3v3e3cycl  30109  uhgr3cyclexlem  30110  1conngr  30123  conngrv2edg  30124  eupth2lem3lem4  30160  eulercrct  30171  isfrgr  30189  frgr3vlem2  30203  1to2vfriswmgr  30208  1to3vfriswmgr  30209  frgrncvvdeqlem9  30236  frgrwopreg  30252  frgr2wwlkeqm  30260  2wspmdisj  30266  numclwwlk1lem2f  30284  frgrreggt1  30322  frgrregord013  30324  frgrregord13  30325  l2p  30408  nmlno0lem  30722  normgt0  31056  ocin  31225  nmlnop0iALT  31924  nmopun  31943  cvpss  32214  cvnbtwn  32215  atcvati  32315  mdsymlem6  32337  iunrnmptss  32494  expgt0b  32741  wrdt2ind  32875  irngssv  33683  issgon  34113  mbfmcnt  34259  ballotlemfc0  34484  ballotlemfcc  34485  satfv0  35345  satfv0fun  35358  fmla1  35374  gonarlem  35381  gonar  35382  goalrlem  35383  goalr  35384  fmla0disjsuc  35385  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  satfun  35398  satfv0fvfmla0  35400  sategoelfv  35407  mthmblem  35567  pprodss4v  35872  funpartfun  35931  funpartfv  35933  5segofs  35994  btwnxfr  36044  brofs2  36065  brifs2  36066  btwnconn1  36089  segleantisym  36103  broutsideof2  36110  outsidene1  36111  outsidene2  36112  funray  36128  lineunray  36135  cldbnd  36314  bj-imdirval3  37172  topdifinffinlem  37335  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlpssretop  37352  inunissunidif  37363  pibt2  37405  matunitlindf  37612  poimir  37647  volsupnfl  37659  itg2addnclem  37665  cover2  37709  sdclem2  37736  fdc  37739  sstotbnd3  37770  heibor1  37804  clmgmOLD  37845  smgrpmgm  37858  smgrpassOLD  37859  dvrunz  37948  0rngo  38021  mopickr  38345  lsatcvat  39043  lshpkrex  39111  cmtbr3N  39247  atn0  39301  atnle  39310  cvlsupr4  39338  cvlsupr5  39339  cvlsupr6  39340  cvrval4N  39408  cvratlem  39415  2llnjN  39561  2lplnj  39614  linepsubN  39746  elpaddatiN  39799  elpcliN  39887  pclcmpatN  39895  ldilval  40107  ltrnu  40115  cdleme18d  40289  tendotp  40755  tendof  40757  tendovalco  40759  diatrl  41038  diaintclN  41052  dvheveccl  41106  dibintclN  41161  dihord6apre  41250  dihmeetlem1N  41284  dihpN  41330  dihintcl  41338  dochkrshp4  41383  oexpreposd  42310  pw2f1ocnv  43026  iocinico  43201  onsucf1olem  43259  succlg  43317  oacl2g  43319  omabs2  43321  omcl2  43322  naddcnfcom  43355  naddcnfass  43358  safesnsupfidom1o  43406  infordmin  43521  pr2cv  43537  expgrowthi  44322  iotavalsb  44422  bi23imp1  44485  ioogtlb  45493  iocgtlb  45500  iocleub  45501  icoltub  45506  iooltub  45508  stoweidlem31  46029  oppr  47031  funressnfv  47044  fsetsniunop  47050  fsetsnf1  47053  eu2ndop1stv  47126  afvelrnb0  47165  otiunsndisjX  47280  el1fzopredsuc  47326  2ffzoeq  47328  uniimaprimaeqfv  47383  elsetpreimafveqfv  47393  iccpartimp  47418  iccpartrn  47431  iccpartf  47432  iccpartnel  47439  fargshiftf  47441  fargshiftfo  47443  ichnfimlem  47464  ichnfim  47465  ichreuopeq  47474  sprel  47485  sprsymrelfvlem  47491  sprsymrelfolem2  47494  prproropf1olem4  47507  prprelb  47517  poprelb  47525  fmtnofac1  47571  prmdvdsfmtnof1lem2  47586  31prm  47598  lighneallem3  47608  nn0o1gt2ALTV  47695  nn0oALTV  47697  odd2prm2  47719  mogoldbblem  47721  fpprbasnn  47730  fpprnn  47731  sbgoldbaltlem1  47780  nnsum3primesle9  47795  bgoldbtbndlem1  47806  bgoldbtbndlem2  47807  grtriproplem  47938  grtriprop  47940  cycl3grtrilem  47945  cycl3grtri  47946  isubgr3stgrlem8  47972  gpgvtxel2  48039  gpgedgiov  48056  gpgedg2iv  48058  gpgprismgr4cycllem7  48091  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5  48113  upwlkbprop  48126  clcllaw  48179  intop  48191  assintop  48197  assintopcllaw  48200  elrngchomALTV  48257  rngccatidALTV  48260  rngcinvALTV  48264  rngcisoALTV  48265  rhmsubcALTVlem3  48271  rhmsubcALTVlem4  48272  funcringcsetcALTV2lem7  48284  elringchomALTV  48291  ringccatidALTV  48294  ringcisoALTV  48299  funcringcsetclem7ALTV  48307  ztprmneprm  48335  suppmptcfin  48364  linccl  48403  linc1  48414  lincolss  48423  ldepspr  48462  nn0sumshdiglem1  48610  0aryfvalelfv  48624  rrxlines  48722  rrxsphere  48737  itsclc0yqsol  48753  itschlc0xyqsol1  48755  fdomne0  48838  f002  48842  fvconstr2  48852  fullthinc  49439