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  2488  hbsb2  2490  dfsb2  2501  2eu2  2656  nfabdwOLD  2933  reu6  3748  2reu2  3920  sseq0  4426  disjel  4480  disjpss  4484  preq12b  4875  prneimg  4879  preqsnd  4883  elinti  4979  zfrepclf  5312  dtruALT2  5388  dtruOLD  5461  opth1g  5498  sbcop1  5508  snopeqop  5525  propeqop  5526  otsndisj  5538  otiunsndisj  5539  iunopeqop  5540  po2ne  5624  soasym  5640  elreldm  5960  dfres3  6014  relcnvtrg  6297  relresfld  6307  elpredimg  6347  ordtr2  6439  ordssun  6497  funopg  6612  funimass2  6661  f0dom0  6805  elfv2ex  6966  fveqdmss  7112  eldmrexrnb  7126  fvcofneq  7127  funopsn  7182  funopdmsn  7184  funsndifnop  7185  elunirn  7288  2f1fvneq  7297  oprabidw  7479  oprabid  7480  brfvopab  7507  limuni3  7889  peano5  7932  peano5OLD  7933  op1steq  8074  el2mpocsbcl  8126  bropopvvv  8131  bropfvvvv  8133  f1o2ndf1  8163  frxp  8167  fnwelem  8172  poxp2  8184  suppimacnv  8215  fvn0elsuppb  8222  suppfnss  8230  reldmtpos  8275  rntpos  8280  seqomlem2  8507  oaordi  8602  oa00  8615  oalimcl  8616  omeulem1  8638  nnaordi  8674  ecopovtrn  8878  undifixp  8992  mapdom2  9214  unxpdomlem3  9315  en1eqsn  9336  enp1iOLD  9342  infssuni  9414  wdompwdom  9647  preleqg  9684  opthreg  9687  inf3lemd  9696  inf3lem2  9698  inf3lem6  9702  cnfcomlem  9768  cnfcom3  9773  karden  9964  carden2a  10035  alephdom  10150  dfac5lem4  10195  dfac5lem4OLD  10197  dfac12r  10216  kmlem2  10221  kmlem12  10231  cfslb2n  10337  alephsing  10345  fin23lem30  10411  fin1a2lem6  10474  fin1a2lem13  10481  axcc2lem  10505  domtriomlem  10511  axdc3lem2  10520  axdc4lem  10524  brdom6disj  10601  alephexp1  10648  pwfseq  10733  addnidpi  10970  indpi  10976  nqereu  10998  ltsonq  11038  distrlem5pr  11096  addcanpr  11115  suplem1pr  11121  suplem2pr  11122  ltsrpr  11146  ltsosr  11163  sqgt0sr  11175  leltne  11379  ltnsym  11388  ltlen  11391  eqlei  11400  eqlei2  11401  infm3  12254  nnunb  12549  0mnnnnn0  12585  elnnnn0b  12597  nn0ge2m1nn  12622  nn0le2is012  12707  btwnz  12746  uz11  12928  xrleltne  13207  xltnegi  13278  xnn0lenn0nn0  13307  xnn0xadd0  13309  xmulasslem2  13344  reltxrnmnf  13404  icogelb  13458  iccleub  13462  uznfz  13667  2ffzeq  13706  elfzonlteqm1  13792  elfzo0l  13806  fzoopth  13812  elfznelfzob  13823  elfzr  13830  elfzlmr  13831  injresinjlem  13837  injresinj  13838  fleqceilz  13905  modadd1  13959  modmul1  13975  modirr  13993  addmodlteq  13997  uzrdgfni  14009  fsuppmapnn0fiub0  14044  fsuppmapnn0ub  14046  seqf1o  14094  expnngt1  14290  hashrabsn01  14422  hashrabsn1  14423  hash1snb  14468  hash1n0  14470  hashf1lem2  14505  hash2prde  14519  hash2prd  14524  hash2pwpr  14525  hashle2pr  14526  hashle2prv  14527  hashge2el2dif  14529  hashge2el2difr  14530  hash3tpde  14542  fundmge2nop0  14551  ffz0iswrd  14589  ccatrcl1  14642  pfxsuff1eqwrdeq  14747  wrdind  14770  wrd2ind  14771  swrdccatin1  14773  swrdccat3blem  14787  2cshwcshw  14874  cshwcsh2id  14877  cshimadifsn  14878  2swrd2eqwrdeq  15002  wwlktovf  15005  wwlktovfo  15007  s3sndisj  15016  s3iunsndisj  15017  relexpindlem  15112  rexico  15402  lo1le  15700  fsum2dlem  15818  ntrivcvg  15945  fprodss  15996  fprod2dlem  16028  0dvds  16325  mod2eq1n2dvds  16395  opoe  16411  omoe  16412  opeo  16413  omeo  16414  m1exp1  16424  nn0enne  16425  nn0o1gt2  16429  gcdneg  16568  dfgcd2  16593  algcvga  16626  eucalglt  16632  lcmf  16680  coprmdvds  16700  divgcdcoprmex  16713  cncongr1  16714  prm2orodd  16738  prm23lt5  16861  pockthi  16954  prmreclem5  16967  ramtcl2  17058  cshwrepswhash1  17150  f1ocpbl  17585  f1ovscpbl  17586  f1olecpbl  17587  monhom  17796  epihom  17803  inveq  17835  invcoisoid  17853  isocoinvid  17854  ciclcl  17863  cicrcl  17864  isinitoi  18066  istermoi  18067  2initoinv  18077  2termoinv  18084  setciso  18158  embedsetcestrclem  18226  ipopos  18606  mgmpropd  18689  gsumval2a  18723  ismnddef  18774  dfgrp2e  19003  symg2bas  19434  snsymgefmndeq  19436  symgvalstruct  19438  symgvalstructOLD  19439  symgfix2  19458  gsmsymgreq  19474  pmtrdifellem4  19521  mndodcongi  19585  pj1eu  19738  cycsubmcmn  19931  dprd2da  20086  rngimf1o  20480  rngimrnghm  20481  c0snmgmhm  20488  0ring01eq  20555  elrngchom  20646  rnghmsubcsetclem1  20653  rnghmsubcsetclem2  20654  rngcid  20657  rngcinv  20659  rngciso  20660  funcrngcsetcALT  20663  zrinitorngc  20664  zrtermorngc  20665  elringchom  20675  rhmsubcsetclem1  20682  rhmsubcsetclem2  20683  ringcid  20686  rhmsubcrngclem1  20688  rhmsubcrngclem2  20689  ringciso  20694  zrtermoringc  20697  rhmsubclem3  20709  rhmsubclem4  20710  lmodfopnelem1  20918  lspdisjb  21151  lspsnsubn0  21165  rngqiprngfulem2  21345  irinitoringc  21513  obs2ss  21772  mamufacex  22421  mat0dim0  22494  mat0dimid  22495  mat0dimscm  22496  dmatmat  22521  scmatmat  22536  mat1scmat  22566  1mavmul  22575  mavmulsolcl  22578  gsummatr01  22686  cpmatpmat  22737  cpmadugsumlemF  22903  tg2  22993  tgcl  22997  neii1  23135  neii2  23137  neindisj2  23152  perfopn  23214  ordtbas2  23220  pnfnei  23249  mnfnei  23250  llyidm  23517  txlm  23677  qtopuni  23731  tgqtop  23741  isfild  23887  snfil  23893  fbunfip  23898  fgss2  23903  fmco  23990  fbflim2  24006  cnpflf2  24029  fcfelbas  24065  fcfneii  24066  alexsubALTlem2  24077  alexsubALT  24080  tgpconncompeqg  24141  tsmscl  24164  tngngpim  24701  tgioo  24837  xrsmopn  24853  iccntr  24862  reconnlem2  24868  addcnlem  24905  htpycn  25024  phtpyhtpy  25033  pi1blem  25091  fgcfil  25324  ioombl1lem4  25615  dyadmbl  25654  itg2gt0  25815  ditgneg  25912  dvivthlem1  26067  coeeq2  26301  aannenlem2  26389  sineq0  26584  efif1o  26606  xrlimcnp  27029  vmacl  27179  efvmacl  27181  vmalelog  27267  dchrelbasd  27301  lgsqr  27413  lgsqrmodndvds  27415  gausslemma2dlem0i  27426  2lgslem2  27457  2lgs  27469  2lgsoddprmlem3  27476  2sqnn  27501  2sqreultlem  27509  2sqreultblem  27510  2sqreunnltlem  27512  2sqreunnltblem  27513  sltintdifex  27724  sltres  27725  nosepnelem  27742  nolt02o  27758  sltlend  27834  negsprop  28085  mulsprop  28174  n0subs  28378  elntg2  29018  uhgr0vb  29107  umgrupgr  29138  umgrnloopv  29141  umgredgprv  29142  umgrislfupgrlem  29157  umgredg  29173  uspgrushgr  29212  uspgrupgr  29213  usgruspgr  29215  usgredgprvALT  29230  usgrnloopvALT  29236  uhgr2edg  29243  edg0usgr  29288  egrsubgr  29312  0uhgrsubgr  29314  uhgrspansubgrlem  29325  nbuhgr  29378  cusgrsize2inds  29489  cusgrfilem2  29492  vtxdg0v  29509  1loopgrnb0  29538  vtxdginducedm1lem4  29578  wlkvtxeledg  29660  wlkeq  29670  wlkl1loop  29674  wlk1walk  29675  upgrwlkedg  29678  uspgr2wlkeq  29682  wlkv0  29687  wlkonl1iedg  29701  wlkon2n0  29702  wlkp1lem8  29716  wlkp1  29717  lfgrwlkprop  29723  lfgrwlknloop  29725  2pthnloop  29767  upgrwlkdvde  29773  spthonepeq  29788  uhgrwkspthlem2  29790  usgr2wlkneq  29792  usgr2trlncl  29796  usgr2trlspth  29797  pthdlem2lem  29803  clwlkcompbp  29818  uspgrn2crct  29841  wwlks  29868  wwlknbp  29875  0enwwlksnge1  29897  wwlkswwlksn  29898  wlklnwwlkln1  29901  wwlksnextproplem3  29944  wwlksnextprop  29945  wspthsnonn0vne  29950  wspn0  29957  2pthon3v  29976  umgr2adedgspth  29981  rusgr0edg  30006  clwwlkccat  30022  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2a4  30029  clwlkclwwlklem2  30032  clwlkclwwlkflem  30036  clwwlknp  30069  clwwlkwwlksb  30086  clwwlkext2edg  30088  erclwwlkneqlen  30100  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  clwwlknonwwlknonb  30138  upgr1wlkdlem1  30177  upgr3v3e3cycl  30212  uhgr3cyclexlem  30213  1conngr  30226  conngrv2edg  30227  eupth2lem3lem4  30263  eulercrct  30274  isfrgr  30292  frgr3vlem2  30306  1to2vfriswmgr  30311  1to3vfriswmgr  30312  frgrncvvdeqlem9  30339  frgrwopreg  30355  frgr2wwlkeqm  30363  2wspmdisj  30369  numclwwlk1lem2f  30387  frgrreggt1  30425  frgrregord013  30427  frgrregord13  30428  l2p  30511  nmlno0lem  30825  normgt0  31159  ocin  31328  nmlnop0iALT  32027  nmopun  32046  cvpss  32317  cvnbtwn  32318  atcvati  32418  mdsymlem6  32440  iunrnmptss  32588  expgt0b  32820  wrdt2ind  32920  irngssv  33688  issgon  34087  mbfmcnt  34233  ballotlemfc0  34457  ballotlemfcc  34458  satfv0  35326  satfv0fun  35339  fmla1  35355  gonarlem  35362  gonar  35363  goalrlem  35364  goalr  35365  fmla0disjsuc  35366  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  satfun  35379  satfv0fvfmla0  35381  sategoelfv  35388  mthmblem  35548  pprodss4v  35848  funpartfun  35907  funpartfv  35909  5segofs  35970  btwnxfr  36020  brofs2  36041  brifs2  36042  btwnconn1  36065  segleantisym  36079  broutsideof2  36086  outsidene1  36087  outsidene2  36088  funray  36104  lineunray  36111  cldbnd  36292  bj-imdirval3  37150  topdifinffinlem  37313  isbasisrelowllem1  37321  isbasisrelowllem2  37322  relowlpssretop  37330  inunissunidif  37341  pibt2  37383  matunitlindf  37578  poimir  37613  volsupnfl  37625  itg2addnclem  37631  cover2  37675  sdclem2  37702  fdc  37705  sstotbnd3  37736  heibor1  37770  clmgmOLD  37811  smgrpmgm  37824  smgrpassOLD  37825  dvrunz  37914  0rngo  37987  mopickr  38319  lsatcvat  39006  lshpkrex  39074  cmtbr3N  39210  atn0  39264  atnle  39273  cvlsupr4  39301  cvlsupr5  39302  cvlsupr6  39303  cvrval4N  39371  cvratlem  39378  2llnjN  39524  2lplnj  39577  linepsubN  39709  elpaddatiN  39762  elpcliN  39850  pclcmpatN  39858  ldilval  40070  ltrnu  40078  cdleme18d  40252  tendotp  40718  tendof  40720  tendovalco  40722  diatrl  41001  diaintclN  41015  dvheveccl  41069  dibintclN  41124  dihord6apre  41213  dihmeetlem1N  41247  dihpN  41293  dihintcl  41301  dochkrshp4  41346  oexpreposd  42309  pw2f1ocnv  42994  iocinico  43173  onsucf1olem  43232  succlg  43290  oacl2g  43292  omabs2  43294  omcl2  43295  naddcnfcom  43328  naddcnfass  43331  safesnsupfidom1o  43379  infordmin  43494  pr2cv  43510  expgrowthi  44302  iotavalsb  44402  bi23imp1  44466  ioogtlb  45413  iocgtlb  45420  iocleub  45421  icoltub  45426  iooltub  45428  stoweidlem31  45952  oppr  46945  funressnfv  46958  fsetsniunop  46964  fsetsnf1  46967  eu2ndop1stv  47040  afvelrnb0  47079  otiunsndisjX  47194  el1fzopredsuc  47240  2ffzoeq  47242  uniimaprimaeqfv  47256  elsetpreimafveqfv  47266  iccpartimp  47291  iccpartrn  47304  iccpartf  47305  iccpartnel  47312  fargshiftf  47314  fargshiftfo  47316  ichnfimlem  47337  ichnfim  47338  ichreuopeq  47347  sprel  47358  sprsymrelfvlem  47364  sprsymrelfolem2  47367  prproropf1olem4  47380  prprelb  47390  poprelb  47398  fmtnofac1  47444  prmdvdsfmtnof1lem2  47459  31prm  47471  lighneallem3  47481  nn0o1gt2ALTV  47568  nn0oALTV  47570  odd2prm2  47592  mogoldbblem  47594  fpprbasnn  47603  fpprnn  47604  sbgoldbaltlem1  47653  nnsum3primesle9  47668  bgoldbtbndlem1  47679  bgoldbtbndlem2  47680  grtriproplem  47790  grtriprop  47792  upwlkbprop  47861  clcllaw  47914  intop  47926  assintop  47932  assintopcllaw  47935  elrngchomALTV  47992  rngccatidALTV  47995  rngcinvALTV  47999  rngcisoALTV  48000  rhmsubcALTVlem3  48006  rhmsubcALTVlem4  48007  funcringcsetcALTV2lem7  48019  elringchomALTV  48026  ringccatidALTV  48029  ringcisoALTV  48034  funcringcsetclem7ALTV  48042  ztprmneprm  48072  suppmptcfin  48104  linccl  48143  linc1  48154  lincolss  48163  ldepspr  48202  nn0sumshdiglem1  48355  0aryfvalelfv  48369  rrxlines  48467  rrxsphere  48482  itsclc0yqsol  48498  itschlc0xyqsol1  48500  fdomne0  48563  f002  48567  fvconstr2  48571  fullthinc  48713