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  1965  sb4a  2483  hbsb2  2485  dfsb2  2496  2eu2  2651  reu6  3707  2reu2  3871  sseq0  4376  disjel  4430  disjpss  4434  preq12b  4823  prneimg  4827  preqsnd  4832  elinti  4928  zfrepclf  5258  dtruALT2  5337  dtruOLD  5413  opth1g  5450  sbcop1  5460  snopeqop  5478  propeqop  5479  otsndisj  5491  otiunsndisj  5492  iunopeqop  5493  po2ne  5574  soasym  5591  elreldm  5912  dfres3  5968  relcnvtrg  6252  relresfld  6262  elpredimg  6302  ordtr2  6394  ordssun  6452  funopg  6566  funimass2  6615  f1imadifssran  6618  f0dom0  6758  elfv2ex  6918  fveqdmss  7064  eldmrexrnb  7078  fvcofneq  7079  funopsn  7134  funopdmsn  7136  funsndifnop  7137  elunirn  7239  2f1fvneq  7248  oprabidw  7430  oprabid  7431  brfvopab  7458  limuni3  7841  peano5  7883  resf1ext2b  7925  op1steq  8026  el2mpocsbcl  8078  bropopvvv  8083  bropfvvvv  8085  f1o2ndf1  8115  frxp  8119  fnwelem  8124  poxp2  8136  suppimacnv  8167  fvn0elsuppb  8174  suppfnss  8182  reldmtpos  8227  rntpos  8232  seqomlem2  8459  oaordi  8552  oa00  8565  oalimcl  8566  omeulem1  8588  nnaordi  8624  ecopovtrn  8828  undifixp  8942  mapdom2  9156  unxpdomlem3  9254  en1eqsn  9274  enp1iOLD  9280  infssuni  9352  wdompwdom  9584  preleqg  9621  opthreg  9624  inf3lemd  9633  inf3lem2  9635  inf3lem6  9639  cnfcomlem  9705  cnfcom3  9710  karden  9901  carden2a  9972  alephdom  10087  dfac5lem4  10132  dfac5lem4OLD  10134  dfac12r  10153  kmlem2  10158  kmlem12  10168  cfslb2n  10274  alephsing  10282  fin23lem30  10348  fin1a2lem6  10411  fin1a2lem13  10418  axcc2lem  10442  domtriomlem  10448  axdc3lem2  10457  axdc4lem  10461  brdom6disj  10538  alephexp1  10585  pwfseq  10670  addnidpi  10907  indpi  10913  nqereu  10935  ltsonq  10975  distrlem5pr  11033  addcanpr  11052  suplem1pr  11058  suplem2pr  11059  ltsrpr  11083  ltsosr  11100  sqgt0sr  11112  leltne  11316  ltnsym  11325  ltlen  11328  eqlei  11337  eqlei2  11338  infm3  12193  nnunb  12489  0mnnnnn0  12525  elnnnn0b  12537  nn0ge2m1nn  12563  nn0le2is012  12649  btwnz  12688  uz11  12869  xrleltne  13153  xltnegi  13224  xnn0lenn0nn0  13253  xnn0xadd0  13255  xmulasslem2  13290  reltxrnmnf  13350  icogelb  13404  iccleub  13408  uznfz  13616  2ffzeq  13655  elfzonlteqm1  13746  elfzo0l  13761  fzoopth  13767  elfznelfzob  13778  elfzr  13785  elfzlmr  13786  injresinjlem  13792  injresinj  13793  fleqceilz  13860  modadd1  13914  modmul1  13931  modirr  13949  addmodlteq  13953  uzrdgfni  13965  fsuppmapnn0fiub0  14000  fsuppmapnn0ub  14002  seqf1o  14050  expnngt1  14247  hashrabsn01  14379  hashrabsn1  14380  hash1snb  14425  hash1n0  14427  hashf1lem2  14462  hash2prde  14476  hash2prd  14481  hash2pwpr  14482  hashle2pr  14483  hashle2prv  14484  hashge2el2dif  14486  hashge2el2difr  14487  hash3tpde  14499  fundmge2nop0  14508  ffz0iswrd  14546  ccatrcl1  14599  pfxsuff1eqwrdeq  14704  wrdind  14727  wrd2ind  14728  swrdccatin1  14730  swrdccat3blem  14744  2cshwcshw  14831  cshwcsh2id  14834  cshimadifsn  14835  2swrd2eqwrdeq  14959  wwlktovf  14962  wwlktovfo  14964  s3sndisj  14973  s3iunsndisj  14974  relexpindlem  15069  rexico  15359  lo1le  15655  fsum2dlem  15773  ntrivcvg  15900  fprodss  15951  fprod2dlem  15983  0dvds  16281  mod2eq1n2dvds  16351  opoe  16367  omoe  16368  opeo  16369  omeo  16370  m1exp1  16380  nn0enne  16381  nn0o1gt2  16385  gcdneg  16526  dfgcd2  16550  algcvga  16583  eucalglt  16589  lcmf  16637  coprmdvds  16657  divgcdcoprmex  16670  cncongr1  16671  prm2orodd  16695  prm23lt5  16819  pockthi  16912  prmreclem5  16925  ramtcl2  17016  cshwrepswhash1  17107  f1ocpbl  17524  f1ovscpbl  17525  f1olecpbl  17526  monhom  17733  epihom  17740  inveq  17772  invcoisoid  17790  isocoinvid  17791  ciclcl  17800  cicrcl  17801  isinitoi  17997  istermoi  17998  2initoinv  18008  2termoinv  18015  setciso  18089  embedsetcestrclem  18154  ipopos  18531  mgmpropd  18614  gsumval2a  18648  ismnddef  18699  dfgrp2e  18931  symg2bas  19359  snsymgefmndeq  19361  symgvalstruct  19363  symgfix2  19382  gsmsymgreq  19398  pmtrdifellem4  19445  mndodcongi  19509  pj1eu  19662  cycsubmcmn  19855  dprd2da  20010  rngimf1o  20399  rngimrnghm  20400  c0snmgmhm  20407  0ring01eq  20474  elrngchom  20569  rnghmsubcsetclem1  20576  rnghmsubcsetclem2  20577  rngcid  20580  rngcinv  20582  rngciso  20583  funcrngcsetcALT  20586  zrinitorngc  20587  zrtermorngc  20588  elringchom  20598  rhmsubcsetclem1  20605  rhmsubcsetclem2  20606  ringcid  20609  rhmsubcrngclem1  20611  rhmsubcrngclem2  20612  ringciso  20617  zrtermoringc  20620  rhmsubclem3  20632  rhmsubclem4  20633  lmodfopnelem1  20840  lspdisjb  21072  lspsnsubn0  21086  rngqiprngfulem2  21258  irinitoringc  21425  obs2ss  21674  mamufacex  22319  mat0dim0  22390  mat0dimid  22391  mat0dimscm  22392  dmatmat  22417  scmatmat  22432  mat1scmat  22462  1mavmul  22471  mavmulsolcl  22474  gsummatr01  22582  cpmatpmat  22633  cpmadugsumlemF  22799  tg2  22888  tgcl  22892  neii1  23029  neii2  23031  neindisj2  23046  perfopn  23108  ordtbas2  23114  pnfnei  23143  mnfnei  23144  llyidm  23411  txlm  23571  qtopuni  23625  tgqtop  23635  isfild  23781  snfil  23787  fbunfip  23792  fgss2  23797  fmco  23884  fbflim2  23900  cnpflf2  23923  fcfelbas  23959  fcfneii  23960  alexsubALTlem2  23971  alexsubALT  23974  tgpconncompeqg  24035  tsmscl  24058  tngngpim  24583  tgioo  24720  xrsmopn  24737  iccntr  24746  reconnlem2  24752  addcnlem  24789  htpycn  24908  phtpyhtpy  24917  pi1blem  24975  fgcfil  25208  ioombl1lem4  25499  dyadmbl  25538  itg2gt0  25698  ditgneg  25795  dvivthlem1  25950  coeeq2  26184  aannenlem2  26274  sineq0  26469  efif1o  26491  xrlimcnp  26914  vmacl  27064  efvmacl  27066  vmalelog  27152  dchrelbasd  27186  lgsqr  27298  lgsqrmodndvds  27300  gausslemma2dlem0i  27311  2lgslem2  27342  2lgs  27354  2lgsoddprmlem3  27361  2sqnn  27386  2sqreultlem  27394  2sqreultblem  27395  2sqreunnltlem  27397  2sqreunnltblem  27398  sltintdifex  27609  sltres  27610  nosepnelem  27627  nolt02o  27643  sltlend  27719  negsprop  27970  mulsprop  28059  n0subs  28263  elntg2  28896  uhgr0vb  28983  umgrupgr  29014  umgrnloopv  29017  umgredgprv  29018  umgrislfupgrlem  29033  umgredg  29049  uspgrushgr  29088  uspgrupgr  29089  usgruspgr  29091  usgredgprvALT  29106  usgrnloopvALT  29112  uhgr2edg  29119  edg0usgr  29164  egrsubgr  29188  0uhgrsubgr  29190  uhgrspansubgrlem  29201  nbuhgr  29254  cusgrsize2inds  29365  cusgrfilem2  29368  vtxdg0v  29385  1loopgrnb0  29414  vtxdginducedm1lem4  29454  wlkvtxeledg  29536  wlkeq  29546  wlkl1loop  29550  wlk1walk  29551  upgrwlkedg  29554  uspgr2wlkeq  29558  wlkv0  29563  wlkonl1iedg  29577  wlkon2n0  29578  wlkp1lem8  29592  wlkp1  29593  lfgrwlkprop  29599  lfgrwlknloop  29601  2pthnloop  29645  upgrwlkdvde  29651  spthonepeq  29666  uhgrwkspthlem2  29668  usgr2wlkneq  29670  usgr2trlncl  29674  usgr2trlspth  29675  pthdlem2lem  29681  clwlkcompbp  29696  uspgrn2crct  29722  wwlks  29749  wwlknbp  29756  0enwwlksnge1  29778  wwlkswwlksn  29779  wlklnwwlkln1  29782  wwlksnextproplem3  29825  wwlksnextprop  29826  wspthsnonn0vne  29831  wspn0  29838  2pthon3v  29857  umgr2adedgspth  29862  rusgr0edg  29887  clwwlkccat  29903  clwlkclwwlklem2fv2  29909  clwlkclwwlklem2a4  29910  clwlkclwwlklem2  29913  clwlkclwwlkflem  29917  clwwlknp  29950  clwwlkwwlksb  29967  clwwlkext2edg  29969  erclwwlkneqlen  29981  hashecclwwlkn1  29990  umgrhashecclwwlk  29991  clwwlknonwwlknonb  30019  upgr1wlkdlem1  30058  upgr3v3e3cycl  30093  uhgr3cyclexlem  30094  1conngr  30107  conngrv2edg  30108  eupth2lem3lem4  30144  eulercrct  30155  isfrgr  30173  frgr3vlem2  30187  1to2vfriswmgr  30192  1to3vfriswmgr  30193  frgrncvvdeqlem9  30220  frgrwopreg  30236  frgr2wwlkeqm  30244  2wspmdisj  30250  numclwwlk1lem2f  30268  frgrreggt1  30306  frgrregord013  30308  frgrregord13  30309  l2p  30392  nmlno0lem  30706  normgt0  31040  ocin  31209  nmlnop0iALT  31908  nmopun  31927  cvpss  32198  cvnbtwn  32199  atcvati  32299  mdsymlem6  32321  iunrnmptss  32479  expgt0b  32728  wrdt2ind  32848  irngssv  33645  issgon  34062  mbfmcnt  34208  ballotlemfc0  34433  ballotlemfcc  34434  satfv0  35301  satfv0fun  35314  fmla1  35330  gonarlem  35337  gonar  35338  goalrlem  35339  goalr  35340  fmla0disjsuc  35341  satffunlem  35344  satffunlem1lem1  35345  satffunlem2lem1  35347  satfun  35354  satfv0fvfmla0  35356  sategoelfv  35363  mthmblem  35523  pprodss4v  35823  funpartfun  35882  funpartfv  35884  5segofs  35945  btwnxfr  35995  brofs2  36016  brifs2  36017  btwnconn1  36040  segleantisym  36054  broutsideof2  36061  outsidene1  36062  outsidene2  36063  funray  36079  lineunray  36086  cldbnd  36265  bj-imdirval3  37123  topdifinffinlem  37286  isbasisrelowllem1  37294  isbasisrelowllem2  37295  relowlpssretop  37303  inunissunidif  37314  pibt2  37356  matunitlindf  37563  poimir  37598  volsupnfl  37610  itg2addnclem  37616  cover2  37660  sdclem2  37687  fdc  37690  sstotbnd3  37721  heibor1  37755  clmgmOLD  37796  smgrpmgm  37809  smgrpassOLD  37810  dvrunz  37899  0rngo  37972  mopickr  38302  lsatcvat  38989  lshpkrex  39057  cmtbr3N  39193  atn0  39247  atnle  39256  cvlsupr4  39284  cvlsupr5  39285  cvlsupr6  39286  cvrval4N  39354  cvratlem  39361  2llnjN  39507  2lplnj  39560  linepsubN  39692  elpaddatiN  39745  elpcliN  39833  pclcmpatN  39841  ldilval  40053  ltrnu  40061  cdleme18d  40235  tendotp  40701  tendof  40703  tendovalco  40705  diatrl  40984  diaintclN  40998  dvheveccl  41052  dibintclN  41107  dihord6apre  41196  dihmeetlem1N  41230  dihpN  41276  dihintcl  41284  dochkrshp4  41329  oexpreposd  42295  pw2f1ocnv  42986  iocinico  43161  onsucf1olem  43219  succlg  43277  oacl2g  43279  omabs2  43281  omcl2  43282  naddcnfcom  43315  naddcnfass  43318  safesnsupfidom1o  43366  infordmin  43481  pr2cv  43497  expgrowthi  44283  iotavalsb  44383  bi23imp1  44446  ioogtlb  45452  iocgtlb  45459  iocleub  45460  icoltub  45465  iooltub  45467  stoweidlem31  45990  oppr  46987  funressnfv  47000  fsetsniunop  47006  fsetsnf1  47009  eu2ndop1stv  47082  afvelrnb0  47121  otiunsndisjX  47236  el1fzopredsuc  47282  2ffzoeq  47284  uniimaprimaeqfv  47314  elsetpreimafveqfv  47324  iccpartimp  47349  iccpartrn  47362  iccpartf  47363  iccpartnel  47370  fargshiftf  47372  fargshiftfo  47374  ichnfimlem  47395  ichnfim  47396  ichreuopeq  47405  sprel  47416  sprsymrelfvlem  47422  sprsymrelfolem2  47425  prproropf1olem4  47438  prprelb  47448  poprelb  47456  fmtnofac1  47502  prmdvdsfmtnof1lem2  47517  31prm  47529  lighneallem3  47539  nn0o1gt2ALTV  47626  nn0oALTV  47628  odd2prm2  47650  mogoldbblem  47652  fpprbasnn  47661  fpprnn  47662  sbgoldbaltlem1  47711  nnsum3primesle9  47726  bgoldbtbndlem1  47737  bgoldbtbndlem2  47738  grtriproplem  47851  grtriprop  47853  cycl3grtrilem  47858  cycl3grtri  47859  isubgr3stgrlem8  47885  gpgvtxel2  47951  upwlkbprop  47999  clcllaw  48052  intop  48064  assintop  48070  assintopcllaw  48073  elrngchomALTV  48130  rngccatidALTV  48133  rngcinvALTV  48137  rngcisoALTV  48138  rhmsubcALTVlem3  48144  rhmsubcALTVlem4  48145  funcringcsetcALTV2lem7  48157  elringchomALTV  48164  ringccatidALTV  48167  ringcisoALTV  48172  funcringcsetclem7ALTV  48180  ztprmneprm  48208  suppmptcfin  48237  linccl  48276  linc1  48287  lincolss  48296  ldepspr  48335  nn0sumshdiglem1  48487  0aryfvalelfv  48501  rrxlines  48599  rrxsphere  48614  itsclc0yqsol  48630  itschlc0xyqsol1  48632  fdomne0  48708  f002  48712  fvconstr2  48720  fullthinc  49123