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  2478  hbsb2  2480  dfsb2  2491  2eu2  2646  reu6  3686  2reu2  3850  sseq0  4354  disjel  4408  disjpss  4412  preq12b  4801  prneimg  4805  preqsnd  4810  elinti  4905  zfrepclf  5230  dtruALT2  5309  opth1g  5421  sbcop1  5431  snopeqop  5449  propeqop  5450  otsndisj  5462  otiunsndisj  5463  iunopeqop  5464  po2ne  5543  soasym  5560  elreldm  5877  dfres3  5935  relcnvtrg  6215  relresfld  6224  elpredimg  6264  ordtr2  6352  ordssun  6411  funopg  6516  funimass2  6565  f1imadifssran  6568  f0dom0  6708  elfv2ex  6866  fveqdmss  7012  eldmrexrnb  7026  fvcofneq  7027  funopsn  7082  funopdmsn  7084  funsndifnop  7085  elunirn  7187  oprabidw  7380  oprabid  7381  brfvopab  7406  limuni3  7785  peano5  7826  resf1ext2b  7868  op1steq  7968  el2mpocsbcl  8018  bropopvvv  8023  bropfvvvv  8025  f1o2ndf1  8055  frxp  8059  fnwelem  8064  poxp2  8076  suppimacnv  8107  fvn0elsuppb  8114  suppfnss  8122  reldmtpos  8167  rntpos  8172  seqomlem2  8373  oaordi  8464  oa00  8477  oalimcl  8478  omeulem1  8500  nnaordi  8536  ecopovtrn  8747  undifixp  8861  mapdom2  9065  unxpdomlem3  9147  en1eqsn  9164  infssuni  9236  wdompwdom  9470  preleqg  9511  opthreg  9514  inf3lemd  9523  inf3lem2  9525  inf3lem6  9529  cnfcomlem  9595  cnfcom3  9600  karden  9791  carden2a  9862  alephdom  9975  dfac5lem4  10020  dfac5lem4OLD  10022  dfac12r  10041  kmlem2  10046  kmlem12  10056  cfslb2n  10162  alephsing  10170  fin23lem30  10236  fin1a2lem6  10299  fin1a2lem13  10306  axcc2lem  10330  domtriomlem  10336  axdc3lem2  10345  axdc4lem  10349  brdom6disj  10426  alephexp1  10473  pwfseq  10558  addnidpi  10795  indpi  10801  nqereu  10823  ltsonq  10863  distrlem5pr  10921  addcanpr  10940  suplem1pr  10946  suplem2pr  10947  ltsrpr  10971  ltsosr  10988  sqgt0sr  11000  leltne  11205  ltnsym  11214  ltlen  11217  eqlei  11226  eqlei2  11227  infm3  12084  nnunb  12380  0mnnnnn0  12416  elnnnn0b  12428  nn0ge2m1nn  12454  nn0le2is012  12540  btwnz  12579  uz11  12760  xrleltne  13047  xltnegi  13118  xnn0lenn0nn0  13147  xnn0xadd0  13149  xmulasslem2  13184  reltxrnmnf  13245  icogelb  13299  iccleub  13304  uznfz  13513  2ffzeq  13552  elfzonlteqm1  13644  elfzo0l  13659  fzoopth  13665  elfznelfzob  13676  elfzr  13683  elfzlmr  13684  injresinjlem  13690  injresinj  13691  fleqceilz  13758  modadd1  13812  modmul1  13831  modirr  13849  addmodlteq  13853  uzrdgfni  13865  fsuppmapnn0fiub0  13900  fsuppmapnn0ub  13902  seqf1o  13950  expnngt1  14148  hashrabsn01  14280  hashrabsn1  14281  hash1snb  14326  hash1n0  14328  hashf1lem2  14363  hash2prde  14377  hash2prd  14382  hash2pwpr  14383  hashle2pr  14384  hashle2prv  14385  hashge2el2dif  14387  hashge2el2difr  14388  hash3tpde  14400  fundmge2nop0  14409  ffz0iswrd  14448  ccatrcl1  14501  pfxsuff1eqwrdeq  14605  wrdind  14628  wrd2ind  14629  swrdccatin1  14631  swrdccat3blem  14645  2cshwcshw  14732  cshwcsh2id  14735  cshimadifsn  14736  2swrd2eqwrdeq  14860  wwlktovf  14863  wwlktovfo  14865  s3sndisj  14874  s3iunsndisj  14875  relexpindlem  14970  rexico  15261  lo1le  15559  fsum2dlem  15677  ntrivcvg  15804  fprodss  15855  fprod2dlem  15887  0dvds  16187  mod2eq1n2dvds  16258  opoe  16274  omoe  16275  opeo  16276  omeo  16277  m1exp1  16287  nn0enne  16288  nn0o1gt2  16292  gcdneg  16433  dfgcd2  16457  algcvga  16490  eucalglt  16496  lcmf  16544  coprmdvds  16564  divgcdcoprmex  16577  cncongr1  16578  prm2orodd  16602  prm23lt5  16726  pockthi  16819  prmreclem5  16832  ramtcl2  16923  cshwrepswhash1  17014  f1ocpbl  17429  f1ovscpbl  17430  f1olecpbl  17431  monhom  17642  epihom  17649  inveq  17681  invcoisoid  17699  isocoinvid  17700  ciclcl  17709  cicrcl  17710  isinitoi  17906  istermoi  17907  2initoinv  17917  2termoinv  17924  setciso  17998  embedsetcestrclem  18063  ipopos  18442  mgmpropd  18525  gsumval2a  18559  ismnddef  18610  dfgrp2e  18842  symg2bas  19272  snsymgefmndeq  19274  symgvalstruct  19276  symgfix2  19295  gsmsymgreq  19311  pmtrdifellem4  19358  mndodcongi  19422  pj1eu  19575  cycsubmcmn  19768  dprd2da  19923  rngimf1o  20339  rngimrnghm  20340  c0snmgmhm  20347  0ring01eq  20414  elrngchom  20509  rnghmsubcsetclem1  20516  rnghmsubcsetclem2  20517  rngcid  20520  rngcinv  20522  rngciso  20523  funcrngcsetcALT  20526  zrinitorngc  20527  zrtermorngc  20528  elringchom  20538  rhmsubcsetclem1  20545  rhmsubcsetclem2  20546  ringcid  20549  rhmsubcrngclem1  20551  rhmsubcrngclem2  20552  ringciso  20557  zrtermoringc  20560  rhmsubclem3  20572  rhmsubclem4  20573  lmodfopnelem1  20801  lspdisjb  21033  lspsnsubn0  21047  rngqiprngfulem2  21219  irinitoringc  21386  obs2ss  21636  mamufacex  22281  mat0dim0  22352  mat0dimid  22353  mat0dimscm  22354  dmatmat  22379  scmatmat  22394  mat1scmat  22424  1mavmul  22433  mavmulsolcl  22436  gsummatr01  22544  cpmatpmat  22595  cpmadugsumlemF  22761  tg2  22850  tgcl  22854  neii1  22991  neii2  22993  neindisj2  23008  perfopn  23070  ordtbas2  23076  pnfnei  23105  mnfnei  23106  llyidm  23373  txlm  23533  qtopuni  23587  tgqtop  23597  isfild  23743  snfil  23749  fbunfip  23754  fgss2  23759  fmco  23846  fbflim2  23862  cnpflf2  23885  fcfelbas  23921  fcfneii  23922  alexsubALTlem2  23933  alexsubALT  23936  tgpconncompeqg  23997  tsmscl  24020  tngngpim  24545  tgioo  24682  xrsmopn  24699  iccntr  24708  reconnlem2  24714  addcnlem  24751  htpycn  24870  phtpyhtpy  24879  pi1blem  24937  fgcfil  25169  ioombl1lem4  25460  dyadmbl  25499  itg2gt0  25659  ditgneg  25756  dvivthlem1  25911  coeeq2  26145  aannenlem2  26235  sineq0  26431  efif1o  26453  xrlimcnp  26876  vmacl  27026  efvmacl  27028  vmalelog  27114  dchrelbasd  27148  lgsqr  27260  lgsqrmodndvds  27262  gausslemma2dlem0i  27273  2lgslem2  27304  2lgs  27316  2lgsoddprmlem3  27323  2sqnn  27348  2sqreultlem  27356  2sqreultblem  27357  2sqreunnltlem  27359  2sqreunnltblem  27360  sltintdifex  27571  sltres  27572  nosepnelem  27589  nolt02o  27605  sltlend  27681  negsprop  27946  mulsprop  28038  onnolt  28172  onslt  28173  n0subs  28258  elntg2  28930  uhgr0vb  29017  umgrupgr  29048  umgrnloopv  29051  umgredgprv  29052  umgrislfupgrlem  29067  umgredg  29083  uspgrushgr  29122  uspgrupgr  29123  usgruspgr  29125  usgredgprvALT  29140  usgrnloopvALT  29146  uhgr2edg  29153  edg0usgr  29198  egrsubgr  29222  0uhgrsubgr  29224  uhgrspansubgrlem  29235  nbuhgr  29288  cusgrsize2inds  29399  cusgrfilem2  29402  vtxdg0v  29419  1loopgrnb0  29448  vtxdginducedm1lem4  29488  wlkvtxeledg  29569  wlkeq  29579  wlkl1loop  29583  wlk1walk  29584  upgrwlkedg  29587  uspgr2wlkeq  29591  wlkv0  29595  wlkonl1iedg  29609  wlkon2n0  29610  wlkp1lem8  29624  wlkp1  29625  lfgrwlkprop  29631  lfgrwlknloop  29633  2pthnloop  29676  upgrwlkdvde  29682  spthonepeq  29697  uhgrwkspthlem2  29699  usgr2wlkneq  29701  usgr2trlncl  29705  usgr2trlspth  29706  pthdlem2lem  29712  clwlkcompbp  29727  uspgrn2crct  29753  wwlks  29780  wwlknbp  29787  0enwwlksnge1  29809  wwlkswwlksn  29810  wlklnwwlkln1  29813  wwlksnextproplem3  29856  wwlksnextprop  29857  wspthsnonn0vne  29862  wspn0  29869  2pthon3v  29888  umgr2adedgspth  29893  rusgr0edg  29918  clwwlkccat  29934  clwlkclwwlklem2fv2  29940  clwlkclwwlklem2a4  29941  clwlkclwwlklem2  29944  clwlkclwwlkflem  29948  clwwlknp  29981  clwwlkwwlksb  29998  clwwlkext2edg  30000  erclwwlkneqlen  30012  hashecclwwlkn1  30021  umgrhashecclwwlk  30022  clwwlknonwwlknonb  30050  upgr1wlkdlem1  30089  upgr3v3e3cycl  30124  uhgr3cyclexlem  30125  1conngr  30138  conngrv2edg  30139  eupth2lem3lem4  30175  eulercrct  30186  isfrgr  30204  frgr3vlem2  30218  1to2vfriswmgr  30223  1to3vfriswmgr  30224  frgrncvvdeqlem9  30251  frgrwopreg  30267  frgr2wwlkeqm  30275  2wspmdisj  30281  numclwwlk1lem2f  30299  frgrreggt1  30337  frgrregord013  30339  frgrregord13  30340  l2p  30423  nmlno0lem  30737  normgt0  31071  ocin  31240  nmlnop0iALT  31939  nmopun  31958  cvpss  32229  cvnbtwn  32230  atcvati  32330  mdsymlem6  32352  iunrnmptss  32509  expgt0b  32761  wrdt2ind  32895  irngssv  33655  issgon  34090  mbfmcnt  34236  ballotlemfc0  34461  ballotlemfcc  34462  satfv0  35335  satfv0fun  35348  fmla1  35364  gonarlem  35371  gonar  35372  goalrlem  35373  goalr  35374  fmla0disjsuc  35375  satffunlem  35378  satffunlem1lem1  35379  satffunlem2lem1  35381  satfun  35388  satfv0fvfmla0  35390  sategoelfv  35397  mthmblem  35557  pprodss4v  35862  funpartfun  35921  funpartfv  35923  5segofs  35984  btwnxfr  36034  brofs2  36055  brifs2  36056  btwnconn1  36079  segleantisym  36093  broutsideof2  36100  outsidene1  36101  outsidene2  36102  funray  36118  lineunray  36125  cldbnd  36304  bj-imdirval3  37162  topdifinffinlem  37325  isbasisrelowllem1  37333  isbasisrelowllem2  37334  relowlpssretop  37342  inunissunidif  37353  pibt2  37395  matunitlindf  37602  poimir  37637  volsupnfl  37649  itg2addnclem  37655  cover2  37699  sdclem2  37726  fdc  37729  sstotbnd3  37760  heibor1  37794  clmgmOLD  37835  smgrpmgm  37848  smgrpassOLD  37849  dvrunz  37938  0rngo  38011  mopickr  38335  lsatcvat  39033  lshpkrex  39101  cmtbr3N  39237  atn0  39291  atnle  39300  cvlsupr4  39328  cvlsupr5  39329  cvlsupr6  39330  cvrval4N  39397  cvratlem  39404  2llnjN  39550  2lplnj  39603  linepsubN  39735  elpaddatiN  39788  elpcliN  39876  pclcmpatN  39884  ldilval  40096  ltrnu  40104  cdleme18d  40278  tendotp  40744  tendof  40746  tendovalco  40748  diatrl  41027  diaintclN  41041  dvheveccl  41095  dibintclN  41150  dihord6apre  41239  dihmeetlem1N  41273  dihpN  41319  dihintcl  41327  dochkrshp4  41372  oexpreposd  42299  pw2f1ocnv  43014  iocinico  43189  onsucf1olem  43247  succlg  43305  oacl2g  43307  omabs2  43309  omcl2  43310  naddcnfcom  43343  naddcnfass  43346  safesnsupfidom1o  43394  infordmin  43509  pr2cv  43525  expgrowthi  44310  iotavalsb  44410  bi23imp1  44473  ioogtlb  45480  iocgtlb  45487  iocleub  45488  icoltub  45493  iooltub  45495  stoweidlem31  46016  oppr  47018  funressnfv  47031  fsetsniunop  47037  fsetsnf1  47040  eu2ndop1stv  47113  afvelrnb0  47152  otiunsndisjX  47267  el1fzopredsuc  47313  2ffzoeq  47315  uniimaprimaeqfv  47370  elsetpreimafveqfv  47380  iccpartimp  47405  iccpartrn  47418  iccpartf  47419  iccpartnel  47426  fargshiftf  47428  fargshiftfo  47430  ichnfimlem  47451  ichnfim  47452  ichreuopeq  47461  sprel  47472  sprsymrelfvlem  47478  sprsymrelfolem2  47481  prproropf1olem4  47494  prprelb  47504  poprelb  47512  fmtnofac1  47558  prmdvdsfmtnof1lem2  47573  31prm  47585  lighneallem3  47595  nn0o1gt2ALTV  47682  nn0oALTV  47684  odd2prm2  47706  mogoldbblem  47708  fpprbasnn  47717  fpprnn  47718  sbgoldbaltlem1  47767  nnsum3primesle9  47782  bgoldbtbndlem1  47793  bgoldbtbndlem2  47794  grimedgi  47924  grtriproplem  47927  grtriprop  47929  cycl3grtrilem  47934  cycl3grtri  47935  isubgr3stgrlem8  47961  gpgvtxel2  48036  gpgedgiov  48053  gpgedg2iv  48055  gpgprismgr4cycllem7  48089  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem2lem1  48102  pgnbgreunbgrlem2lem2  48103  pgnbgreunbgrlem2lem3  48104  pgnbgreunbgrlem2  48105  pgnbgreunbgrlem4  48107  pgnbgreunbgrlem5  48111  upwlkbprop  48126  clcllaw  48179  intop  48191  assintop  48197  assintopcllaw  48200  elrngchomALTV  48257  rngccatidALTV  48260  rngcinvALTV  48264  rngcisoALTV  48265  rhmsubcALTVlem3  48271  rhmsubcALTVlem4  48272  funcringcsetcALTV2lem7  48284  elringchomALTV  48291  ringccatidALTV  48294  ringcisoALTV  48299  funcringcsetclem7ALTV  48307  ztprmneprm  48335  suppmptcfin  48364  linccl  48403  linc1  48414  lincolss  48423  ldepspr  48462  nn0sumshdiglem1  48610  0aryfvalelfv  48624  rrxlines  48722  rrxsphere  48737  itsclc0yqsol  48753  itschlc0xyqsol1  48755  fdomne0  48838  f002  48842  fvconstr2  48852  fullthinc  49439