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  1967  sb4a  2482  hbsb2  2484  dfsb2  2495  2eu2  2651  reu6  3682  2reu2  3846  sseq0  4353  disjel  4407  disjpss  4411  preq12b  4804  prneimg  4808  preqsnd  4813  elinti  4909  zfrepclf  5234  dtruALT2  5313  opth1g  5424  sbcop1  5434  snopeqop  5452  propeqop  5453  otsndisj  5465  otiunsndisj  5466  iunopeqop  5467  po2ne  5546  soasym  5563  elreldm  5882  dfres3  5941  relcnvtrg  6223  relresfld  6232  elpredimg  6272  ordtr2  6360  ordssun  6419  funopg  6524  funimass2  6573  f1imadifssran  6576  f0dom0  6716  elfv2ex  6875  fveqdmss  7021  eldmrexrnb  7035  fvcofneq  7036  funopsn  7091  funopdmsn  7093  funsndifnop  7094  elunirn  7195  oprabidw  7387  oprabid  7388  brfvopab  7413  limuni3  7792  peano5  7833  resf1ext2b  7875  op1steq  7975  el2mpocsbcl  8025  bropopvvv  8030  bropfvvvv  8032  f1o2ndf1  8062  frxp  8066  fnwelem  8071  poxp2  8083  suppimacnv  8114  fvn0elsuppb  8121  suppfnss  8129  reldmtpos  8174  rntpos  8179  seqomlem2  8380  oaordi  8471  oa00  8484  oalimcl  8485  omeulem1  8507  nnaordi  8544  ecopovtrn  8755  undifixp  8870  mapdom2  9074  unxpdomlem3  9156  en1eqsn  9173  infssuni  9244  wdompwdom  9481  preleqg  9522  opthreg  9525  inf3lemd  9534  inf3lem2  9536  inf3lem6  9540  cnfcomlem  9606  cnfcom3  9611  karden  9805  carden2a  9876  alephdom  9989  dfac5lem4  10034  dfac5lem4OLD  10036  dfac12r  10055  kmlem2  10060  kmlem12  10070  cfslb2n  10176  alephsing  10184  fin23lem30  10250  fin1a2lem6  10313  fin1a2lem13  10320  axcc2lem  10344  domtriomlem  10350  axdc3lem2  10359  axdc4lem  10363  brdom6disj  10440  alephexp1  10488  pwfseq  10573  addnidpi  10810  indpi  10816  nqereu  10838  ltsonq  10878  distrlem5pr  10936  addcanpr  10955  suplem1pr  10961  suplem2pr  10962  ltsrpr  10986  ltsosr  11003  sqgt0sr  11015  leltne  11220  ltnsym  11229  ltlen  11232  eqlei  11241  eqlei2  11242  infm3  12099  nnunb  12395  0mnnnnn0  12431  elnnnn0b  12443  nn0ge2m1nn  12469  nn0le2is012  12554  btwnz  12593  uz11  12774  xrleltne  13057  xltnegi  13129  xnn0lenn0nn0  13158  xnn0xadd0  13160  xmulasslem2  13195  reltxrnmnf  13256  icogelb  13310  iccleub  13315  uznfz  13524  2ffzeq  13563  elfzonlteqm1  13655  elfzo0l  13670  fzoopth  13676  elfznelfzob  13688  elfzr  13695  elfzlmr  13696  injresinjlem  13704  injresinj  13705  fleqceilz  13772  modadd1  13826  modmul1  13845  modirr  13863  addmodlteq  13867  uzrdgfni  13879  fsuppmapnn0fiub0  13914  fsuppmapnn0ub  13916  seqf1o  13964  expnngt1  14162  hashrabsn01  14294  hashrabsn1  14295  hash1snb  14340  hash1n0  14342  hashf1lem2  14377  hash2prde  14391  hash2prd  14396  hash2pwpr  14397  hashle2pr  14398  hashle2prv  14399  hashge2el2dif  14401  hashge2el2difr  14402  hash3tpde  14414  fundmge2nop0  14423  ffz0iswrd  14462  ccatrcl1  14516  pfxsuff1eqwrdeq  14620  wrdind  14643  wrd2ind  14644  swrdccatin1  14646  swrdccat3blem  14660  2cshwcshw  14746  cshwcsh2id  14749  cshimadifsn  14750  2swrd2eqwrdeq  14874  wwlktovf  14877  wwlktovfo  14879  s3sndisj  14888  s3iunsndisj  14889  relexpindlem  14984  rexico  15275  lo1le  15573  fsum2dlem  15691  ntrivcvg  15818  fprodss  15869  fprod2dlem  15901  0dvds  16201  mod2eq1n2dvds  16272  opoe  16288  omoe  16289  opeo  16290  omeo  16291  m1exp1  16301  nn0enne  16302  nn0o1gt2  16306  gcdneg  16447  dfgcd2  16471  algcvga  16504  eucalglt  16510  lcmf  16558  coprmdvds  16578  divgcdcoprmex  16591  cncongr1  16592  prm2orodd  16616  prm23lt5  16740  pockthi  16833  prmreclem5  16846  ramtcl2  16937  cshwrepswhash1  17028  f1ocpbl  17444  f1ovscpbl  17445  f1olecpbl  17446  monhom  17657  epihom  17664  inveq  17696  invcoisoid  17714  isocoinvid  17715  ciclcl  17724  cicrcl  17725  isinitoi  17921  istermoi  17922  2initoinv  17932  2termoinv  17939  setciso  18013  embedsetcestrclem  18078  ipopos  18457  mgmpropd  18574  gsumval2a  18608  ismnddef  18659  dfgrp2e  18891  symg2bas  19320  snsymgefmndeq  19322  symgvalstruct  19324  symgfix2  19343  gsmsymgreq  19359  pmtrdifellem4  19406  mndodcongi  19470  pj1eu  19623  cycsubmcmn  19816  dprd2da  19971  rngimf1o  20388  rngimrnghm  20389  c0snmgmhm  20396  0ring01eq  20460  elrngchom  20555  rnghmsubcsetclem1  20562  rnghmsubcsetclem2  20563  rngcid  20566  rngcinv  20568  rngciso  20569  funcrngcsetcALT  20572  zrinitorngc  20573  zrtermorngc  20574  elringchom  20584  rhmsubcsetclem1  20591  rhmsubcsetclem2  20592  ringcid  20595  rhmsubcrngclem1  20597  rhmsubcrngclem2  20598  ringciso  20603  zrtermoringc  20606  rhmsubclem3  20618  rhmsubclem4  20619  lmodfopnelem1  20847  lspdisjb  21079  lspsnsubn0  21093  rngqiprngfulem2  21265  irinitoringc  21432  obs2ss  21682  mamufacex  22338  mat0dim0  22409  mat0dimid  22410  mat0dimscm  22411  dmatmat  22436  scmatmat  22451  mat1scmat  22481  1mavmul  22490  mavmulsolcl  22493  gsummatr01  22601  cpmatpmat  22652  cpmadugsumlemF  22818  tg2  22907  tgcl  22911  neii1  23048  neii2  23050  neindisj2  23065  perfopn  23127  ordtbas2  23133  pnfnei  23162  mnfnei  23163  llyidm  23430  txlm  23590  qtopuni  23644  tgqtop  23654  isfild  23800  snfil  23806  fbunfip  23811  fgss2  23816  fmco  23903  fbflim2  23919  cnpflf2  23942  fcfelbas  23978  fcfneii  23979  alexsubALTlem2  23990  alexsubALT  23993  tgpconncompeqg  24054  tsmscl  24077  tngngpim  24601  tgioo  24738  xrsmopn  24755  iccntr  24764  reconnlem2  24770  addcnlem  24807  htpycn  24926  phtpyhtpy  24935  pi1blem  24993  fgcfil  25225  ioombl1lem4  25516  dyadmbl  25555  itg2gt0  25715  ditgneg  25812  dvivthlem1  25967  coeeq2  26201  aannenlem2  26291  sineq0  26487  efif1o  26509  xrlimcnp  26932  vmacl  27082  efvmacl  27084  vmalelog  27170  dchrelbasd  27204  lgsqr  27316  lgsqrmodndvds  27318  gausslemma2dlem0i  27329  2lgslem2  27360  2lgs  27372  2lgsoddprmlem3  27379  2sqnn  27404  2sqreultlem  27412  2sqreultblem  27413  2sqreunnltlem  27415  2sqreunnltblem  27416  sltintdifex  27627  sltres  27628  nosepnelem  27645  nolt02o  27661  sltlend  27737  negsprop  28004  mulsprop  28099  onnolt  28234  onslt  28235  n0subs  28322  bdaypw2n0s  28420  elntg2  29007  uhgr0vb  29094  umgrupgr  29125  umgrnloopv  29128  umgredgprv  29129  umgrislfupgrlem  29144  umgredg  29160  uspgrushgr  29199  uspgrupgr  29200  usgruspgr  29202  usgredgprvALT  29217  usgrnloopvALT  29223  uhgr2edg  29230  edg0usgr  29275  egrsubgr  29299  0uhgrsubgr  29301  uhgrspansubgrlem  29312  nbuhgr  29365  cusgrsize2inds  29476  cusgrfilem2  29479  vtxdg0v  29496  1loopgrnb0  29525  vtxdginducedm1lem4  29565  wlkvtxeledg  29646  wlkeq  29656  wlkl1loop  29660  wlk1walk  29661  upgrwlkedg  29664  uspgr2wlkeq  29668  wlkv0  29672  wlkonl1iedg  29686  wlkon2n0  29687  wlkp1lem8  29701  wlkp1  29702  lfgrwlkprop  29708  lfgrwlknloop  29710  2pthnloop  29753  upgrwlkdvde  29759  spthonepeq  29774  uhgrwkspthlem2  29776  usgr2wlkneq  29778  usgr2trlncl  29782  usgr2trlspth  29783  pthdlem2lem  29789  clwlkcompbp  29804  uspgrn2crct  29830  wwlks  29857  wwlknbp  29864  0enwwlksnge1  29886  wwlkswwlksn  29887  wlklnwwlkln1  29890  wwlksnextproplem3  29933  wwlksnextprop  29934  wspthsnonn0vne  29939  wspn0  29946  2pthon3v  29965  umgr2adedgspth  29970  rusgr0edg  29998  clwwlkccat  30014  clwlkclwwlklem2fv2  30020  clwlkclwwlklem2a4  30021  clwlkclwwlklem2  30024  clwlkclwwlkflem  30028  clwwlknp  30061  clwwlkwwlksb  30078  clwwlkext2edg  30080  erclwwlkneqlen  30092  hashecclwwlkn1  30101  umgrhashecclwwlk  30102  clwwlknonwwlknonb  30130  upgr1wlkdlem1  30169  upgr3v3e3cycl  30204  uhgr3cyclexlem  30205  1conngr  30218  conngrv2edg  30219  eupth2lem3lem4  30255  eulercrct  30266  isfrgr  30284  frgr3vlem2  30298  1to2vfriswmgr  30303  1to3vfriswmgr  30304  frgrncvvdeqlem9  30331  frgrwopreg  30347  frgr2wwlkeqm  30355  2wspmdisj  30361  numclwwlk1lem2f  30379  frgrreggt1  30417  frgrregord013  30419  frgrregord13  30420  l2p  30503  nmlno0lem  30817  normgt0  31151  ocin  31320  nmlnop0iALT  32019  nmopun  32038  cvpss  32309  cvnbtwn  32310  atcvati  32410  mdsymlem6  32432  iunrnmptss  32589  expgt0b  32846  wrdt2ind  32984  irngssv  33794  issgon  34229  mbfmcnt  34374  ballotlemfc0  34599  ballotlemfcc  34600  satfv0  35501  satfv0fun  35514  fmla1  35530  gonarlem  35537  gonar  35538  goalrlem  35539  goalr  35540  fmla0disjsuc  35541  satffunlem  35544  satffunlem1lem1  35545  satffunlem2lem1  35547  satfun  35554  satfv0fvfmla0  35556  sategoelfv  35563  mthmblem  35723  pprodss4v  36025  funpartfun  36086  funpartfv  36088  5segofs  36149  btwnxfr  36199  brofs2  36220  brifs2  36221  btwnconn1  36244  segleantisym  36258  broutsideof2  36265  outsidene1  36266  outsidene2  36267  funray  36283  lineunray  36290  cldbnd  36469  bj-imdirval3  37328  topdifinffinlem  37491  isbasisrelowllem1  37499  isbasisrelowllem2  37500  relowlpssretop  37508  inunissunidif  37519  pibt2  37561  matunitlindf  37758  poimir  37793  volsupnfl  37805  itg2addnclem  37811  cover2  37855  sdclem2  37882  fdc  37885  sstotbnd3  37916  heibor1  37950  clmgmOLD  37991  smgrpmgm  38004  smgrpassOLD  38005  dvrunz  38094  0rngo  38167  mopickr  38495  sucmapleftuniq  38602  lsatcvat  39249  lshpkrex  39317  cmtbr3N  39453  atn0  39507  atnle  39516  cvlsupr4  39544  cvlsupr5  39545  cvlsupr6  39546  cvrval4N  39613  cvratlem  39620  2llnjN  39766  2lplnj  39819  linepsubN  39951  elpaddatiN  40004  elpcliN  40092  pclcmpatN  40100  ldilval  40312  ltrnu  40320  cdleme18d  40494  tendotp  40960  tendof  40962  tendovalco  40964  diatrl  41243  diaintclN  41257  dvheveccl  41311  dibintclN  41366  dihord6apre  41455  dihmeetlem1N  41489  dihpN  41535  dihintcl  41543  dochkrshp4  41588  oexpreposd  42519  pw2f1ocnv  43221  iocinico  43396  onsucf1olem  43454  succlg  43512  oacl2g  43514  omabs2  43516  omcl2  43517  naddcnfcom  43550  naddcnfass  43553  safesnsupfidom1o  43600  infordmin  43715  pr2cv  43731  expgrowthi  44516  iotavalsb  44616  bi23imp1  44678  ioogtlb  45683  iocgtlb  45690  iocleub  45691  icoltub  45696  iooltub  45698  stoweidlem31  46217  oppr  47218  funressnfv  47231  fsetsniunop  47237  fsetsnf1  47240  eu2ndop1stv  47313  afvelrnb0  47352  otiunsndisjX  47467  el1fzopredsuc  47513  2ffzoeq  47515  uniimaprimaeqfv  47570  elsetpreimafveqfv  47580  iccpartimp  47605  iccpartrn  47618  iccpartf  47619  iccpartnel  47626  fargshiftf  47628  fargshiftfo  47630  ichnfimlem  47651  ichnfim  47652  ichreuopeq  47661  sprel  47672  sprsymrelfvlem  47678  sprsymrelfolem2  47681  prproropf1olem4  47694  prprelb  47704  poprelb  47712  fmtnofac1  47758  prmdvdsfmtnof1lem2  47773  31prm  47785  lighneallem3  47795  nn0o1gt2ALTV  47882  nn0oALTV  47884  odd2prm2  47906  mogoldbblem  47908  fpprbasnn  47917  fpprnn  47918  sbgoldbaltlem1  47967  nnsum3primesle9  47982  bgoldbtbndlem1  47993  bgoldbtbndlem2  47994  grimedgi  48124  grtriproplem  48127  grtriprop  48129  cycl3grtrilem  48134  cycl3grtri  48135  isubgr3stgrlem8  48161  gpgvtxel2  48236  gpgedgiov  48253  gpgedg2iv  48255  gpgprismgr4cycllem7  48289  pgnbgreunbgrlem1  48301  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  pgnbgreunbgrlem2  48305  pgnbgreunbgrlem4  48307  pgnbgreunbgrlem5  48311  upwlkbprop  48326  clcllaw  48379  intop  48391  assintop  48397  assintopcllaw  48400  elrngchomALTV  48457  rngccatidALTV  48460  rngcinvALTV  48464  rngcisoALTV  48465  rhmsubcALTVlem3  48471  rhmsubcALTVlem4  48472  funcringcsetcALTV2lem7  48484  elringchomALTV  48491  ringccatidALTV  48494  ringcisoALTV  48499  funcringcsetclem7ALTV  48507  ztprmneprm  48535  suppmptcfin  48564  linccl  48602  linc1  48613  lincolss  48622  ldepspr  48661  nn0sumshdiglem1  48809  0aryfvalelfv  48823  rrxlines  48921  rrxsphere  48936  itsclc0yqsol  48952  itschlc0xyqsol1  48954  fdomne0  49037  f002  49041  fvconstr2  49051  fullthinc  49637