Theorem biimtrdi 256

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 232	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 36	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ax12i  1999  sb4a  2514  hbsb2  2516  dfsb2  2527  2eu2  2682  reu6  3691  nrmod  3846  2reu2  3853  disjel  4417  disjpss  4421  preq12b  4817  prneimg  4821  preqsnd  4826  elinti  4923  zfrepclf  5254  exnelv  5278  dtruALT2  5343  opth1g  5462  sbcop1  5472  snopeqop  5491  propeqop  5492  otsndisj  5504  otiunsndisj  5505  iunopeqop  5506  iunopeqopOLD  5507  po2ne  5587  soasym  5604  elreldm  5927  dfres3  5985  relcnvtrgOLD  6271  relresfldOLD  6281  elpredimg  6321  ordtr2  6410  ordssun  6469  funopg  6574  funimass2  6623  f0dom0  6766  elfv2ex  6928  fveqdmss  7077  eldmrexrnb  7091  fvcofneq  7092  funopsn  7150  funopsnOLD  7151  funopdmsn  7153  funsndifnop  7154  elunirn  7254  oprabidw  7450  oprabid  7451  brfvopab  7476  limuni3  7854  peano5  7896  resf1ext2b  7938  op1steq  8036  el2mpocsbcl  8086  bropopvvv  8091  bropfvvvv  8093  f1o2ndf1  8123  frxp  8128  fnwelem  8133  poxp2  8145  suppimacnv  8176  fvn0elsuppb  8183  suppfnss  8191  reldmtpos  8236  rntpos  8241  seqomlem2  8444  oaordi  8537  oa00  8550  oalimcl  8551  omeulem1  8573  nnaordi  8610  ecopovtrn  8824  undifixp  8938  mapdom2  9143  unxpdomlem3  9225  en1eqsn  9242  infssuni  9310  wdompwdom  9547  preleqg  9591  opthreg  9594  inf3lemd  9603  inf3lem2  9605  inf3lem6  9609  cnfcomlem  9675  cnfcom3  9680  karden  9895  kardenOLD  9896  carden2a  9968  alephdom  10081  dfac5lem4  10126  dfac12r  10146  kmlem2  10151  kmlem12  10161  cfslb2n  10267  alephsing  10275  fin23lem30  10341  fin1a2lem6  10404  fin1a2lem13  10411  axcc2lem  10435  domtriomlem  10441  axdc3lem2  10450  axdc4lem  10454  brdom6disj  10532  alephexp1  10583  pwfseq  10668  addnidpi  10905  indpi  10911  nqereu  10933  ltsonq  10973  distrlem5pr  11031  addcanpr  11050  suplem1pr  11056  suplem2pr  11057  ltsrpr  11081  ltsosr  11098  sqgt0sr  11110  leltne  11318  ltnsym  11327  ltlen  11330  eqlei  11339  eqlei2  11340  infm3  12193  nnunb  12519  0mnnnnn0  12555  elnnnn0b  12567  nn0ge2m1nn  12593  nn0le2is012  12680  btwnz  12719  uz11  12907  xrleltne  13190  xltnegi  13262  xnn0lenn0nn0  13291  xnn0xadd0  13293  xmulasslem2  13328  reltxrnmnf  13389  icogelb  13443  iccleub  13448  uznfz  13659  2ffzeq  13698  elfzonlteqm1  13791  elfzo0l  13806  fzoopth  13812  elfznelfzob  13824  elfzr  13831  elfzlmr  13832  injresinjlem  13840  injresinj  13841  fleqceilz  13909  modadd1  13963  modmul1  13982  modirr  14000  addmodlteq  14004  uzrdgfni  14016  fsuppmapnn0fiub0  14051  fsuppmapnn0ub  14053  seqf1o  14101  expnngt1  14299  hashrabsn01  14431  hashrabsn1  14432  hash1snb  14478  hash1n0  14480  hashf1lem2  14515  hash2prde  14529  hash2prd  14534  hash2pwpr  14535  hashle2pr  14536  hashle2prv  14537  hashge2el2dif  14539  hashge2el2difr  14540  hash3tpde  14552  fundmge2nop0  14561  ffz0iswrd  14600  ccatrcl1  14655  pfxsuff1eqwrdeq  14762  wrdind  14785  wrd2ind  14786  swrdccatin1  14788  swrdccat3blem  14802  2cshwcshw  14890  cshwcsh2id  14893  cshimadifsn  14894  2swrd2eqwrdeq  15018  wwlktovf  15021  wwlktovfo  15023  s3sndisj  15032  s3iunsndisj  15033  relexpindlem  15128  rexico  15433  lo1le  15731  fsum2dlem  15848  ntrivcvg  15978  fprodss  16029  fprod2dlem  16061  0dvds  16360  mod2eq1n2dvds  16431  opoe  16447  omoe  16448  opeo  16449  omeo  16450  m1exp1  16460  nn0enne  16461  nn0o1gt2  16465  gcdneg  16606  dfgcd2  16630  algcvga  16663  eucalglt  16669  lcmf  16717  coprmdvds  16737  divgcdcoprmex  16750  cncongr1  16751  prm2orodd  16775  prm23lt5  16900  pockthi  16993  prmreclem5  17006  ramtcl2  17097  cshwrepswhash1  17188  f1ocpbl  17605  f1ovscpbl  17606  f1olecpbl  17607  monhom  17818  epihom  17825  inveq  17857  invcoisoid  17875  isocoinvid  17876  ciclcl  17885  cicrcl  17886  isinitoi  18082  istermoi  18083  2initoinv  18093  2termoinv  18100  setciso  18174  embedsetcestrclem  18239  ipopos  18618  mgmpropd  18737  gsumval2a  18779  ismnddef  18830  dfgrp2e  19078  symg2bas  19511  snsymgefmndeq  19513  symgvalstruct  19515  symgfix2  19534  gsmsymgreq  19550  pmtrdifellem4  19597  mndodcongi  19661  pj1eu  19814  cycsubmcmn  20007  dprd2da  20162  rngimf1o  20586  rngimrnghm  20587  c0snmgmhm  20594  0ring01eq  20681  elrngchom  20777  rnghmsubcsetclem1  20784  rnghmsubcsetclem2  20785  rngcid  20788  rngcinv  20790  rngciso  20791  funcrngcsetcALT  20794  zrinitorngc  20795  zrtermorngc  20796  elringchom  20806  rhmsubcsetclem1  20813  rhmsubcsetclem2  20814  ringcid  20817  rhmsubcrngclem1  20819  rhmsubcrngclem2  20820  ringciso  20825  zrtermoringc  20828  rhmsubclem3  20840  rhmsubclem4  20841  lmodfopnelem1  21073  lspdisjb  21304  lspsnsubn0  21318  rngqiprngfulem2  21506  irinitoringc  21683  obs2ss  21933  mamufacex  22607  mat0dim0  22678  mat0dimid  22679  mat0dimscm  22680  dmatmat  22705  scmatmat  22720  mat1scmat  22750  1mavmul  22759  mavmulsolcl  22762  gsummatr01  22870  cpmatpmat  22921  cpmadugsumlemF  23087  tg2  23176  tgcl  23180  neii1  23317  neii2  23319  neindisj2  23334  perfopn  23396  ordtbas2  23402  pnfnei  23431  mnfnei  23432  llyidm  23700  txlm  23860  qtopuni  23914  tgqtop  23924  isfild  24070  snfil  24076  fbunfip  24081  fgss2  24086  fmco  24173  fbflim2  24189  cnpflf2  24212  fcfelbas  24248  fcfneii  24249  alexsubALTlem2  24260  alexsubALT  24263  tgpconncompeqg  24324  tsmscl  24347  tngngpim  24871  tgioo  25008  xrsmopn  25025  iccntr  25034  reconnlem2  25040  addcnlem  25077  htpycn  25187  phtpyhtpy  25196  pi1blem  25253  fgcfil  25485  ioombl1lem4  25775  dyadmbl  25814  itg2gt0  25974  ditgneg  26071  dvivthlem1  26222  coeeq2  26454  aannenlem2  26547  sineq0  26744  efif1o  26766  xrlimcnp  27188  vmacl  27337  efvmacl  27339  vmalelog  27424  dchrelbasd  27458  lgsqr  27570  lgsqrmodndvds  27572  gausslemma2dlem0i  27583  2lgslem2  27614  2lgs  27626  2lgsoddprmlem3  27633  2sqnn  27658  2sqreultlem  27666  2sqreultblem  27667  2sqreunnltlem  27669  2sqreunnltblem  27670  ltsintdifex  27880  ltsres  27881  nosepnelem  27898  nolt02o  27914  ltlesnd  27994  negsprop  28283  mulsprop  28378  onnolt  28514  onlts  28515  n0subs  28611  bdaypw2n0bndlem  28711  bdaypw2n0bnd  28712  bdayfinbndlem2  28716  elntg2  29394  uhgr0vb  29481  umgrupgr  29512  umgrnloopv  29515  umgredgprv  29516  umgrislfupgrlem  29531  umgredg  29547  uspgrushgr  29589  uspgrupgr  29590  usgruspgr  29592  usgredgprvALT  29607  usgrnloopvALT  29613  uhgr2edg  29620  edg0usgr  29665  egrsubgr  29689  0uhgrsubgr  29691  uhgrspansubgrlem  29702  nbuhgr  29755  cusgrsize2inds  29865  cusgrfilem2  29868  vtxdg0v  29885  1loopgrnb0  29914  vtxdginducedm1lem4  29954  wlkvtxeledg  30035  wlkeq  30045  wlkl1loop  30049  wlk1walk  30050  upgrwlkedg  30053  uspgr2wlkeq  30057  wlkv0  30061  wlkonl1iedg  30075  wlkon2n0  30076  wlkp1lem8  30090  wlkp1  30091  lfgrwlkprop  30101  lfgrwlknloop  30103  2pthnloop  30148  upgrwlkdvde  30154  spthonepeq  30169  uhgrwkspthlem2  30171  usgr2wlkneq  30173  usgr2trlncl  30177  usgr2trlspth  30178  pthdlem2lem  30184  clwlkcompbp  30200  uspgrn2crct  30228  wwlks  30255  wwlknbp  30262  0enwwlksnge1  30284  wwlkswwlksn  30285  wlklnwwlkln1  30288  wwlksnextproplem3  30331  wwlksnextprop  30332  wspthsnonn0vne  30337  wspn0  30344  2pthon3v  30363  umgr2adedgspth  30368  rusgr0edg  30396  clwwlkccat  30412  clwlkclwwlklem2fv2  30418  clwlkclwwlklem2a4  30419  clwlkclwwlklem2  30422  clwlkclwwlkflem  30426  clwwlknp  30459  clwwlkwwlksb  30476  clwwlkext2edg  30478  erclwwlkneqlen  30490  hashecclwwlkn1  30499  umgrhashecclwwlk  30500  clwwlknonwwlknonb  30528  upgr1wlkdlem1  30567  upgr3v3e3cycl  30606  uhgr3cyclexlem  30607  1conngr  30620  conngrv2edg  30621  eupth2lem3lem4  30657  eulercrct  30668  isfrgr  30686  frgr3vlem2  30700  1to2vfriswmgr  30705  1to3vfriswmgr  30706  frgrncvvdeqlem9  30733  frgrwopreg  30749  frgr2wwlkeqm  30757  2wspmdisj  30763  numclwwlk1lem2f  30781  frgrreggt1  30819  frgrregord013  30821  frgrregord13  30822  l2p  30906  nmlno0lem  31220  normgt0  31554  ocin  31723  nmlnop0iALT  32422  nmopun  32441  cvpss  32712  cvnbtwn  32713  atcvati  32813  mdsymlem6  32835  iunrnmptss  32985  expgt0b  33235  wrdt2ind  33343  irngssv  34146  issgon  34581  mbfmcnt  34727  ballotlemfc0  34952  ballotlemfcc  34953  kardcard2b  35639  satfv0  35891  satfv0fun  35904  fmla1  35920  gonarlem  35927  gonar  35928  goalrlem  35929  goalr  35930  fmla0disjsuc  35931  satffunlem  35934  satffunlem1lem1  35935  satffunlem2lem1  35937  satfun  35944  satfv0fvfmla0  35946  sategoelfv  35953  mthmblem  36113  pprodss4v  36415  funpartfun  36476  funpartfv  36478  5segofs  36539  btwnxfr  36589  brofs2  36610  brifs2  36611  btwnconn1  36634  segleantisym  36648  broutsideof2  36655  outsidene1  36656  outsidene2  36657  funray  36673  lineunray  36680  cldbnd  36898  bj-imdirval3  37889  topdifinffinlem  38054  isbasisrelowllem1  38062  isbasisrelowllem2  38063  relowlpssretop  38071  inunissunidif  38082  pibt2  38124  matunitlindf  38330  poimir  38365  volsupnfl  38377  itg2addnclem  38383  findcard4  38426  cover2  38428  sdclem2  38455  fdc  38458  sstotbnd3  38489  heibor1  38523  clmgmOLD  38564  smgrpmgm  38577  smgrpassOLD  38578  dvrunz  38667  0rngo  38740  mopickr  39082  sucmapleftuniq  39201  lsatcvat  39886  lshpkrex  39954  cmtbr3N  40090  atn0  40144  atnle  40153  cvlsupr4  40181  cvlsupr5  40182  cvlsupr6  40183  cvrval4N  40250  cvratlem  40257  2llnjN  40403  2lplnj  40456  linepsubN  40588  elpaddatiN  40641  elpcliN  40729  pclcmpatN  40737  ldilval  40949  ltrnu  40957  cdleme18d  41131  tendotp  41597  tendof  41599  tendovalco  41601  diatrl  41880  diaintclN  41894  dvheveccl  41948  dibintclN  42003  dihord6apre  42092  dihmeetlem1N  42126  dihpN  42172  dihintcl  42180  dochkrshp4  42225  oexpreposd  43160  pw2f1ocnv  43841  iocinico  44016  onsucf1olem  44074  succlg  44132  oacl2g  44134  omabs2  44136  omcl2  44137  naddcnfcom  44170  naddcnfass  44173  safesnsupfidom1o  44220  infordmin  44335  pr2cv  44351  expgrowthi  45120  iotavalsb  45220  bi23imp1  45281  ioogtlb  46288  iocgtlb  46295  iocleub  46296  icoltub  46301  iooltub  46303  stoweidlem31  46822  oppr  47844  funressnfv  47857  fsetsniunop  47863  fsetsnf1  47866  eu2ndop1stv  47939  afvelrnb0  47978  otiunsndisjX  48093  el1fzopredsuc  48140  2ffzoeq  48142  uniimaprimaeqfv  48208  elsetpreimafveqfv  48218  iccpartimp  48243  iccpartrn  48256  iccpartf  48257  iccpartnel  48264  fargshiftf  48266  fargshiftfo  48268  ichnfimlem  48289  ichnfim  48290  ichreuopeq  48299  sprel  48310  sprsymrelfvlem  48316  sprsymrelfolem2  48319  prproropf1olem4  48332  prprelb  48342  poprelb  48350  fmtnofac1  48399  prmdvdsfmtnof1lem2  48414  31prm  48426  lighneallem3  48436  ppivalnnnprm  48457  nn0o1gt2ALTV  48536  nn0oALTV  48538  odd2prm2  48560  mogoldbblem  48562  fpprbasnn  48571  fpprnn  48572  sbgoldbaltlem1  48621  nnsum3primesle9  48636  bgoldbtbndlem1  48647  bgoldbtbndlem2  48648  elclnbgrelnbgr  48667  grimedgi  48778  grtriproplem  48781  grtriprop  48783  cycl3grtrilem  48788  cycl3grtri  48789  isubgr3stgrlem8  48815  gpgvtxel2  48890  gpgedgiov  48907  gpgedg2iv  48909  gpgprismgr4cycllem7  48943  pgnbgreunbgrlem1  48955  pgnbgreunbgrlem2lem1  48956  pgnbgreunbgrlem2lem2  48957  pgnbgreunbgrlem2lem3  48958  pgnbgreunbgrlem2  48959  pgnbgreunbgrlem4  48961  pgnbgreunbgrlem5  48965  upwlkbprop  48980  clcllaw  49032  intop  49044  assintop  49050  assintopcllaw  49053  elrngchomALTV  49110  rngccatidALTV  49113  rngcinvALTV  49117  rngcisoALTV  49118  rhmsubcALTVlem3  49124  rhmsubcALTVlem4  49125  funcringcsetcALTV2lem7  49137  elringchomALTV  49144  ringccatidALTV  49147  ringcisoALTV  49152  funcringcsetclem7ALTV  49160  prmringnzring  49178  ztprmneprm  49203  suppmptcfin  49232  linccl  49270  linc1  49281  lincolss  49290  ldepspr  49329  nn0sumshdiglem1  49477  0aryfvalelfv  49491  rrxlines  49589  rrxsphere  49604  itsclc0yqsol  49620  itschlc0xyqsol1  49622  fdomne0  49704  f002  49708  fvconstr2  49718  fullthinc  50304