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  2509  hbsb2  2511  dfsb2  2522  2eu2  2677  reu6  3684  nrmod  3839  2reu2  3846  disjel  4410  disjpss  4414  preq12b  4810  prneimg  4814  preqsnd  4819  elinti  4916  zfrepclf  5246  exnelv  5270  dtruALT2  5335  opth1g  5454  sbcop1  5464  snopeqop  5483  propeqop  5484  otsndisj  5496  otiunsndisj  5497  iunopeqop  5498  iunopeqopOLD  5499  po2ne  5579  soasym  5596  elreldm  5919  dfres3  5977  relcnvtrgOLD  6264  relresfldOLD  6274  elpredimg  6314  ordtr2  6403  ordssun  6462  funopg  6568  funimass2  6617  f0dom0  6760  elfv2ex  6922  fveqdmss  7072  eldmrexrnb  7086  fvcofneq  7087  funopsn  7145  funopsnOLD  7146  funopdmsn  7148  funsndifnop  7149  elunirn  7249  oprabidw  7445  oprabid  7446  brfvopab  7471  limuni3  7849  peano5  7891  resf1ext2b  7933  op1steq  8031  el2mpocsbcl  8083  bropopvvv  8088  bropfvvvv  8090  f1o2ndf1  8120  frxp  8125  fnwelem  8130  poxp2  8142  suppimacnv  8173  fvn0elsuppb  8180  suppfnss  8188  reldmtpos  8233  rntpos  8238  seqomlem2  8443  oaordi  8536  oa00  8549  oalimcl  8550  omeulem1  8572  nnaordi  8609  ecopovtrn  8823  undifixp  8944  mapdom2  9149  unxpdomlem3  9231  en1eqsn  9248  infssuni  9316  wdompwdom  9553  preleqg  9597  opthreg  9600  inf3lemd  9609  inf3lem2  9611  inf3lem6  9615  cnfcomlem  9681  cnfcom3  9686  karden  9901  kardenOLD  9902  carden2a  9974  alephdom  10087  dfac5lem4  10132  dfac12r  10152  kmlem2  10157  kmlem12  10167  cfslb2n  10273  alephsing  10281  fin23lem30  10347  fin1a2lem6  10410  fin1a2lem13  10417  axcc2lem  10441  domtriomlem  10447  axdc3lem2  10456  axdc4lem  10460  brdom6disj  10538  alephexp1  10591  pwfseq  10676  addnidpi  10913  indpi  10919  nqereu  10941  ltsonq  10981  distrlem5pr  11039  addcanpr  11058  suplem1pr  11064  suplem2pr  11065  ltsrpr  11089  ltsosr  11106  sqgt0sr  11118  leltne  11326  ltnsym  11335  ltlen  11338  eqlei  11347  eqlei2  11348  infm3  12201  nnunb  12527  0mnnnnn0  12563  elnnnn0b  12575  nn0ge2m1nn  12601  nn0le2is012  12688  btwnz  12727  uz11  12915  xrleltne  13199  xltnegi  13271  xnn0lenn0nn0  13300  xnn0xadd0  13302  xmulasslem2  13337  reltxrnmnf  13398  icogelb  13452  iccleub  13457  uznfz  13668  2ffzeq  13707  elfzonlteqm1  13800  elfzo0l  13815  fzoopth  13821  elfznelfzob  13833  elfzr  13840  elfzlmr  13841  injresinjlem  13849  injresinj  13850  fleqceilz  13918  modadd1  13972  modmul1  13991  modirr  14009  addmodlteq  14013  uzrdgfni  14025  fsuppmapnn0fiub0  14060  fsuppmapnn0ub  14062  seqf1o  14110  expnngt1  14308  hashrabsn01  14440  hashrabsn1  14441  hash1snb  14487  hash1n0  14489  hashf1lem2  14524  hash2prde  14538  hash2prd  14543  hash2pwpr  14544  hashle2pr  14545  hashle2prv  14546  hashge2el2dif  14548  hashge2el2difr  14549  hash3tpde  14561  fundmge2nop0  14570  ffz0iswrd  14609  ccatrcl1  14664  pfxsuff1eqwrdeq  14771  wrdind  14794  wrd2ind  14795  swrdccatin1  14797  swrdccat3blem  14811  2cshwcshw  14899  cshwcsh2id  14902  cshimadifsn  14903  2swrd2eqwrdeq  15029  wwlktovf  15032  wwlktovfo  15034  s3sndisj  15043  s3iunsndisj  15044  relexpindlem  15139  rexico  15444  lo1le  15742  fsum2dlem  15859  ntrivcvg  15989  fprodss  16038  fprod2dlem  16070  0dvds  16369  mod2eq1n2dvds  16440  opoe  16456  omoe  16457  opeo  16458  omeo  16459  m1exp1  16469  nn0enne  16470  nn0o1gt2  16474  gcdneg  16615  dfgcd2  16639  algcvga  16672  eucalglt  16678  lcmf  16726  coprmdvds  16746  divgcdcoprmex  16759  cncongr1  16760  prm2orodd  16784  prm23lt5  16909  pockthi  17002  prmreclem5  17015  ramtcl2  17106  cshwrepswhash1  17197  f1ocpbl  17614  f1ovscpbl  17615  f1olecpbl  17616  monhom  17827  epihom  17834  inveq  17866  invcoisoid  17884  isocoinvid  17885  ciclcl  17894  cicrcl  17895  isinitoi  18091  istermoi  18092  2initoinv  18102  2termoinv  18109  setciso  18183  embedsetcestrclem  18248  ipopos  18627  mgmpropd  18746  gsumval2a  18790  ismnddef  18841  dfgrp2e  19090  symg2bas  19523  snsymgefmndeq  19525  symgvalstruct  19527  symgfix2  19546  gsmsymgreq  19562  pmtrdifellem4  19609  mndodcongi  19673  pj1eu  19826  cycsubmcmn  20019  dprd2da  20174  rngimf1o  20598  rngimrnghm  20599  c0snmgmhm  20606  0ring01eq  20693  elrngchom  20789  rnghmsubcsetclem1  20796  rnghmsubcsetclem2  20797  rngcid  20800  rngcinv  20802  rngciso  20803  funcrngcsetcALT  20806  zrinitorngc  20807  zrtermorngc  20808  elringchom  20818  rhmsubcsetclem1  20825  rhmsubcsetclem2  20826  ringcid  20829  rhmsubcrngclem1  20831  rhmsubcrngclem2  20832  ringciso  20837  zrtermoringc  20840  rhmsubclem3  20852  rhmsubclem4  20853  lmodfopnelem1  21085  lspdisjb  21316  lspsnsubn0  21330  rngqiprngfulem2  21518  irinitoringc  21695  obs2ss  21945  mamufacex  22621  mat0dim0  22692  mat0dimid  22693  mat0dimscm  22694  dmatmat  22719  scmatmat  22734  mat1scmat  22764  1mavmul  22773  mavmulsolcl  22776  gsummatr01  22884  matunitlindf  22906  cpmatpmat  22938  cpmadugsumlemF  23104  tg2  23193  tgcl  23197  neii1  23334  neii2  23336  neindisj2  23351  perfopn  23413  ordtbas2  23419  pnfnei  23448  mnfnei  23449  llyidm  23717  txlm  23877  qtopuni  23931  tgqtop  23941  isfild  24087  snfil  24093  fbunfip  24098  fgss2  24103  fmco  24190  fbflim2  24206  cnpflf2  24229  fcfelbas  24265  fcfneii  24266  alexsubALTlem2  24277  alexsubALT  24280  tgpconncompeqg  24341  tsmscl  24364  tngngpim  24888  tgioo  25025  xrsmopn  25042  iccntr  25051  reconnlem2  25057  addcnlem  25094  htpycn  25204  phtpyhtpy  25213  pi1blem  25270  fgcfil  25502  ioombl1lem4  25792  dyadmbl  25831  itg2gt0  25991  ditgneg  26087  dvivthlem1  26238  coeeq2  26471  aannenlem2  26568  sineq0  26764  efif1o  26786  xrlimcnp  27208  vmacl  27357  efvmacl  27359  vmalelog  27444  dchrelbasd  27478  lgsqr  27590  lgsqrmodndvds  27592  gausslemma2dlem0i  27603  2lgslem2  27634  2lgs  27646  2lgsoddprmlem3  27653  2sqnn  27678  2sqreultlem  27686  2sqreultblem  27687  2sqreunnltlem  27689  2sqreunnltblem  27690  ltsintdifex  27900  ltsres  27901  nosepnelem  27918  nolt02o  27934  ltlesnd  28014  negsprop  28303  mulsprop  28398  onnolt  28534  onlts  28535  n0subs  28631  bdaypw2n0bndlem  28731  bdaypw2n0bnd  28732  bdayfinbndlem2  28736  elntg2  29445  uhgr0vb  29532  umgrupgr  29563  umgrnloopv  29566  umgredgprv  29567  umgrislfupgrlem  29582  umgredg  29598  uspgrushgr  29640  uspgrupgr  29641  usgruspgr  29643  usgredgprvALT  29658  usgrnloopvALT  29664  uhgr2edg  29671  edg0usgr  29716  egrsubgr  29740  0uhgrsubgr  29742  uhgrspansubgrlem  29753  nbuhgr  29806  cusgrsize2inds  29916  cusgrfilem2  29919  vtxdg0v  29936  1loopgrnb0  29965  vtxdginducedm1lem4  30005  wlkvtxeledg  30086  wlkeq  30096  wlkl1loop  30100  wlk1walk  30101  upgrwlkedg  30104  uspgr2wlkeq  30108  wlkv0  30112  wlkonl1iedg  30126  wlkon2n0  30127  wlkp1lem8  30141  wlkp1  30142  lfgrwlkprop  30152  lfgrwlknloop  30154  2pthnloop  30199  upgrwlkdvde  30205  spthonepeq  30220  uhgrwkspthlem2  30222  usgr2wlkneq  30224  usgr2trlncl  30228  usgr2trlspth  30229  pthdlem2lem  30235  clwlkcompbp  30251  uspgrn2crct  30279  wwlks  30306  wwlknbp  30313  0enwwlksnge1  30335  wwlkswwlksn  30336  wlklnwwlkln1  30339  wwlksnextproplem3  30382  wwlksnextprop  30383  wspthsnonn0vne  30388  wspn0  30395  2pthon3v  30414  umgr2adedgspth  30419  rusgr0edg  30447  clwwlkccat  30463  clwlkclwwlklem2fv2  30469  clwlkclwwlklem2a4  30470  clwlkclwwlklem2  30473  clwlkclwwlkflem  30477  clwwlknp  30510  clwwlkwwlksb  30527  clwwlkext2edg  30529  erclwwlkneqlen  30541  hashecclwwlkn1  30550  umgrhashecclwwlk  30551  clwwlknonwwlknonb  30579  upgr1wlkdlem1  30618  upgr3v3e3cycl  30663  uhgr3cyclexlem  30664  1conngr  30677  conngrv2edg  30678  eupth2lem3lem4  30714  eulercrct  30725  isfrgr  30743  frgr3vlem2  30757  1to2vfriswmgr  30762  1to3vfriswmgr  30763  frgrncvvdeqlem9  30790  frgrwopreg  30806  frgr2wwlkeqm  30814  2wspmdisj  30820  numclwwlk1lem2f  30838  frgrreggt1  30876  frgrregord013  30878  frgrregord13  30879  l2p  30963  nmlno0lem  31277  normgt0  31611  ocin  31780  nmlnop0iALT  32479  nmopun  32498  cvpss  32769  cvnbtwn  32770  atcvati  32870  mdsymlem6  32892  iunrnmptss  33041  expgt0b  33290  wrdt2ind  33398  irngssv  34201  issgon  34636  mbfmcnt  34782  ballotlemfc0  35007  ballotlemfcc  35008  kardcard2b  35694  satfv0  35940  satfv0fun  35953  fmla1  35969  gonarlem  35976  gonar  35977  goalrlem  35978  goalr  35979  fmla0disjsuc  35980  satffunlem  35983  satffunlem1lem1  35984  satffunlem2lem1  35986  satfun  35993  satfv0fvfmla0  35995  sategoelfv  36002  mthmblem  36162  pprodss4v  36464  funpartfun  36525  funpartfv  36527  5segofs  36589  btwnxfr  36639  brofs2  36660  brifs2  36661  btwnconn1  36684  segleantisym  36698  broutsideof2  36705  outsidene1  36706  outsidene2  36707  funray  36723  lineunray  36730  cldbnd  36948  bj-imdirval3  37939  topdifinffinlem  38104  isbasisrelowllem1  38112  isbasisrelowllem2  38113  relowlpssretop  38121  inunissunidif  38132  pibt2  38174  poimir  38405  volsupnfl  38417  itg2addnclem  38423  findcard4  38466  cover2  38468  sdclem2  38495  fdc  38498  sstotbnd3  38529  heibor1  38563  clmgmOLD  38604  smgrpmgm  38617  smgrpassOLD  38618  dvrunz  38707  0rngo  38780  mopickr  39122  sucmapleftuniq  39241  lsatcvat  39926  lshpkrex  39994  cmtbr3N  40130  atn0  40184  atnle  40193  cvlsupr4  40221  cvlsupr5  40222  cvlsupr6  40223  cvrval4N  40290  cvratlem  40297  2llnjN  40443  2lplnj  40496  linepsubN  40628  elpaddatiN  40681  elpcliN  40769  pclcmpatN  40777  ldilval  40989  ltrnu  40997  cdleme18d  41171  tendotp  41637  tendof  41639  tendovalco  41641  diatrl  41920  diaintclN  41934  dvheveccl  41988  dibintclN  42043  dihord6apre  42132  dihmeetlem1N  42166  dihpN  42212  dihintcl  42220  dochkrshp4  42265  oexpreposd  43200  pw2f1ocnv  43881  iocinico  44056  onsucf1olem  44114  succlg  44172  oacl2g  44174  omabs2  44176  omcl2  44177  naddcnfcom  44210  naddcnfass  44213  safesnsupfidom1o  44260  infordmin  44375  pr2cv  44391  expgrowthi  45160  iotavalsb  45260  bi23imp1  45321  ioogtlb  46328  iocgtlb  46335  iocleub  46336  icoltub  46341  iooltub  46343  stoweidlem31  46862  oppr  47921  funressnfv  47934  fsetsniunop  47940  fsetsnf1  47943  eu2ndop1stv  48016  afvelrnb0  48055  otiunsndisjX  48170  el1fzopredsuc  48217  2ffzoeq  48219  uniimaprimaeqfv  48285  elsetpreimafveqfv  48295  iccpartimp  48320  iccpartrn  48333  iccpartf  48334  iccpartnel  48341  fargshiftf  48343  fargshiftfo  48345  ichnfimlem  48366  ichnfim  48367  ichreuopeq  48376  sprel  48387  sprsymrelfvlem  48393  sprsymrelfolem2  48396  prproropf1olem4  48409  prprelb  48419  poprelb  48427  fmtnofac1  48476  prmdvdsfmtnof1lem2  48491  31prm  48503  lighneallem3  48513  ppivalnnnprm  48534  nn0o1gt2ALTV  48613  nn0oALTV  48615  odd2prm2  48637  mogoldbblem  48639  fpprbasnn  48648  fpprnn  48649  sbgoldbaltlem1  48698  nnsum3primesle9  48713  bgoldbtbndlem1  48724  bgoldbtbndlem2  48725  elclnbgrelnbgr  48744  grimedgi  48855  grtriproplem  48858  grtriprop  48860  cycl3grtrilem  48865  cycl3grtri  48866  isubgr3stgrlem8  48892  gpgvtxel2  48967  gpgedgiov  48984  gpgedg2iv  48986  gpgprismgr4cycllem7  49020  pgnbgreunbgrlem1  49032  pgnbgreunbgrlem2lem1  49033  pgnbgreunbgrlem2lem2  49034  pgnbgreunbgrlem2lem3  49035  pgnbgreunbgrlem2  49036  pgnbgreunbgrlem4  49038  pgnbgreunbgrlem5  49042  upwlkbprop  49057  clcllaw  49109  intop  49121  assintop  49127  assintopcllaw  49130  elrngchomALTV  49187  rngccatidALTV  49190  rngcinvALTV  49194  rngcisoALTV  49195  rhmsubcALTVlem3  49201  rhmsubcALTVlem4  49202  funcringcsetcALTV2lem7  49214  elringchomALTV  49221  ringccatidALTV  49224  ringcisoALTV  49229  funcringcsetclem7ALTV  49237  prmringnzring  49255  ztprmneprm  49280  suppmptcfin  49309  linccl  49347  linc1  49358  lincolss  49367  ldepspr  49406  nn0sumshdiglem1  49554  0aryfvalelfv  49568  rrxlines  49666  rrxsphere  49681  itsclc0yqsol  49697  itschlc0xyqsol1  49699  fdomne0  49781  f002  49785  elovconstbrd  49795  fullthinc  50379