Theorem biimtrdi 252

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 228	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  ax12i  1963  sb4a  2475  hbsb2  2477  dfsb2  2488  2eu2  2644  nfabdwOLD  2924  reu6  3721  2reu2  3891  sseq0  4400  disjel  4457  disjpss  4461  preq12b  4852  prneimg  4856  preqsnd  4860  elinti  4958  zfrepclf  5294  dtruALT2  5370  dtruOLD  5443  opth1g  5480  sbcop1  5490  snopeqop  5508  propeqop  5509  otsndisj  5521  otiunsndisj  5522  iunopeqop  5523  po2ne  5606  soasym  5621  elreldm  5937  dfres3  5990  relcnvtrg  6270  relresfld  6280  elpredimg  6320  ordtr2  6413  ordssun  6471  funopg  6587  funimass2  6636  f0dom0  6781  elfv2ex  6943  fveqdmss  7088  eldmrexrnb  7102  fvcofneq  7103  funopsn  7157  funopdmsn  7159  funsndifnop  7160  elunirn  7261  2f1fvneq  7270  oprabidw  7451  oprabid  7452  brfvopab  7477  limuni3  7856  peano5  7899  peano5OLD  7900  op1steq  8037  el2mpocsbcl  8090  bropopvvv  8095  bropfvvvv  8097  f1o2ndf1  8127  frxp  8131  fnwelem  8136  poxp2  8148  suppimacnv  8179  fvn0elsuppb  8186  suppfnss  8194  reldmtpos  8240  rntpos  8245  seqomlem2  8472  oaordi  8567  oa00  8580  oalimcl  8581  omeulem1  8603  nnaordi  8639  ecopovtrn  8839  undifixp  8953  mapdom2  9173  unxpdomlem3  9277  en1eqsn  9299  enp1iOLD  9305  findcard2OLD  9309  infssuni  9368  wdompwdom  9602  preleqg  9639  opthreg  9642  inf3lemd  9651  inf3lem2  9653  inf3lem6  9657  cnfcomlem  9723  cnfcom3  9728  karden  9919  carden2a  9990  alephdom  10105  dfac5lem4  10150  dfac12r  10170  kmlem2  10175  kmlem12  10185  cfslb2n  10292  alephsing  10300  fin23lem30  10366  fin1a2lem6  10429  fin1a2lem13  10436  axcc2lem  10460  domtriomlem  10466  axdc3lem2  10475  axdc4lem  10479  brdom6disj  10556  alephexp1  10603  pwfseq  10688  addnidpi  10925  indpi  10931  nqereu  10953  ltsonq  10993  distrlem5pr  11051  addcanpr  11070  suplem1pr  11076  suplem2pr  11077  ltsrpr  11101  ltsosr  11118  sqgt0sr  11130  leltne  11334  ltnsym  11343  ltlen  11346  eqlei  11355  eqlei2  11356  infm3  12204  nnunb  12499  0mnnnnn0  12535  elnnnn0b  12547  nn0ge2m1nn  12572  nn0le2is012  12657  btwnz  12696  uz11  12878  xrleltne  13157  xltnegi  13228  xnn0lenn0nn0  13257  xnn0xadd0  13259  xmulasslem2  13294  reltxrnmnf  13354  icogelb  13408  iccleub  13412  uznfz  13617  2ffzeq  13655  elfzonlteqm1  13741  elfzo0l  13755  elfznelfzob  13771  elfzr  13778  elfzlmr  13779  injresinjlem  13785  injresinj  13786  fleqceilz  13852  modadd1  13906  modmul1  13922  modirr  13940  addmodlteq  13944  uzrdgfni  13956  fsuppmapnn0fiub0  13991  fsuppmapnn0ub  13993  seqf1o  14041  expnngt1  14236  hashrabsn01  14365  hashrabsn1  14366  hash1snb  14411  hash1n0  14413  hashf1lem2  14450  hash2prde  14464  hash2prd  14469  hash2pwpr  14470  hashle2pr  14471  hashle2prv  14472  hashge2el2dif  14474  hashge2el2difr  14475  fundmge2nop0  14486  ffz0iswrd  14524  ccatrcl1  14577  pfxsuff1eqwrdeq  14682  wrdind  14705  wrd2ind  14706  swrdccatin1  14708  swrdccat3blem  14722  2cshwcshw  14809  cshwcsh2id  14812  cshimadifsn  14813  2swrd2eqwrdeq  14937  wwlktovf  14940  wwlktovfo  14942  s3sndisj  14947  s3iunsndisj  14948  relexpindlem  15043  rexico  15333  lo1le  15631  fsum2dlem  15749  ntrivcvg  15876  fprodss  15925  fprod2dlem  15957  0dvds  16254  mod2eq1n2dvds  16324  opoe  16340  omoe  16341  opeo  16342  omeo  16343  m1exp1  16353  nn0enne  16354  nn0o1gt2  16358  gcdneg  16497  dfgcd2  16522  algcvga  16550  eucalglt  16556  lcmf  16604  coprmdvds  16624  divgcdcoprmex  16637  cncongr1  16638  prm2orodd  16662  prm23lt5  16783  pockthi  16876  prmreclem5  16889  ramtcl2  16980  cshwrepswhash1  17072  f1ocpbl  17507  f1ovscpbl  17508  f1olecpbl  17509  monhom  17718  epihom  17725  inveq  17757  invcoisoid  17775  isocoinvid  17776  ciclcl  17785  cicrcl  17786  isinitoi  17988  istermoi  17989  2initoinv  17999  2termoinv  18006  setciso  18080  embedsetcestrclem  18148  ipopos  18528  mgmpropd  18611  gsumval2a  18645  ismnddef  18696  dfgrp2e  18920  symg2bas  19347  snsymgefmndeq  19349  symgvalstruct  19351  symgvalstructOLD  19352  symgfix2  19371  gsmsymgreq  19387  pmtrdifellem4  19434  mndodcongi  19498  pj1eu  19651  cycsubmcmn  19844  dprd2da  19999  rngimf1o  20393  rngimrnghm  20394  c0snmgmhm  20401  0ring01eq  20466  elrngchom  20557  rnghmsubcsetclem1  20564  rnghmsubcsetclem2  20565  rngcid  20568  rngcinv  20570  rngciso  20571  funcrngcsetcALT  20574  zrinitorngc  20575  zrtermorngc  20576  elringchom  20586  rhmsubcsetclem1  20593  rhmsubcsetclem2  20594  ringcid  20597  rhmsubcrngclem1  20599  rhmsubcrngclem2  20600  ringciso  20605  zrtermoringc  20608  rhmsubclem3  20620  rhmsubclem4  20621  lmodfopnelem1  20781  lspdisjb  21014  lspsnsubn0  21028  rngqiprngfulem2  21202  irinitoringc  21405  obs2ss  21663  psrbaglefiOLD  21866  mamufacex  22304  mat0dim0  22382  mat0dimid  22383  mat0dimscm  22384  dmatmat  22409  scmatmat  22424  mat1scmat  22454  1mavmul  22463  mavmulsolcl  22466  gsummatr01  22574  cpmatpmat  22625  cpmadugsumlemF  22791  tg2  22881  tgcl  22885  neii1  23023  neii2  23025  neindisj2  23040  perfopn  23102  ordtbas2  23108  pnfnei  23137  mnfnei  23138  llyidm  23405  txlm  23565  qtopuni  23619  tgqtop  23629  isfild  23775  snfil  23781  fbunfip  23786  fgss2  23791  fmco  23878  fbflim2  23894  cnpflf2  23917  fcfelbas  23953  fcfneii  23954  alexsubALTlem2  23965  alexsubALT  23968  tgpconncompeqg  24029  tsmscl  24052  tngngpim  24589  tgioo  24725  xrsmopn  24741  iccntr  24750  reconnlem2  24756  addcnlem  24793  htpycn  24912  phtpyhtpy  24921  pi1blem  24979  fgcfil  25212  ioombl1lem4  25503  dyadmbl  25542  itg2gt0  25703  ditgneg  25799  dvivthlem1  25954  coeeq2  26189  aannenlem2  26277  sineq0  26471  efif1o  26493  xrlimcnp  26913  vmacl  27063  efvmacl  27065  vmalelog  27151  dchrelbasd  27185  lgsqr  27297  lgsqrmodndvds  27299  gausslemma2dlem0i  27310  2lgslem2  27341  2lgs  27353  2lgsoddprmlem3  27360  2sqnn  27385  2sqreultlem  27393  2sqreultblem  27394  2sqreunnltlem  27396  2sqreunnltblem  27397  sltintdifex  27607  sltres  27608  nosepnelem  27625  nolt02o  27641  sltlend  27717  negsprop  27960  mulsprop  28043  elntg2  28809  uhgr0vb  28898  umgrupgr  28929  umgrnloopv  28932  umgredgprv  28933  umgrislfupgrlem  28948  umgredg  28964  uspgrushgr  29003  uspgrupgr  29004  usgruspgr  29006  usgredgprvALT  29021  usgrnloopvALT  29027  uhgr2edg  29034  edg0usgr  29079  egrsubgr  29103  0uhgrsubgr  29105  uhgrspansubgrlem  29116  nbuhgr  29169  cusgrsize2inds  29280  cusgrfilem2  29283  vtxdg0v  29300  1loopgrnb0  29329  vtxdginducedm1lem4  29369  wlkvtxeledg  29451  wlkeq  29461  wlkl1loop  29465  wlk1walk  29466  upgrwlkedg  29469  uspgr2wlkeq  29473  wlkv0  29478  wlkonl1iedg  29492  wlkon2n0  29493  wlkp1lem8  29507  wlkp1  29508  lfgrwlkprop  29514  lfgrwlknloop  29516  2pthnloop  29558  upgrwlkdvde  29564  spthonepeq  29579  uhgrwkspthlem2  29581  usgr2wlkneq  29583  usgr2trlncl  29587  usgr2trlspth  29588  pthdlem2lem  29594  clwlkcompbp  29609  uspgrn2crct  29632  wwlks  29659  wwlknbp  29666  0enwwlksnge1  29688  wwlkswwlksn  29689  wlklnwwlkln1  29692  wwlksnextproplem3  29735  wwlksnextprop  29736  wspthsnonn0vne  29741  wspn0  29748  2pthon3v  29767  umgr2adedgspth  29772  rusgr0edg  29797  clwwlkccat  29813  clwlkclwwlklem2fv2  29819  clwlkclwwlklem2a4  29820  clwlkclwwlklem2  29823  clwlkclwwlkflem  29827  clwwlknp  29860  clwwlkwwlksb  29877  clwwlkext2edg  29879  erclwwlkneqlen  29891  hashecclwwlkn1  29900  umgrhashecclwwlk  29901  clwwlknonwwlknonb  29929  upgr1wlkdlem1  29968  upgr3v3e3cycl  30003  uhgr3cyclexlem  30004  1conngr  30017  conngrv2edg  30018  eupth2lem3lem4  30054  eulercrct  30065  isfrgr  30083  frgr3vlem2  30097  1to2vfriswmgr  30102  1to3vfriswmgr  30103  frgrncvvdeqlem9  30130  frgrwopreg  30146  frgr2wwlkeqm  30154  2wspmdisj  30160  numclwwlk1lem2f  30178  frgrreggt1  30216  frgrregord013  30218  frgrregord13  30219  l2p  30302  nmlno0lem  30616  normgt0  30950  ocin  31119  nmlnop0iALT  31818  nmopun  31837  cvpss  32108  cvnbtwn  32109  atcvati  32209  mdsymlem6  32231  iunrnmptss  32369  wrdt2ind  32687  irngssv  33366  issgon  33742  mbfmcnt  33888  ballotlemfc0  34112  ballotlemfcc  34113  satfv0  34968  satfv0fun  34981  fmla1  34997  gonarlem  35004  gonar  35005  goalrlem  35006  goalr  35007  fmla0disjsuc  35008  satffunlem  35011  satffunlem1lem1  35012  satffunlem2lem1  35014  satfun  35021  satfv0fvfmla0  35023  sategoelfv  35030  mthmblem  35190  pprodss4v  35480  funpartfun  35539  funpartfv  35541  5segofs  35602  btwnxfr  35652  brofs2  35673  brifs2  35674  btwnconn1  35697  segleantisym  35711  broutsideof2  35718  outsidene1  35719  outsidene2  35720  funray  35736  lineunray  35743  cldbnd  35810  bj-imdirval3  36663  topdifinffinlem  36826  isbasisrelowllem1  36834  isbasisrelowllem2  36835  relowlpssretop  36843  inunissunidif  36854  pibt2  36896  matunitlindf  37091  poimir  37126  volsupnfl  37138  itg2addnclem  37144  cover2  37188  sdclem2  37215  fdc  37218  sstotbnd3  37249  heibor1  37283  clmgmOLD  37324  smgrpmgm  37337  smgrpassOLD  37338  dvrunz  37427  0rngo  37500  mopickr  37835  lsatcvat  38522  lshpkrex  38590  cmtbr3N  38726  atn0  38780  atnle  38789  cvlsupr4  38817  cvlsupr5  38818  cvlsupr6  38819  cvrval4N  38887  cvratlem  38894  2llnjN  39040  2lplnj  39093  linepsubN  39225  elpaddatiN  39278  elpcliN  39366  pclcmpatN  39374  ldilval  39586  ltrnu  39594  cdleme18d  39768  tendotp  40234  tendof  40236  tendovalco  40238  diatrl  40517  diaintclN  40531  dvheveccl  40585  dibintclN  40640  dihord6apre  40729  dihmeetlem1N  40763  dihpN  40809  dihintcl  40817  dochkrshp4  40862  oexpreposd  41881  pw2f1ocnv  42458  iocinico  42640  onsucf1olem  42699  succlg  42757  oacl2g  42759  omabs2  42761  omcl2  42762  naddcnfcom  42795  naddcnfass  42798  safesnsupfidom1o  42847  infordmin  42962  pr2cv  42978  expgrowthi  43770  iotavalsb  43870  bi23imp1  43934  ioogtlb  44880  iocgtlb  44887  iocleub  44888  icoltub  44893  iooltub  44895  stoweidlem31  45419  oppr  46412  funressnfv  46425  fsetsniunop  46431  fsetsnf1  46434  eu2ndop1stv  46505  afvelrnb0  46544  otiunsndisjX  46659  el1fzopredsuc  46705  fzoopth  46707  2ffzoeq  46708  uniimaprimaeqfv  46722  elsetpreimafveqfv  46732  iccpartimp  46757  iccpartrn  46770  iccpartf  46771  iccpartnel  46778  fargshiftf  46780  fargshiftfo  46782  ichnfimlem  46803  ichnfim  46804  ichreuopeq  46813  sprel  46824  sprsymrelfvlem  46830  sprsymrelfolem2  46833  prproropf1olem4  46846  prprelb  46856  poprelb  46864  fmtnofac1  46910  prmdvdsfmtnof1lem2  46925  31prm  46937  lighneallem3  46947  nn0o1gt2ALTV  47034  nn0oALTV  47036  odd2prm2  47058  mogoldbblem  47060  fpprbasnn  47069