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  3694  2reu2  3858  sseq0  4362  disjel  4416  disjpss  4420  preq12b  4810  prneimg  4814  preqsnd  4819  elinti  4915  zfrepclf  5241  dtruALT2  5320  dtruOLD  5396  opth1g  5433  sbcop1  5443  snopeqop  5461  propeqop  5462  otsndisj  5474  otiunsndisj  5475  iunopeqop  5476  po2ne  5555  soasym  5572  elreldm  5888  dfres3  5944  relcnvtrg  6227  relresfld  6237  elpredimg  6277  ordtr2  6365  ordssun  6424  funopg  6534  funimass2  6583  f1imadifssran  6586  f0dom0  6726  elfv2ex  6886  fveqdmss  7032  eldmrexrnb  7046  fvcofneq  7047  funopsn  7102  funopdmsn  7104  funsndifnop  7105  elunirn  7207  oprabidw  7400  oprabid  7401  brfvopab  7426  limuni3  7808  peano5  7849  resf1ext2b  7891  op1steq  7991  el2mpocsbcl  8041  bropopvvv  8046  bropfvvvv  8048  f1o2ndf1  8078  frxp  8082  fnwelem  8087  poxp2  8099  suppimacnv  8130  fvn0elsuppb  8137  suppfnss  8145  reldmtpos  8190  rntpos  8195  seqomlem2  8396  oaordi  8487  oa00  8500  oalimcl  8501  omeulem1  8523  nnaordi  8559  ecopovtrn  8770  undifixp  8884  mapdom2  9089  unxpdomlem3  9175  en1eqsn  9195  enp1iOLD  9201  infssuni  9273  wdompwdom  9507  preleqg  9544  opthreg  9547  inf3lemd  9556  inf3lem2  9558  inf3lem6  9562  cnfcomlem  9628  cnfcom3  9633  karden  9824  carden2a  9895  alephdom  10010  dfac5lem4  10055  dfac5lem4OLD  10057  dfac12r  10076  kmlem2  10081  kmlem12  10091  cfslb2n  10197  alephsing  10205  fin23lem30  10271  fin1a2lem6  10334  fin1a2lem13  10341  axcc2lem  10365  domtriomlem  10371  axdc3lem2  10380  axdc4lem  10384  brdom6disj  10461  alephexp1  10508  pwfseq  10593  addnidpi  10830  indpi  10836  nqereu  10858  ltsonq  10898  distrlem5pr  10956  addcanpr  10975  suplem1pr  10981  suplem2pr  10982  ltsrpr  11006  ltsosr  11023  sqgt0sr  11035  leltne  11239  ltnsym  11248  ltlen  11251  eqlei  11260  eqlei2  11261  infm3  12118  nnunb  12414  0mnnnnn0  12450  elnnnn0b  12462  nn0ge2m1nn  12488  nn0le2is012  12574  btwnz  12613  uz11  12794  xrleltne  13081  xltnegi  13152  xnn0lenn0nn0  13181  xnn0xadd0  13183  xmulasslem2  13218  reltxrnmnf  13279  icogelb  13333  iccleub  13338  uznfz  13547  2ffzeq  13586  elfzonlteqm1  13678  elfzo0l  13693  fzoopth  13699  elfznelfzob  13710  elfzr  13717  elfzlmr  13718  injresinjlem  13724  injresinj  13725  fleqceilz  13792  modadd1  13846  modmul1  13865  modirr  13883  addmodlteq  13887  uzrdgfni  13899  fsuppmapnn0fiub0  13934  fsuppmapnn0ub  13936  seqf1o  13984  expnngt1  14182  hashrabsn01  14314  hashrabsn1  14315  hash1snb  14360  hash1n0  14362  hashf1lem2  14397  hash2prde  14411  hash2prd  14416  hash2pwpr  14417  hashle2pr  14418  hashle2prv  14419  hashge2el2dif  14421  hashge2el2difr  14422  hash3tpde  14434  fundmge2nop0  14443  ffz0iswrd  14482  ccatrcl1  14535  pfxsuff1eqwrdeq  14640  wrdind  14663  wrd2ind  14664  swrdccatin1  14666  swrdccat3blem  14680  2cshwcshw  14767  cshwcsh2id  14770  cshimadifsn  14771  2swrd2eqwrdeq  14895  wwlktovf  14898  wwlktovfo  14900  s3sndisj  14909  s3iunsndisj  14910  relexpindlem  15005  rexico  15296  lo1le  15594  fsum2dlem  15712  ntrivcvg  15839  fprodss  15890  fprod2dlem  15922  0dvds  16222  mod2eq1n2dvds  16293  opoe  16309  omoe  16310  opeo  16311  omeo  16312  m1exp1  16322  nn0enne  16323  nn0o1gt2  16327  gcdneg  16468  dfgcd2  16492  algcvga  16525  eucalglt  16531  lcmf  16579  coprmdvds  16599  divgcdcoprmex  16612  cncongr1  16613  prm2orodd  16637  prm23lt5  16761  pockthi  16854  prmreclem5  16867  ramtcl2  16958  cshwrepswhash1  17049  f1ocpbl  17464  f1ovscpbl  17465  f1olecpbl  17466  monhom  17677  epihom  17684  inveq  17716  invcoisoid  17734  isocoinvid  17735  ciclcl  17744  cicrcl  17745  isinitoi  17941  istermoi  17942  2initoinv  17952  2termoinv  17959  setciso  18033  embedsetcestrclem  18098  ipopos  18477  mgmpropd  18560  gsumval2a  18594  ismnddef  18645  dfgrp2e  18877  symg2bas  19307  snsymgefmndeq  19309  symgvalstruct  19311  symgfix2  19330  gsmsymgreq  19346  pmtrdifellem4  19393  mndodcongi  19457  pj1eu  19610  cycsubmcmn  19803  dprd2da  19958  rngimf1o  20374  rngimrnghm  20375  c0snmgmhm  20382  0ring01eq  20449  elrngchom  20544  rnghmsubcsetclem1  20551  rnghmsubcsetclem2  20552  rngcid  20555  rngcinv  20557  rngciso  20558  funcrngcsetcALT  20561  zrinitorngc  20562  zrtermorngc  20563  elringchom  20573  rhmsubcsetclem1  20580  rhmsubcsetclem2  20581  ringcid  20584  rhmsubcrngclem1  20586  rhmsubcrngclem2  20587  ringciso  20592  zrtermoringc  20595  rhmsubclem3  20607  rhmsubclem4  20608  lmodfopnelem1  20836  lspdisjb  21068  lspsnsubn0  21082  rngqiprngfulem2  21254  irinitoringc  21421  obs2ss  21671  mamufacex  22316  mat0dim0  22387  mat0dimid  22388  mat0dimscm  22389  dmatmat  22414  scmatmat  22429  mat1scmat  22459  1mavmul  22468  mavmulsolcl  22471  gsummatr01  22579  cpmatpmat  22630  cpmadugsumlemF  22796  tg2  22885  tgcl  22889  neii1  23026  neii2  23028  neindisj2  23043  perfopn  23105  ordtbas2  23111  pnfnei  23140  mnfnei  23141  llyidm  23408  txlm  23568  qtopuni  23622  tgqtop  23632  isfild  23778  snfil  23784  fbunfip  23789  fgss2  23794  fmco  23881  fbflim2  23897  cnpflf2  23920  fcfelbas  23956  fcfneii  23957  alexsubALTlem2  23968  alexsubALT  23971  tgpconncompeqg  24032  tsmscl  24055  tngngpim  24580  tgioo  24717  xrsmopn  24734  iccntr  24743  reconnlem2  24749  addcnlem  24786  htpycn  24905  phtpyhtpy  24914  pi1blem  24972  fgcfil  25204  ioombl1lem4  25495  dyadmbl  25534  itg2gt0  25694  ditgneg  25791  dvivthlem1  25946  coeeq2  26180  aannenlem2  26270  sineq0  26466  efif1o  26488  xrlimcnp  26911  vmacl  27061  efvmacl  27063  vmalelog  27149  dchrelbasd  27183  lgsqr  27295  lgsqrmodndvds  27297  gausslemma2dlem0i  27308  2lgslem2  27339  2lgs  27351  2lgsoddprmlem3  27358  2sqnn  27383  2sqreultlem  27391  2sqreultblem  27392  2sqreunnltlem  27394  2sqreunnltblem  27395  sltintdifex  27606  sltres  27607  nosepnelem  27624  nolt02o  27640  sltlend  27716  negsprop  27981  mulsprop  28073  onnolt  28207  onslt  28208  n0subs  28293  elntg2  28965  uhgr0vb  29052  umgrupgr  29083  umgrnloopv  29086  umgredgprv  29087  umgrislfupgrlem  29102  umgredg  29118  uspgrushgr  29157  uspgrupgr  29158  usgruspgr  29160  usgredgprvALT  29175  usgrnloopvALT  29181  uhgr2edg  29188  edg0usgr  29233  egrsubgr  29257  0uhgrsubgr  29259  uhgrspansubgrlem  29270  nbuhgr  29323  cusgrsize2inds  29434  cusgrfilem2  29437  vtxdg0v  29454  1loopgrnb0  29483  vtxdginducedm1lem4  29523  wlkvtxeledg  29604  wlkeq  29614  wlkl1loop  29618  wlk1walk  29619  upgrwlkedg  29622  uspgr2wlkeq  29626  wlkv0  29630  wlkonl1iedg  29644  wlkon2n0  29645  wlkp1lem8  29659  wlkp1  29660  lfgrwlkprop  29666  lfgrwlknloop  29668  2pthnloop  29711  upgrwlkdvde  29717  spthonepeq  29732  uhgrwkspthlem2  29734  usgr2wlkneq  29736  usgr2trlncl  29740  usgr2trlspth  29741  pthdlem2lem  29747  clwlkcompbp  29762  uspgrn2crct  29788  wwlks  29815  wwlknbp  29822  0enwwlksnge1  29844  wwlkswwlksn  29845  wlklnwwlkln1  29848  wwlksnextproplem3  29891  wwlksnextprop  29892  wspthsnonn0vne  29897  wspn0  29904  2pthon3v  29923  umgr2adedgspth  29928  rusgr0edg  29953  clwwlkccat  29969  clwlkclwwlklem2fv2  29975  clwlkclwwlklem2a4  29976  clwlkclwwlklem2  29979  clwlkclwwlkflem  29983  clwwlknp  30016  clwwlkwwlksb  30033  clwwlkext2edg  30035  erclwwlkneqlen  30047  hashecclwwlkn1  30056  umgrhashecclwwlk  30057  clwwlknonwwlknonb  30085  upgr1wlkdlem1  30124  upgr3v3e3cycl  30159  uhgr3cyclexlem  30160  1conngr  30173  conngrv2edg  30174  eupth2lem3lem4  30210  eulercrct  30221  isfrgr  30239  frgr3vlem2  30253  1to2vfriswmgr  30258  1to3vfriswmgr  30259  frgrncvvdeqlem9  30286  frgrwopreg  30302  frgr2wwlkeqm  30310  2wspmdisj  30316  numclwwlk1lem2f  30334  frgrreggt1  30372  frgrregord013  30374  frgrregord13  30375  l2p  30458  nmlno0lem  30772  normgt0  31106  ocin  31275  nmlnop0iALT  31974  nmopun  31993  cvpss  32264  cvnbtwn  32265  atcvati  32365  mdsymlem6  32387  iunrnmptss  32544  expgt0b  32791  wrdt2ind  32925  irngssv  33676  issgon  34106  mbfmcnt  34252  ballotlemfc0  34477  ballotlemfcc  34478  satfv0  35338  satfv0fun  35351  fmla1  35367  gonarlem  35374  gonar  35375  goalrlem  35376  goalr  35377  fmla0disjsuc  35378  satffunlem  35381  satffunlem1lem1  35382  satffunlem2lem1  35384  satfun  35391  satfv0fvfmla0  35393  sategoelfv  35400  mthmblem  35560  pprodss4v  35865  funpartfun  35924  funpartfv  35926  5segofs  35987  btwnxfr  36037  brofs2  36058  brifs2  36059  btwnconn1  36082  segleantisym  36096  broutsideof2  36103  outsidene1  36104  outsidene2  36105  funray  36121  lineunray  36128  cldbnd  36307  bj-imdirval3  37165  topdifinffinlem  37328  isbasisrelowllem1  37336  isbasisrelowllem2  37337  relowlpssretop  37345  inunissunidif  37356  pibt2  37398  matunitlindf  37605  poimir  37640  volsupnfl  37652  itg2addnclem  37658  cover2  37702  sdclem2  37729  fdc  37732  sstotbnd3  37763  heibor1  37797  clmgmOLD  37838  smgrpmgm  37851  smgrpassOLD  37852  dvrunz  37941  0rngo  38014  mopickr  38338  lsatcvat  39036  lshpkrex  39104  cmtbr3N  39240  atn0  39294  atnle  39303  cvlsupr4  39331  cvlsupr5  39332  cvlsupr6  39333  cvrval4N  39401  cvratlem  39408  2llnjN  39554  2lplnj  39607  linepsubN  39739  elpaddatiN  39792  elpcliN  39880  pclcmpatN  39888  ldilval  40100  ltrnu  40108  cdleme18d  40282  tendotp  40748  tendof  40750  tendovalco  40752  diatrl  41031  diaintclN  41045  dvheveccl  41099  dibintclN  41154  dihord6apre  41243  dihmeetlem1N  41277  dihpN  41323  dihintcl  41331  dochkrshp4  41376  oexpreposd  42303  pw2f1ocnv  43019  iocinico  43194  onsucf1olem  43252  succlg  43310  oacl2g  43312  omabs2  43314  omcl2  43315  naddcnfcom  43348  naddcnfass  43351  safesnsupfidom1o  43399  infordmin  43514  pr2cv  43530  expgrowthi  44315  iotavalsb  44415  bi23imp1  44478  ioogtlb  45486  iocgtlb  45493  iocleub  45494  icoltub  45499  iooltub  45501  stoweidlem31  46022  oppr  47024  funressnfv  47037  fsetsniunop  47043  fsetsnf1  47046  eu2ndop1stv  47119  afvelrnb0  47158  otiunsndisjX  47273  el1fzopredsuc  47319  2ffzoeq  47321  uniimaprimaeqfv  47376  elsetpreimafveqfv  47386  iccpartimp  47411  iccpartrn  47424  iccpartf  47425  iccpartnel  47432  fargshiftf  47434  fargshiftfo  47436  ichnfimlem  47457  ichnfim  47458  ichreuopeq  47467  sprel  47478  sprsymrelfvlem  47484  sprsymrelfolem2  47487  prproropf1olem4  47500  prprelb  47510  poprelb  47518  fmtnofac1  47564  prmdvdsfmtnof1lem2  47579  31prm  47591  lighneallem3  47601  nn0o1gt2ALTV  47688  nn0oALTV  47690  odd2prm2  47712  mogoldbblem  47714  fpprbasnn  47723  fpprnn  47724  sbgoldbaltlem1  47773  nnsum3primesle9  47788  bgoldbtbndlem1  47799  bgoldbtbndlem2  47800  grtriproplem  47931  grtriprop  47933  cycl3grtrilem  47938  cycl3grtri  47939  isubgr3stgrlem8  47965  gpgvtxel2  48032  gpgedgiov  48049  gpgedg2iv  48051  gpgprismgr4cycllem7  48084  pgnbgreunbgrlem1  48096  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgnbgreunbgrlem2lem3  48099  pgnbgreunbgrlem2  48100  pgnbgreunbgrlem4  48102  pgnbgreunbgrlem5  48106  upwlkbprop  48119  clcllaw  48172  intop  48184  assintop  48190  assintopcllaw  48193  elrngchomALTV  48250  rngccatidALTV  48253  rngcinvALTV  48257  rngcisoALTV  48258  rhmsubcALTVlem3  48264  rhmsubcALTVlem4  48265  funcringcsetcALTV2lem7  48277  elringchomALTV  48284  ringccatidALTV  48287  ringcisoALTV  48292  funcringcsetclem7ALTV  48300  ztprmneprm  48328  suppmptcfin  48357  linccl  48396  linc1  48407  lincolss  48416  ldepspr  48455  nn0sumshdiglem1  48603  0aryfvalelfv  48617  rrxlines  48715  rrxsphere  48730  itsclc0yqsol  48746  itschlc0xyqsol1  48748  fdomne0  48831  f002  48835  fvconstr2  48845  fullthinc  49432