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 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ax12i  1993  sb4a  2518  hbsb2  2520  dfsb2  2531  2eu2  2686  reu6  3698  2reu2  3860  sseq0  4367  disjel  4423  disjpss  4427  preq12b  4819  prneimg  4823  preqsnd  4828  elinti  4925  zfrepclf  5256  exnelv  5278  dtruALT2  5342  opth1g  5461  sbcop1  5471  snopeqop  5490  propeqop  5491  otsndisj  5503  otiunsndisj  5504  iunopeqop  5505  iunopeqopOLD  5506  po2ne  5586  soasym  5603  elreldm  5926  dfres3  5984  relcnvtrg  6269  relresfld  6278  elpredimg  6318  ordtr2  6407  ordssun  6466  funopg  6571  funimass2  6620  f0dom0  6763  elfv2ex  6925  fveqdmss  7074  eldmrexrnb  7088  fvcofneq  7089  funopsn  7145  funopsnOLD  7146  funopdmsn  7148  funsndifnop  7149  elunirn  7250  oprabidw  7442  oprabid  7443  brfvopab  7468  limuni3  7848  peano5  7890  resf1ext2b  7932  op1steq  8030  el2mpocsbcl  8080  bropopvvv  8085  bropfvvvv  8087  f1o2ndf1  8117  frxp  8122  fnwelem  8127  poxp2  8139  suppimacnv  8170  fvn0elsuppb  8177  suppfnss  8185  reldmtpos  8230  rntpos  8235  seqomlem2  8438  oaordi  8531  oa00  8544  oalimcl  8545  omeulem1  8567  nnaordi  8604  ecopovtrn  8818  undifixp  8932  mapdom2  9136  unxpdomlem3  9218  en1eqsn  9235  infssuni  9303  wdompwdom  9540  preleqg  9584  opthreg  9587  inf3lemd  9596  inf3lem2  9598  inf3lem6  9602  cnfcomlem  9668  cnfcom3  9673  karden  9881  carden2a  9952  alephdom  10065  dfac5lem4  10110  dfac12r  10130  kmlem2  10135  kmlem12  10145  cfslb2n  10252  alephsing  10260  fin23lem30  10326  fin1a2lem6  10389  fin1a2lem13  10396  axcc2lem  10420  domtriomlem  10426  axdc3lem2  10435  axdc4lem  10439  brdom6disj  10516  alephexp1  10564  pwfseq  10649  addnidpi  10886  indpi  10892  nqereu  10914  ltsonq  10954  distrlem5pr  11012  addcanpr  11031  suplem1pr  11037  suplem2pr  11038  ltsrpr  11062  ltsosr  11079  sqgt0sr  11091  leltne  11299  ltnsym  11308  ltlen  11311  eqlei  11320  eqlei2  11321  infm3  12174  nnunb  12500  0mnnnnn0  12536  elnnnn0b  12548  nn0ge2m1nn  12574  nn0le2is012  12660  btwnz  12699  uz11  12887  xrleltne  13170  xltnegi  13242  xnn0lenn0nn0  13271  xnn0xadd0  13273  xmulasslem2  13308  reltxrnmnf  13369  icogelb  13423  iccleub  13428  uznfz  13638  2ffzeq  13677  elfzonlteqm1  13770  elfzo0l  13785  fzoopth  13791  elfznelfzob  13803  elfzr  13810  elfzlmr  13811  injresinjlem  13819  injresinj  13820  fleqceilz  13887  modadd1  13941  modmul1  13960  modirr  13978  addmodlteq  13982  uzrdgfni  13994  fsuppmapnn0fiub0  14029  fsuppmapnn0ub  14031  seqf1o  14079  expnngt1  14277  hashrabsn01  14409  hashrabsn1  14410  hash1snb  14456  hash1n0  14458  hashf1lem2  14493  hash2prde  14507  hash2prd  14512  hash2pwpr  14513  hashle2pr  14514  hashle2prv  14515  hashge2el2dif  14517  hashge2el2difr  14518  hash3tpde  14530  fundmge2nop0  14539  ffz0iswrd  14578  ccatrcl1  14632  pfxsuff1eqwrdeq  14736  wrdind  14759  wrd2ind  14760  swrdccatin1  14762  swrdccat3blem  14776  2cshwcshw  14862  cshwcsh2id  14865  cshimadifsn  14866  2swrd2eqwrdeq  14990  wwlktovf  14993  wwlktovfo  14995  s3sndisj  15004  s3iunsndisj  15005  relexpindlem  15100  rexico  15405  lo1le  15703  fsum2dlem  15821  ntrivcvg  15951  fprodss  16002  fprod2dlem  16034  0dvds  16334  mod2eq1n2dvds  16405  opoe  16421  omoe  16422  opeo  16423  omeo  16424  m1exp1  16434  nn0enne  16435  nn0o1gt2  16439  gcdneg  16580  dfgcd2  16604  algcvga  16637  eucalglt  16643  lcmf  16691  coprmdvds  16711  divgcdcoprmex  16724  cncongr1  16725  prm2orodd  16749  prm23lt5  16874  pockthi  16967  prmreclem5  16980  ramtcl2  17071  cshwrepswhash1  17162  f1ocpbl  17579  f1ovscpbl  17580  f1olecpbl  17581  monhom  17792  epihom  17799  inveq  17831  invcoisoid  17849  isocoinvid  17850  ciclcl  17859  cicrcl  17860  isinitoi  18056  istermoi  18057  2initoinv  18067  2termoinv  18074  setciso  18148  embedsetcestrclem  18213  ipopos  18592  mgmpropd  18709  gsumval2a  18743  ismnddef  18794  dfgrp2e  19030  symg2bas  19463  snsymgefmndeq  19465  symgvalstruct  19467  symgfix2  19486  gsmsymgreq  19502  pmtrdifellem4  19549  mndodcongi  19613  pj1eu  19766  cycsubmcmn  19959  dprd2da  20114  rngimf1o  20536  rngimrnghm  20537  c0snmgmhm  20544  0ring01eq  20613  elrngchom  20709  rnghmsubcsetclem1  20716  rnghmsubcsetclem2  20717  rngcid  20720  rngcinv  20722  rngciso  20723  funcrngcsetcALT  20726  zrinitorngc  20727  zrtermorngc  20728  elringchom  20738  rhmsubcsetclem1  20745  rhmsubcsetclem2  20746  ringcid  20749  rhmsubcrngclem1  20751  rhmsubcrngclem2  20752  ringciso  20757  zrtermoringc  20760  rhmsubclem3  20772  rhmsubclem4  20773  lmodfopnelem1  20997  lspdisjb  21228  lspsnsubn0  21242  rngqiprngfulem2  21423  irinitoringc  21598  obs2ss  21848  mamufacex  22522  mat0dim0  22593  mat0dimid  22594  mat0dimscm  22595  dmatmat  22620  scmatmat  22635  mat1scmat  22665  1mavmul  22674  mavmulsolcl  22677  gsummatr01  22785  cpmatpmat  22836  cpmadugsumlemF  23002  tg2  23091  tgcl  23095  neii1  23232  neii2  23234  neindisj2  23249  perfopn  23311  ordtbas2  23317  pnfnei  23346  mnfnei  23347  llyidm  23614  txlm  23774  qtopuni  23828  tgqtop  23838  isfild  23984  snfil  23990  fbunfip  23995  fgss2  24000  fmco  24087  fbflim2  24103  cnpflf2  24126  fcfelbas  24162  fcfneii  24163  alexsubALTlem2  24174  alexsubALT  24177  tgpconncompeqg  24238  tsmscl  24261  tngngpim  24785  tgioo  24922  xrsmopn  24939  iccntr  24948  reconnlem2  24954  addcnlem  24991  htpycn  25101  phtpyhtpy  25110  pi1blem  25167  fgcfil  25399  ioombl1lem4  25689  dyadmbl  25728  itg2gt0  25888  ditgneg  25985  dvivthlem1  26136  coeeq2  26368  aannenlem2  26459  sineq0  26655  efif1o  26677  xrlimcnp  27099  vmacl  27248  efvmacl  27250  vmalelog  27335  dchrelbasd  27369  lgsqr  27481  lgsqrmodndvds  27483  gausslemma2dlem0i  27494  2lgslem2  27525  2lgs  27537  2lgsoddprmlem3  27544  2sqnn  27569  2sqreultlem  27577  2sqreultblem  27578  2sqreunnltlem  27580  2sqreunnltblem  27581  ltsintdifex  27791  ltsres  27792  nosepnelem  27809  nolt02o  27825  ltlesnd  27905  negsprop  28194  mulsprop  28289  onnolt  28425  onlts  28426  n0subs  28522  bdaypw2n0bndlem  28622  bdaypw2n0bnd  28623  bdayfinbndlem2  28627  elntg2  29276  uhgr0vb  29363  umgrupgr  29394  umgrnloopv  29397  umgredgprv  29398  umgrislfupgrlem  29413  umgredg  29429  uspgrushgr  29468  uspgrupgr  29469  usgruspgr  29471  usgredgprvALT  29486  usgrnloopvALT  29492  uhgr2edg  29499  edg0usgr  29544  egrsubgr  29568  0uhgrsubgr  29570  uhgrspansubgrlem  29581  nbuhgr  29634  cusgrsize2inds  29744  cusgrfilem2  29747  vtxdg0v  29764  1loopgrnb0  29793  vtxdginducedm1lem4  29833  wlkvtxeledg  29914  wlkeq  29924  wlkl1loop  29928  wlk1walk  29929  upgrwlkedg  29932  uspgr2wlkeq  29936  wlkv0  29940  wlkonl1iedg  29954  wlkon2n0  29955  wlkp1lem8  29969  wlkp1  29970  lfgrwlkprop  29976  lfgrwlknloop  29978  2pthnloop  30021  upgrwlkdvde  30027  spthonepeq  30042  uhgrwkspthlem2  30044  usgr2wlkneq  30046  usgr2trlncl  30050  usgr2trlspth  30051  pthdlem2lem  30057  clwlkcompbp  30072  uspgrn2crct  30098  wwlks  30125  wwlknbp  30132  0enwwlksnge1  30154  wwlkswwlksn  30155  wlklnwwlkln1  30158  wwlksnextproplem3  30201  wwlksnextprop  30202  wspthsnonn0vne  30207  wspn0  30214  2pthon3v  30233  umgr2adedgspth  30238  rusgr0edg  30266  clwwlkccat  30282  clwlkclwwlklem2fv2  30288  clwlkclwwlklem2a4  30289  clwlkclwwlklem2  30292  clwlkclwwlkflem  30296  clwwlknp  30329  clwwlkwwlksb  30346  clwwlkext2edg  30348  erclwwlkneqlen  30360  hashecclwwlkn1  30369  umgrhashecclwwlk  30370  clwwlknonwwlknonb  30398  upgr1wlkdlem1  30437  upgr3v3e3cycl  30472  uhgr3cyclexlem  30473  1conngr  30486  conngrv2edg  30487  eupth2lem3lem4  30523  eulercrct  30534  isfrgr  30552  frgr3vlem2  30566  1to2vfriswmgr  30571  1to3vfriswmgr  30572  frgrncvvdeqlem9  30599  frgrwopreg  30615  frgr2wwlkeqm  30623  2wspmdisj  30629  numclwwlk1lem2f  30647  frgrreggt1  30685  frgrregord013  30687  frgrregord13  30688  l2p  30772  nmlno0lem  31086  normgt0  31420  ocin  31589  nmlnop0iALT  32288  nmopun  32307  cvpss  32578  cvnbtwn  32579  atcvati  32679  mdsymlem6  32701  iunrnmptss  32851  expgt0b  33102  wrdt2ind  33214  irngssv  34023  issgon  34458  mbfmcnt  34603  ballotlemfc0  34828  ballotlemfcc  34829  kardcard2b  35511  satfv0  35783  satfv0fun  35796  fmla1  35812  gonarlem  35819  gonar  35820  goalrlem  35821  goalr  35822  fmla0disjsuc  35823  satffunlem  35826  satffunlem1lem1  35827  satffunlem2lem1  35829  satfun  35836  satfv0fvfmla0  35838  sategoelfv  35845  mthmblem  36005  pprodss4v  36307  funpartfun  36368  funpartfv  36370  5segofs  36431  btwnxfr  36481  brofs2  36502  brifs2  36503  btwnconn1  36526  segleantisym  36540  broutsideof2  36547  outsidene1  36548  outsidene2  36549  funray  36565  lineunray  36572  cldbnd  36760  bj-imdirval3  37750  topdifinffinlem  37915  isbasisrelowllem1  37923  isbasisrelowllem2  37924  relowlpssretop  37932  inunissunidif  37943  pibt2  37985  matunitlindf  38191  poimir  38226  volsupnfl  38238  itg2addnclem  38244  cover2  38288  sdclem2  38315  fdc  38318  sstotbnd3  38349  heibor1  38383  clmgmOLD  38424  smgrpmgm  38437  smgrpassOLD  38438  dvrunz  38527  0rngo  38600  mopickr  38944  sucmapleftuniq  39063  lsatcvat  39748  lshpkrex  39816  cmtbr3N  39952  atn0  40006  atnle  40015  cvlsupr4  40043  cvlsupr5  40044  cvlsupr6  40045  cvrval4N  40112  cvratlem  40119  2llnjN  40265  2lplnj  40318  linepsubN  40450  elpaddatiN  40503  elpcliN  40591  pclcmpatN  40599  ldilval  40811  ltrnu  40819  cdleme18d  40993  tendotp  41459  tendof  41461  tendovalco  41463  diatrl  41742  diaintclN  41756  dvheveccl  41810  dibintclN  41865  dihord6apre  41954  dihmeetlem1N  41988  dihpN  42034  dihintcl  42042  dochkrshp4  42087  oexpreposd  43007  pw2f1ocnv  43690  iocinico  43865  onsucf1olem  43923  succlg  43981  oacl2g  43983  omabs2  43985  omcl2  43986  naddcnfcom  44019  naddcnfass  44022  safesnsupfidom1o  44069  infordmin  44184  pr2cv  44200  expgrowthi  44969  iotavalsb  45069  bi23imp1  45130  ioogtlb  46137  iocgtlb  46144  iocleub  46145  icoltub  46150  iooltub  46152  stoweidlem31  46671  oppr  47690  funressnfv  47703  fsetsniunop  47709  fsetsnf1  47712  eu2ndop1stv  47785  afvelrnb0  47824  otiunsndisjX  47939  el1fzopredsuc  47986  2ffzoeq  47988  uniimaprimaeqfv  48054  elsetpreimafveqfv  48064  iccpartimp  48089  iccpartrn  48102  iccpartf  48103  iccpartnel  48110  fargshiftf  48112  fargshiftfo  48114  ichnfimlem  48135  ichnfim  48136  ichreuopeq  48145  sprel  48156  sprsymrelfvlem  48162  sprsymrelfolem2  48165  prproropf1olem4  48178  prprelb  48188  poprelb  48196  fmtnofac1  48245  prmdvdsfmtnof1lem2  48260  31prm  48272  lighneallem3  48282  ppivalnnnprm  48303  nn0o1gt2ALTV  48382  nn0oALTV  48384  odd2prm2  48406  mogoldbblem  48408  fpprbasnn  48417  fpprnn  48418  sbgoldbaltlem1  48467  nnsum3primesle9  48482  bgoldbtbndlem1  48493  bgoldbtbndlem2  48494  elclnbgrelnbgr  48513  grimedgi  48624  grtriproplem  48627  grtriprop  48629  cycl3grtrilem  48634  cycl3grtri  48635  isubgr3stgrlem8  48661  gpgvtxel2  48736  gpgedgiov  48753  gpgedg2iv  48755  gpgprismgr4cycllem7  48789  pgnbgreunbgrlem1  48801  pgnbgreunbgrlem2lem1  48802  pgnbgreunbgrlem2lem2  48803  pgnbgreunbgrlem2lem3  48804  pgnbgreunbgrlem2  48805  pgnbgreunbgrlem4  48807  pgnbgreunbgrlem5  48811  upwlkbprop  48826  clcllaw  48879  intop  48891  assintop  48897  assintopcllaw  48900  elrngchomALTV  48957  rngccatidALTV  48960  rngcinvALTV  48964  rngcisoALTV  48965  rhmsubcALTVlem3  48971  rhmsubcALTVlem4  48972  funcringcsetcALTV2lem7  48984  elringchomALTV  48991  ringccatidALTV  48994  ringcisoALTV  48999  funcringcsetclem7ALTV  49007  prmringnzring  49025  ztprmneprm  49046  suppmptcfin  49075  linccl  49113  linc1  49124  lincolss  49133  ldepspr  49172  nn0sumshdiglem1  49320  0aryfvalelfv  49334  rrxlines  49432  rrxsphere  49447  itsclc0yqsol  49463  itschlc0xyqsol1  49465  fdomne0  49547  f002  49551  fvconstr2  49561  fullthinc  50147