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  2485  hbsb2  2487  dfsb2  2498  2eu2  2653  reu6  3732  2reu2  3898  sseq0  4403  disjel  4457  disjpss  4461  preq12b  4850  prneimg  4854  preqsnd  4859  elinti  4955  zfrepclf  5291  dtruALT2  5370  dtruOLD  5446  opth1g  5483  sbcop1  5493  snopeqop  5511  propeqop  5512  otsndisj  5524  otiunsndisj  5525  iunopeqop  5526  po2ne  5608  soasym  5625  elreldm  5946  dfres3  6002  relcnvtrg  6286  relresfld  6296  elpredimg  6336  ordtr2  6428  ordssun  6486  funopg  6600  funimass2  6649  f1imadifssran  6652  f0dom0  6792  elfv2ex  6952  fveqdmss  7098  eldmrexrnb  7112  fvcofneq  7113  funopsn  7168  funopdmsn  7170  funsndifnop  7171  elunirn  7271  2f1fvneq  7280  oprabidw  7462  oprabid  7463  brfvopab  7490  limuni3  7873  peano5  7915  resf1ext2b  7957  op1steq  8058  el2mpocsbcl  8110  bropopvvv  8115  bropfvvvv  8117  f1o2ndf1  8147  frxp  8151  fnwelem  8156  poxp2  8168  suppimacnv  8199  fvn0elsuppb  8206  suppfnss  8214  reldmtpos  8259  rntpos  8264  seqomlem2  8491  oaordi  8584  oa00  8597  oalimcl  8598  omeulem1  8620  nnaordi  8656  ecopovtrn  8860  undifixp  8974  mapdom2  9188  unxpdomlem3  9288  en1eqsn  9308  enp1iOLD  9314  infssuni  9386  wdompwdom  9618  preleqg  9655  opthreg  9658  inf3lemd  9667  inf3lem2  9669  inf3lem6  9673  cnfcomlem  9739  cnfcom3  9744  karden  9935  carden2a  10006  alephdom  10121  dfac5lem4  10166  dfac5lem4OLD  10168  dfac12r  10187  kmlem2  10192  kmlem12  10202  cfslb2n  10308  alephsing  10316  fin23lem30  10382  fin1a2lem6  10445  fin1a2lem13  10452  axcc2lem  10476  domtriomlem  10482  axdc3lem2  10491  axdc4lem  10495  brdom6disj  10572  alephexp1  10619  pwfseq  10704  addnidpi  10941  indpi  10947  nqereu  10969  ltsonq  11009  distrlem5pr  11067  addcanpr  11086  suplem1pr  11092  suplem2pr  11093  ltsrpr  11117  ltsosr  11134  sqgt0sr  11146  leltne  11350  ltnsym  11359  ltlen  11362  eqlei  11371  eqlei2  11372  infm3  12227  nnunb  12522  0mnnnnn0  12558  elnnnn0b  12570  nn0ge2m1nn  12596  nn0le2is012  12682  btwnz  12721  uz11  12903  xrleltne  13187  xltnegi  13258  xnn0lenn0nn0  13287  xnn0xadd0  13289  xmulasslem2  13324  reltxrnmnf  13384  icogelb  13438  iccleub  13442  uznfz  13650  2ffzeq  13689  elfzonlteqm1  13780  elfzo0l  13795  fzoopth  13801  elfznelfzob  13812  elfzr  13819  elfzlmr  13820  injresinjlem  13826  injresinj  13827  fleqceilz  13894  modadd1  13948  modmul1  13965  modirr  13983  addmodlteq  13987  uzrdgfni  13999  fsuppmapnn0fiub0  14034  fsuppmapnn0ub  14036  seqf1o  14084  expnngt1  14280  hashrabsn01  14412  hashrabsn1  14413  hash1snb  14458  hash1n0  14460  hashf1lem2  14495  hash2prde  14509  hash2prd  14514  hash2pwpr  14515  hashle2pr  14516  hashle2prv  14517  hashge2el2dif  14519  hashge2el2difr  14520  hash3tpde  14532  fundmge2nop0  14541  ffz0iswrd  14579  ccatrcl1  14632  pfxsuff1eqwrdeq  14737  wrdind  14760  wrd2ind  14761  swrdccatin1  14763  swrdccat3blem  14777  2cshwcshw  14864  cshwcsh2id  14867  cshimadifsn  14868  2swrd2eqwrdeq  14992  wwlktovf  14995  wwlktovfo  14997  s3sndisj  15006  s3iunsndisj  15007  relexpindlem  15102  rexico  15392  lo1le  15688  fsum2dlem  15806  ntrivcvg  15933  fprodss  15984  fprod2dlem  16016  0dvds  16314  mod2eq1n2dvds  16384  opoe  16400  omoe  16401  opeo  16402  omeo  16403  m1exp1  16413  nn0enne  16414  nn0o1gt2  16418  gcdneg  16559  dfgcd2  16583  algcvga  16616  eucalglt  16622  lcmf  16670  coprmdvds  16690  divgcdcoprmex  16703  cncongr1  16704  prm2orodd  16728  prm23lt5  16852  pockthi  16945  prmreclem5  16958  ramtcl2  17049  cshwrepswhash1  17140  f1ocpbl  17570  f1ovscpbl  17571  f1olecpbl  17572  monhom  17779  epihom  17786  inveq  17818  invcoisoid  17836  isocoinvid  17837  ciclcl  17846  cicrcl  17847  isinitoi  18044  istermoi  18045  2initoinv  18055  2termoinv  18062  setciso  18136  embedsetcestrclem  18202  ipopos  18581  mgmpropd  18664  gsumval2a  18698  ismnddef  18749  dfgrp2e  18981  symg2bas  19410  snsymgefmndeq  19412  symgvalstruct  19414  symgvalstructOLD  19415  symgfix2  19434  gsmsymgreq  19450  pmtrdifellem4  19497  mndodcongi  19561  pj1eu  19714  cycsubmcmn  19907  dprd2da  20062  rngimf1o  20454  rngimrnghm  20455  c0snmgmhm  20462  0ring01eq  20529  elrngchom  20624  rnghmsubcsetclem1  20631  rnghmsubcsetclem2  20632  rngcid  20635  rngcinv  20637  rngciso  20638  funcrngcsetcALT  20641  zrinitorngc  20642  zrtermorngc  20643  elringchom  20653  rhmsubcsetclem1  20660  rhmsubcsetclem2  20661  ringcid  20664  rhmsubcrngclem1  20666  rhmsubcrngclem2  20667  ringciso  20672  zrtermoringc  20675  rhmsubclem3  20687  rhmsubclem4  20688  lmodfopnelem1  20896  lspdisjb  21128  lspsnsubn0  21142  rngqiprngfulem2  21322  irinitoringc  21490  obs2ss  21749  mamufacex  22400  mat0dim0  22473  mat0dimid  22474  mat0dimscm  22475  dmatmat  22500  scmatmat  22515  mat1scmat  22545  1mavmul  22554  mavmulsolcl  22557  gsummatr01  22665  cpmatpmat  22716  cpmadugsumlemF  22882  tg2  22972  tgcl  22976  neii1  23114  neii2  23116  neindisj2  23131  perfopn  23193  ordtbas2  23199  pnfnei  23228  mnfnei  23229  llyidm  23496  txlm  23656  qtopuni  23710  tgqtop  23720  isfild  23866  snfil  23872  fbunfip  23877  fgss2  23882  fmco  23969  fbflim2  23985  cnpflf2  24008  fcfelbas  24044  fcfneii  24045  alexsubALTlem2  24056  alexsubALT  24059  tgpconncompeqg  24120  tsmscl  24143  tngngpim  24680  tgioo  24817  xrsmopn  24834  iccntr  24843  reconnlem2  24849  addcnlem  24886  htpycn  25005  phtpyhtpy  25014  pi1blem  25072  fgcfil  25305  ioombl1lem4  25596  dyadmbl  25635  itg2gt0  25795  ditgneg  25892  dvivthlem1  26047  coeeq2  26281  aannenlem2  26371  sineq0  26566  efif1o  26588  xrlimcnp  27011  vmacl  27161  efvmacl  27163  vmalelog  27249  dchrelbasd  27283  lgsqr  27395  lgsqrmodndvds  27397  gausslemma2dlem0i  27408  2lgslem2  27439  2lgs  27451  2lgsoddprmlem3  27458  2sqnn  27483  2sqreultlem  27491  2sqreultblem  27492  2sqreunnltlem  27494  2sqreunnltblem  27495  sltintdifex  27706  sltres  27707  nosepnelem  27724  nolt02o  27740  sltlend  27816  negsprop  28067  mulsprop  28156  n0subs  28360  elntg2  29000  uhgr0vb  29089  umgrupgr  29120  umgrnloopv  29123  umgredgprv  29124  umgrislfupgrlem  29139  umgredg  29155  uspgrushgr  29194  uspgrupgr  29195  usgruspgr  29197  usgredgprvALT  29212  usgrnloopvALT  29218  uhgr2edg  29225  edg0usgr  29270  egrsubgr  29294  0uhgrsubgr  29296  uhgrspansubgrlem  29307  nbuhgr  29360  cusgrsize2inds  29471  cusgrfilem2  29474  vtxdg0v  29491  1loopgrnb0  29520  vtxdginducedm1lem4  29560  wlkvtxeledg  29642  wlkeq  29652  wlkl1loop  29656  wlk1walk  29657  upgrwlkedg  29660  uspgr2wlkeq  29664  wlkv0  29669  wlkonl1iedg  29683  wlkon2n0  29684  wlkp1lem8  29698  wlkp1  29699  lfgrwlkprop  29705  lfgrwlknloop  29707  2pthnloop  29751  upgrwlkdvde  29757  spthonepeq  29772  uhgrwkspthlem2  29774  usgr2wlkneq  29776  usgr2trlncl  29780  usgr2trlspth  29781  pthdlem2lem  29787  clwlkcompbp  29802  uspgrn2crct  29828  wwlks  29855  wwlknbp  29862  0enwwlksnge1  29884  wwlkswwlksn  29885  wlklnwwlkln1  29888  wwlksnextproplem3  29931  wwlksnextprop  29932  wspthsnonn0vne  29937  wspn0  29944  2pthon3v  29963  umgr2adedgspth  29968  rusgr0edg  29993  clwwlkccat  30009  clwlkclwwlklem2fv2  30015  clwlkclwwlklem2a4  30016  clwlkclwwlklem2  30019  clwlkclwwlkflem  30023  clwwlknp  30056  clwwlkwwlksb  30073  clwwlkext2edg  30075  erclwwlkneqlen  30087  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  clwwlknonwwlknonb  30125  upgr1wlkdlem1  30164  upgr3v3e3cycl  30199  uhgr3cyclexlem  30200  1conngr  30213  conngrv2edg  30214  eupth2lem3lem4  30250  eulercrct  30261  isfrgr  30279  frgr3vlem2  30293  1to2vfriswmgr  30298  1to3vfriswmgr  30299  frgrncvvdeqlem9  30326  frgrwopreg  30342  frgr2wwlkeqm  30350  2wspmdisj  30356  numclwwlk1lem2f  30374  frgrreggt1  30412  frgrregord013  30414  frgrregord13  30415  l2p  30498  nmlno0lem  30812  normgt0  31146  ocin  31315  nmlnop0iALT  32014  nmopun  32033  cvpss  32304  cvnbtwn  32305  atcvati  32405  mdsymlem6  32427  iunrnmptss  32578  expgt0b  32818  wrdt2ind  32938  irngssv  33738  issgon  34124  mbfmcnt  34270  ballotlemfc0  34495  ballotlemfcc  34496  satfv0  35363  satfv0fun  35376  fmla1  35392  gonarlem  35399  gonar  35400  goalrlem  35401  goalr  35402  fmla0disjsuc  35403  satffunlem  35406  satffunlem1lem1  35407  satffunlem2lem1  35409  satfun  35416  satfv0fvfmla0  35418  sategoelfv  35425  mthmblem  35585  pprodss4v  35885  funpartfun  35944  funpartfv  35946  5segofs  36007  btwnxfr  36057  brofs2  36078  brifs2  36079  btwnconn1  36102  segleantisym  36116  broutsideof2  36123  outsidene1  36124  outsidene2  36125  funray  36141  lineunray  36148  cldbnd  36327  bj-imdirval3  37185  topdifinffinlem  37348  isbasisrelowllem1  37356  isbasisrelowllem2  37357  relowlpssretop  37365  inunissunidif  37376  pibt2  37418  matunitlindf  37625  poimir  37660  volsupnfl  37672  itg2addnclem  37678  cover2  37722  sdclem2  37749  fdc  37752  sstotbnd3  37783  heibor1  37817  clmgmOLD  37858  smgrpmgm  37871  smgrpassOLD  37872  dvrunz  37961  0rngo  38034  mopickr  38364  lsatcvat  39051  lshpkrex  39119  cmtbr3N  39255  atn0  39309  atnle  39318  cvlsupr4  39346  cvlsupr5  39347  cvlsupr6  39348  cvrval4N  39416  cvratlem  39423  2llnjN  39569  2lplnj  39622  linepsubN  39754  elpaddatiN  39807  elpcliN  39895  pclcmpatN  39903  ldilval  40115  ltrnu  40123  cdleme18d  40297  tendotp  40763  tendof  40765  tendovalco  40767  diatrl  41046  diaintclN  41060  dvheveccl  41114  dibintclN  41169  dihord6apre  41258  dihmeetlem1N  41292  dihpN  41338  dihintcl  41346  dochkrshp4  41391  oexpreposd  42357  pw2f1ocnv  43049  iocinico  43224  onsucf1olem  43283  succlg  43341  oacl2g  43343  omabs2  43345  omcl2  43346  naddcnfcom  43379  naddcnfass  43382  safesnsupfidom1o  43430  infordmin  43545  pr2cv  43561  expgrowthi  44352  iotavalsb  44452  bi23imp1  44515  ioogtlb  45508  iocgtlb  45515  iocleub  45516  icoltub  45521  iooltub  45523  stoweidlem31  46046  oppr  47042  funressnfv  47055  fsetsniunop  47061  fsetsnf1  47064  eu2ndop1stv  47137  afvelrnb0  47176  otiunsndisjX  47291  el1fzopredsuc  47337  2ffzoeq  47339  uniimaprimaeqfv  47369  elsetpreimafveqfv  47379  iccpartimp  47404  iccpartrn  47417  iccpartf  47418  iccpartnel  47425  fargshiftf  47427  fargshiftfo  47429  ichnfimlem  47450  ichnfim  47451  ichreuopeq  47460  sprel  47471  sprsymrelfvlem  47477  sprsymrelfolem2  47480  prproropf1olem4  47493  prprelb  47503  poprelb  47511  fmtnofac1  47557  prmdvdsfmtnof1lem2  47572  31prm  47584  lighneallem3  47594  nn0o1gt2ALTV  47681  nn0oALTV  47683  odd2prm2  47705  mogoldbblem  47707  fpprbasnn  47716  fpprnn  47717  sbgoldbaltlem1  47766  nnsum3primesle9  47781  bgoldbtbndlem1  47792  bgoldbtbndlem2  47793  grtriproplem  47906  grtriprop  47908  cycl3grtrilem  47913  cycl3grtri  47914  isubgr3stgrlem8  47940  gpgvtxel2  48006  upwlkbprop  48054  clcllaw  48107  intop  48119  assintop  48125  assintopcllaw  48128  elrngchomALTV  48185  rngccatidALTV  48188  rngcinvALTV  48192  rngcisoALTV  48193  rhmsubcALTVlem3  48199  rhmsubcALTVlem4  48200  funcringcsetcALTV2lem7  48212  elringchomALTV  48219  ringccatidALTV  48222  ringcisoALTV  48227  funcringcsetclem7ALTV  48235  ztprmneprm  48263  suppmptcfin  48292  linccl  48331  linc1  48342  lincolss  48351  ldepspr  48390  nn0sumshdiglem1  48542  0aryfvalelfv  48556  rrxlines  48654  rrxsphere  48669  itsclc0yqsol  48685  itschlc0xyqsol1  48687  fdomne0  48759  f002  48763  fvconstr2  48767  fullthinc  49099