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  1963  sb4a  2482  hbsb2  2484  dfsb2  2495  2eu2  2650  reu6  3734  2reu2  3906  sseq0  4408  disjel  4462  disjpss  4466  preq12b  4854  prneimg  4858  preqsnd  4863  elinti  4959  zfrepclf  5296  dtruALT2  5375  dtruOLD  5451  opth1g  5488  sbcop1  5498  snopeqop  5515  propeqop  5516  otsndisj  5528  otiunsndisj  5529  iunopeqop  5530  po2ne  5612  soasym  5628  elreldm  5948  dfres3  6004  relcnvtrg  6287  relresfld  6297  elpredimg  6337  ordtr2  6429  ordssun  6487  funopg  6601  funimass2  6650  f0dom0  6792  elfv2ex  6952  fveqdmss  7097  eldmrexrnb  7111  fvcofneq  7112  funopsn  7167  funopdmsn  7169  funsndifnop  7170  elunirn  7270  2f1fvneq  7279  oprabidw  7461  oprabid  7462  brfvopab  7489  limuni3  7872  peano5  7915  op1steq  8056  el2mpocsbcl  8108  bropopvvv  8113  bropfvvvv  8115  f1o2ndf1  8145  frxp  8149  fnwelem  8154  poxp2  8166  suppimacnv  8197  fvn0elsuppb  8204  suppfnss  8212  reldmtpos  8257  rntpos  8262  seqomlem2  8489  oaordi  8582  oa00  8595  oalimcl  8596  omeulem1  8618  nnaordi  8654  ecopovtrn  8858  undifixp  8972  mapdom2  9186  unxpdomlem3  9285  en1eqsn  9305  enp1iOLD  9311  infssuni  9383  wdompwdom  9615  preleqg  9652  opthreg  9655  inf3lemd  9664  inf3lem2  9666  inf3lem6  9670  cnfcomlem  9736  cnfcom3  9741  karden  9932  carden2a  10003  alephdom  10118  dfac5lem4  10163  dfac5lem4OLD  10165  dfac12r  10184  kmlem2  10189  kmlem12  10199  cfslb2n  10305  alephsing  10313  fin23lem30  10379  fin1a2lem6  10442  fin1a2lem13  10449  axcc2lem  10473  domtriomlem  10479  axdc3lem2  10488  axdc4lem  10492  brdom6disj  10569  alephexp1  10616  pwfseq  10701  addnidpi  10938  indpi  10944  nqereu  10966  ltsonq  11006  distrlem5pr  11064  addcanpr  11083  suplem1pr  11089  suplem2pr  11090  ltsrpr  11114  ltsosr  11131  sqgt0sr  11143  leltne  11347  ltnsym  11356  ltlen  11359  eqlei  11368  eqlei2  11369  infm3  12224  nnunb  12519  0mnnnnn0  12555  elnnnn0b  12567  nn0ge2m1nn  12593  nn0le2is012  12679  btwnz  12718  uz11  12900  xrleltne  13183  xltnegi  13254  xnn0lenn0nn0  13283  xnn0xadd0  13285  xmulasslem2  13320  reltxrnmnf  13380  icogelb  13434  iccleub  13438  uznfz  13646  2ffzeq  13685  elfzonlteqm1  13776  elfzo0l  13791  fzoopth  13797  elfznelfzob  13808  elfzr  13815  elfzlmr  13816  injresinjlem  13822  injresinj  13823  fleqceilz  13890  modadd1  13944  modmul1  13961  modirr  13979  addmodlteq  13983  uzrdgfni  13995  fsuppmapnn0fiub0  14030  fsuppmapnn0ub  14032  seqf1o  14080  expnngt1  14276  hashrabsn01  14408  hashrabsn1  14409  hash1snb  14454  hash1n0  14456  hashf1lem2  14491  hash2prde  14505  hash2prd  14510  hash2pwpr  14511  hashle2pr  14512  hashle2prv  14513  hashge2el2dif  14515  hashge2el2difr  14516  hash3tpde  14528  fundmge2nop0  14537  ffz0iswrd  14575  ccatrcl1  14628  pfxsuff1eqwrdeq  14733  wrdind  14756  wrd2ind  14757  swrdccatin1  14759  swrdccat3blem  14773  2cshwcshw  14860  cshwcsh2id  14863  cshimadifsn  14864  2swrd2eqwrdeq  14988  wwlktovf  14991  wwlktovfo  14993  s3sndisj  15002  s3iunsndisj  15003  relexpindlem  15098  rexico  15388  lo1le  15684  fsum2dlem  15802  ntrivcvg  15929  fprodss  15980  fprod2dlem  16012  0dvds  16310  mod2eq1n2dvds  16380  opoe  16396  omoe  16397  opeo  16398  omeo  16399  m1exp1  16409  nn0enne  16410  nn0o1gt2  16414  gcdneg  16555  dfgcd2  16579  algcvga  16612  eucalglt  16618  lcmf  16666  coprmdvds  16686  divgcdcoprmex  16699  cncongr1  16700  prm2orodd  16724  prm23lt5  16847  pockthi  16940  prmreclem5  16953  ramtcl2  17044  cshwrepswhash1  17136  f1ocpbl  17571  f1ovscpbl  17572  f1olecpbl  17573  monhom  17782  epihom  17789  inveq  17821  invcoisoid  17839  isocoinvid  17840  ciclcl  17849  cicrcl  17850  isinitoi  18052  istermoi  18053  2initoinv  18063  2termoinv  18070  setciso  18144  embedsetcestrclem  18212  ipopos  18593  mgmpropd  18676  gsumval2a  18710  ismnddef  18761  dfgrp2e  18993  symg2bas  19424  snsymgefmndeq  19426  symgvalstruct  19428  symgvalstructOLD  19429  symgfix2  19448  gsmsymgreq  19464  pmtrdifellem4  19511  mndodcongi  19575  pj1eu  19728  cycsubmcmn  19921  dprd2da  20076  rngimf1o  20470  rngimrnghm  20471  c0snmgmhm  20478  0ring01eq  20545  elrngchom  20640  rnghmsubcsetclem1  20647  rnghmsubcsetclem2  20648  rngcid  20651  rngcinv  20653  rngciso  20654  funcrngcsetcALT  20657  zrinitorngc  20658  zrtermorngc  20659  elringchom  20669  rhmsubcsetclem1  20676  rhmsubcsetclem2  20677  ringcid  20680  rhmsubcrngclem1  20682  rhmsubcrngclem2  20683  ringciso  20688  zrtermoringc  20691  rhmsubclem3  20703  rhmsubclem4  20704  lmodfopnelem1  20912  lspdisjb  21145  lspsnsubn0  21159  rngqiprngfulem2  21339  irinitoringc  21507  obs2ss  21766  mamufacex  22415  mat0dim0  22488  mat0dimid  22489  mat0dimscm  22490  dmatmat  22515  scmatmat  22530  mat1scmat  22560  1mavmul  22569  mavmulsolcl  22572  gsummatr01  22680  cpmatpmat  22731  cpmadugsumlemF  22897  tg2  22987  tgcl  22991  neii1  23129  neii2  23131  neindisj2  23146  perfopn  23208  ordtbas2  23214  pnfnei  23243  mnfnei  23244  llyidm  23511  txlm  23671  qtopuni  23725  tgqtop  23735  isfild  23881  snfil  23887  fbunfip  23892  fgss2  23897  fmco  23984  fbflim2  24000  cnpflf2  24023  fcfelbas  24059  fcfneii  24060  alexsubALTlem2  24071  alexsubALT  24074  tgpconncompeqg  24135  tsmscl  24158  tngngpim  24695  tgioo  24831  xrsmopn  24847  iccntr  24856  reconnlem2  24862  addcnlem  24899  htpycn  25018  phtpyhtpy  25027  pi1blem  25085  fgcfil  25318  ioombl1lem4  25609  dyadmbl  25648  itg2gt0  25809  ditgneg  25906  dvivthlem1  26061  coeeq2  26295  aannenlem2  26385  sineq0  26580  efif1o  26602  xrlimcnp  27025  vmacl  27175  efvmacl  27177  vmalelog  27263  dchrelbasd  27297  lgsqr  27409  lgsqrmodndvds  27411  gausslemma2dlem0i  27422  2lgslem2  27453  2lgs  27465  2lgsoddprmlem3  27472  2sqnn  27497  2sqreultlem  27505  2sqreultblem  27506  2sqreunnltlem  27508  2sqreunnltblem  27509  sltintdifex  27720  sltres  27721  nosepnelem  27738  nolt02o  27754  sltlend  27830  negsprop  28081  mulsprop  28170  n0subs  28374  elntg2  29014  uhgr0vb  29103  umgrupgr  29134  umgrnloopv  29137  umgredgprv  29138  umgrislfupgrlem  29153  umgredg  29169  uspgrushgr  29208  uspgrupgr  29209  usgruspgr  29211  usgredgprvALT  29226  usgrnloopvALT  29232  uhgr2edg  29239  edg0usgr  29284  egrsubgr  29308  0uhgrsubgr  29310  uhgrspansubgrlem  29321  nbuhgr  29374  cusgrsize2inds  29485  cusgrfilem2  29488  vtxdg0v  29505  1loopgrnb0  29534  vtxdginducedm1lem4  29574  wlkvtxeledg  29656  wlkeq  29666  wlkl1loop  29670  wlk1walk  29671  upgrwlkedg  29674  uspgr2wlkeq  29678  wlkv0  29683  wlkonl1iedg  29697  wlkon2n0  29698  wlkp1lem8  29712  wlkp1  29713  lfgrwlkprop  29719  lfgrwlknloop  29721  2pthnloop  29763  upgrwlkdvde  29769  spthonepeq  29784  uhgrwkspthlem2  29786  usgr2wlkneq  29788  usgr2trlncl  29792  usgr2trlspth  29793  pthdlem2lem  29799  clwlkcompbp  29814  uspgrn2crct  29837  wwlks  29864  wwlknbp  29871  0enwwlksnge1  29893  wwlkswwlksn  29894  wlklnwwlkln1  29897  wwlksnextproplem3  29940  wwlksnextprop  29941  wspthsnonn0vne  29946  wspn0  29953  2pthon3v  29972  umgr2adedgspth  29977  rusgr0edg  30002  clwwlkccat  30018  clwlkclwwlklem2fv2  30024  clwlkclwwlklem2a4  30025  clwlkclwwlklem2  30028  clwlkclwwlkflem  30032  clwwlknp  30065  clwwlkwwlksb  30082  clwwlkext2edg  30084  erclwwlkneqlen  30096  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  clwwlknonwwlknonb  30134  upgr1wlkdlem1  30173  upgr3v3e3cycl  30208  uhgr3cyclexlem  30209  1conngr  30222  conngrv2edg  30223  eupth2lem3lem4  30259  eulercrct  30270  isfrgr  30288  frgr3vlem2  30302  1to2vfriswmgr  30307  1to3vfriswmgr  30308  frgrncvvdeqlem9  30335  frgrwopreg  30351  frgr2wwlkeqm  30359  2wspmdisj  30365  numclwwlk1lem2f  30383  frgrreggt1  30421  frgrregord013  30423  frgrregord13  30424  l2p  30507  nmlno0lem  30821  normgt0  31155  ocin  31324  nmlnop0iALT  32023  nmopun  32042  cvpss  32313  cvnbtwn  32314  atcvati  32414  mdsymlem6  32436  iunrnmptss  32585  expgt0b  32822  wrdt2ind  32922  irngssv  33702  issgon  34103  mbfmcnt  34249  ballotlemfc0  34473  ballotlemfcc  34474  satfv0  35342  satfv0fun  35355  fmla1  35371  gonarlem  35378  gonar  35379  goalrlem  35380  goalr  35381  fmla0disjsuc  35382  satffunlem  35385  satffunlem1lem1  35386  satffunlem2lem1  35388  satfun  35395  satfv0fvfmla0  35397  sategoelfv  35404  mthmblem  35564  pprodss4v  35865  funpartfun  35924  funpartfv  35926  5segofs  35987  btwnxfr  36037  brofs2  36058  brifs2  36059  btwnconn1  36082  segleantisym  36096  broutsideof2  36103  outsidene1  36104  outsidene2  36105  funray  36121  lineunray  36128  cldbnd  36308  bj-imdirval3  37166  topdifinffinlem  37329  isbasisrelowllem1  37337  isbasisrelowllem2  37338  relowlpssretop  37346  inunissunidif  37357  pibt2  37399  matunitlindf  37604  poimir  37639  volsupnfl  37651  itg2addnclem  37657  cover2  37701  sdclem2  37728  fdc  37731  sstotbnd3  37762  heibor1  37796  clmgmOLD  37837  smgrpmgm  37850  smgrpassOLD  37851  dvrunz  37940  0rngo  38013  mopickr  38344  lsatcvat  39031  lshpkrex  39099  cmtbr3N  39235  atn0  39289  atnle  39298  cvlsupr4  39326  cvlsupr5  39327  cvlsupr6  39328  cvrval4N  39396  cvratlem  39403  2llnjN  39549  2lplnj  39602  linepsubN  39734  elpaddatiN  39787  elpcliN  39875  pclcmpatN  39883  ldilval  40095  ltrnu  40103  cdleme18d  40277  tendotp  40743  tendof  40745  tendovalco  40747  diatrl  41026  diaintclN  41040  dvheveccl  41094  dibintclN  41149  dihord6apre  41238  dihmeetlem1N  41272  dihpN  41318  dihintcl  41326  dochkrshp4  41371  oexpreposd  42335  pw2f1ocnv  43025  iocinico  43200  onsucf1olem  43259  succlg  43317  oacl2g  43319  omabs2  43321  omcl2  43322  naddcnfcom  43355  naddcnfass  43358  safesnsupfidom1o  43406  infordmin  43521  pr2cv  43537  expgrowthi  44328  iotavalsb  44428  bi23imp1  44492  ioogtlb  45447  iocgtlb  45454  iocleub  45455  icoltub  45460  iooltub  45462  stoweidlem31  45986  oppr  46979  funressnfv  46992  fsetsniunop  46998  fsetsnf1  47001  eu2ndop1stv  47074  afvelrnb0  47113  otiunsndisjX  47228  el1fzopredsuc  47274  2ffzoeq  47276  uniimaprimaeqfv  47306  elsetpreimafveqfv  47316  iccpartimp  47341  iccpartrn  47354  iccpartf  47355  iccpartnel  47362  fargshiftf  47364  fargshiftfo  47366  ichnfimlem  47387  ichnfim  47388  ichreuopeq  47397  sprel  47408  sprsymrelfvlem  47414  sprsymrelfolem2  47417  prproropf1olem4  47430  prprelb  47440  poprelb  47448  fmtnofac1  47494  prmdvdsfmtnof1lem2  47509  31prm  47521  lighneallem3  47531  nn0o1gt2ALTV  47618  nn0oALTV  47620  odd2prm2  47642  mogoldbblem  47644  fpprbasnn  47653  fpprnn  47654  sbgoldbaltlem1  47703  nnsum3primesle9  47718  bgoldbtbndlem1  47729  bgoldbtbndlem2  47730  grtriproplem  47843  grtriprop  47845  isubgr3stgrlem8  47875  gpgvtxel2  47941  upwlkbprop  47981  clcllaw  48034  intop  48046  assintop  48052  assintopcllaw  48055  elrngchomALTV  48112  rngccatidALTV  48115  rngcinvALTV  48119  rngcisoALTV  48120  rhmsubcALTVlem3  48126  rhmsubcALTVlem4  48127  funcringcsetcALTV2lem7  48139  elringchomALTV  48146  ringccatidALTV  48149  ringcisoALTV  48154  funcringcsetclem7ALTV  48162  ztprmneprm  48191  suppmptcfin  48220  linccl  48259  linc1  48270  lincolss  48279  ldepspr  48318  nn0sumshdiglem1  48470  0aryfvalelfv  48484  rrxlines  48582  rrxsphere  48597  itsclc0yqsol  48613  itschlc0xyqsol1  48615  fdomne0  48679  f002  48683  fvconstr2  48687  fullthinc  48845