Theorem biimtrdi 256

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ax12i  1996  sb4a  2512  hbsb2  2514  dfsb2  2525  2eu2  2680  reu6  3689  nrmod  3845  2reu2  3852  disjel  4417  disjpss  4421  preq12b  4815  prneimg  4819  preqsnd  4824  elinti  4921  zfrepclf  5252  exnelv  5276  dtruALT2  5341  opth1g  5460  sbcop1  5470  snopeqop  5489  propeqop  5490  otsndisj  5502  otiunsndisj  5503  iunopeqop  5504  iunopeqopOLD  5505  po2ne  5585  soasym  5602  elreldm  5925  dfres3  5983  relcnvtrg  6268  relresfld  6277  elpredimg  6317  ordtr2  6406  ordssun  6465  funopg  6570  funimass2  6619  f0dom0  6762  elfv2ex  6924  fveqdmss  7073  eldmrexrnb  7087  fvcofneq  7088  funopsn  7144  funopsnOLD  7145  funopdmsn  7147  funsndifnop  7148  elunirn  7249  oprabidw  7441  oprabid  7442  brfvopab  7467  limuni3  7844  peano5  7886  resf1ext2b  7928  op1steq  8026  el2mpocsbcl  8076  bropopvvv  8081  bropfvvvv  8083  f1o2ndf1  8113  frxp  8118  fnwelem  8123  poxp2  8135  suppimacnv  8166  fvn0elsuppb  8173  suppfnss  8181  reldmtpos  8226  rntpos  8231  seqomlem2  8434  oaordi  8527  oa00  8540  oalimcl  8541  omeulem1  8563  nnaordi  8600  ecopovtrn  8814  undifixp  8928  mapdom2  9132  unxpdomlem3  9214  en1eqsn  9231  infssuni  9299  wdompwdom  9536  preleqg  9580  opthreg  9583  inf3lemd  9592  inf3lem2  9594  inf3lem6  9598  cnfcomlem  9664  cnfcom3  9669  karden  9877  carden2a  9948  alephdom  10061  dfac5lem4  10106  dfac12r  10126  kmlem2  10131  kmlem12  10141  cfslb2n  10247  alephsing  10255  fin23lem30  10321  fin1a2lem6  10384  fin1a2lem13  10391  axcc2lem  10415  domtriomlem  10421  axdc3lem2  10430  axdc4lem  10434  brdom6disj  10511  alephexp1  10559  pwfseq  10644  addnidpi  10881  indpi  10887  nqereu  10909  ltsonq  10949  distrlem5pr  11007  addcanpr  11026  suplem1pr  11032  suplem2pr  11033  ltsrpr  11057  ltsosr  11074  sqgt0sr  11086  leltne  11294  ltnsym  11303  ltlen  11306  eqlei  11315  eqlei2  11316  infm3  12169  nnunb  12495  0mnnnnn0  12531  elnnnn0b  12543  nn0ge2m1nn  12569  nn0le2is012  12655  btwnz  12694  uz11  12882  xrleltne  13165  xltnegi  13237  xnn0lenn0nn0  13266  xnn0xadd0  13268  xmulasslem2  13303  reltxrnmnf  13364  icogelb  13418  iccleub  13423  uznfz  13634  2ffzeq  13673  elfzonlteqm1  13766  elfzo0l  13781  fzoopth  13787  elfznelfzob  13799  elfzr  13806  elfzlmr  13807  injresinjlem  13815  injresinj  13816  fleqceilz  13883  modadd1  13937  modmul1  13956  modirr  13974  addmodlteq  13978  uzrdgfni  13990  fsuppmapnn0fiub0  14025  fsuppmapnn0ub  14027  seqf1o  14075  expnngt1  14273  hashrabsn01  14405  hashrabsn1  14406  hash1snb  14452  hash1n0  14454  hashf1lem2  14489  hash2prde  14503  hash2prd  14508  hash2pwpr  14509  hashle2pr  14510  hashle2prv  14511  hashge2el2dif  14513  hashge2el2difr  14514  hash3tpde  14526  fundmge2nop0  14535  ffz0iswrd  14574  ccatrcl1  14628  pfxsuff1eqwrdeq  14732  wrdind  14755  wrd2ind  14756  swrdccatin1  14758  swrdccat3blem  14772  2cshwcshw  14858  cshwcsh2id  14861  cshimadifsn  14862  2swrd2eqwrdeq  14986  wwlktovf  14989  wwlktovfo  14991  s3sndisj  15000  s3iunsndisj  15001  relexpindlem  15096  rexico  15401  lo1le  15699  fsum2dlem  15817  ntrivcvg  15947  fprodss  15998  fprod2dlem  16030  0dvds  16329  mod2eq1n2dvds  16400  opoe  16416  omoe  16417  opeo  16418  omeo  16419  m1exp1  16429  nn0enne  16430  nn0o1gt2  16434  gcdneg  16575  dfgcd2  16599  algcvga  16632  eucalglt  16638  lcmf  16686  coprmdvds  16706  divgcdcoprmex  16719  cncongr1  16720  prm2orodd  16744  prm23lt5  16869  pockthi  16962  prmreclem5  16975  ramtcl2  17066  cshwrepswhash1  17157  f1ocpbl  17574  f1ovscpbl  17575  f1olecpbl  17576  monhom  17787  epihom  17794  inveq  17826  invcoisoid  17844  isocoinvid  17845  ciclcl  17854  cicrcl  17855  isinitoi  18051  istermoi  18052  2initoinv  18062  2termoinv  18069  setciso  18143  embedsetcestrclem  18208  ipopos  18587  mgmpropd  18704  gsumval2a  18738  ismnddef  18789  dfgrp2e  19025  symg2bas  19458  snsymgefmndeq  19460  symgvalstruct  19462  symgfix2  19481  gsmsymgreq  19497  pmtrdifellem4  19544  mndodcongi  19608  pj1eu  19761  cycsubmcmn  19954  dprd2da  20109  rngimf1o  20532  rngimrnghm  20533  c0snmgmhm  20540  0ring01eq  20627  elrngchom  20723  rnghmsubcsetclem1  20730  rnghmsubcsetclem2  20731  rngcid  20734  rngcinv  20736  rngciso  20737  funcrngcsetcALT  20740  zrinitorngc  20741  zrtermorngc  20742  elringchom  20752  rhmsubcsetclem1  20759  rhmsubcsetclem2  20760  ringcid  20763  rhmsubcrngclem1  20765  rhmsubcrngclem2  20766  ringciso  20771  zrtermoringc  20774  rhmsubclem3  20786  rhmsubclem4  20787  lmodfopnelem1  21019  lspdisjb  21250  lspsnsubn0  21264  rngqiprngfulem2  21452  irinitoringc  21629  obs2ss  21879  mamufacex  22553  mat0dim0  22624  mat0dimid  22625  mat0dimscm  22626  dmatmat  22651  scmatmat  22666  mat1scmat  22696  1mavmul  22705  mavmulsolcl  22708  gsummatr01  22816  cpmatpmat  22867  cpmadugsumlemF  23033  tg2  23122  tgcl  23126  neii1  23263  neii2  23265  neindisj2  23280  perfopn  23342  ordtbas2  23348  pnfnei  23377  mnfnei  23378  llyidm  23645  txlm  23805  qtopuni  23859  tgqtop  23869  isfild  24015  snfil  24021  fbunfip  24026  fgss2  24031  fmco  24118  fbflim2  24134  cnpflf2  24157  fcfelbas  24193  fcfneii  24194  alexsubALTlem2  24205  alexsubALT  24208  tgpconncompeqg  24269  tsmscl  24292  tngngpim  24816  tgioo  24953  xrsmopn  24970  iccntr  24979  reconnlem2  24985  addcnlem  25022  htpycn  25132  phtpyhtpy  25141  pi1blem  25198  fgcfil  25430  ioombl1lem4  25720  dyadmbl  25759  itg2gt0  25919  ditgneg  26016  dvivthlem1  26167  coeeq2  26399  aannenlem2  26492  sineq0  26689  efif1o  26711  xrlimcnp  27133  vmacl  27282  efvmacl  27284  vmalelog  27369  dchrelbasd  27403  lgsqr  27515  lgsqrmodndvds  27517  gausslemma2dlem0i  27528  2lgslem2  27559  2lgs  27571  2lgsoddprmlem3  27578  2sqnn  27603  2sqreultlem  27611  2sqreultblem  27612  2sqreunnltlem  27614  2sqreunnltblem  27615  ltsintdifex  27825  ltsres  27826  nosepnelem  27843  nolt02o  27859  ltlesnd  27939  negsprop  28228  mulsprop  28323  onnolt  28459  onlts  28460  n0subs  28556  bdaypw2n0bndlem  28656  bdaypw2n0bnd  28657  bdayfinbndlem2  28661  elntg2  29335  uhgr0vb  29422  umgrupgr  29453  umgrnloopv  29456  umgredgprv  29457  umgrislfupgrlem  29472  umgredg  29488  uspgrushgr  29527  uspgrupgr  29528  usgruspgr  29530  usgredgprvALT  29545  usgrnloopvALT  29551  uhgr2edg  29558  edg0usgr  29603  egrsubgr  29627  0uhgrsubgr  29629  uhgrspansubgrlem  29640  nbuhgr  29693  cusgrsize2inds  29803  cusgrfilem2  29806  vtxdg0v  29823  1loopgrnb0  29852  vtxdginducedm1lem4  29892  wlkvtxeledg  29973  wlkeq  29983  wlkl1loop  29987  wlk1walk  29988  upgrwlkedg  29991  uspgr2wlkeq  29995  wlkv0  29999  wlkonl1iedg  30013  wlkon2n0  30014  wlkp1lem8  30028  wlkp1  30029  lfgrwlkprop  30035  lfgrwlknloop  30037  2pthnloop  30080  upgrwlkdvde  30086  spthonepeq  30101  uhgrwkspthlem2  30103  usgr2wlkneq  30105  usgr2trlncl  30109  usgr2trlspth  30110  pthdlem2lem  30116  clwlkcompbp  30131  uspgrn2crct  30157  wwlks  30184  wwlknbp  30191  0enwwlksnge1  30213  wwlkswwlksn  30214  wlklnwwlkln1  30217  wwlksnextproplem3  30260  wwlksnextprop  30261  wspthsnonn0vne  30266  wspn0  30273  2pthon3v  30292  umgr2adedgspth  30297  rusgr0edg  30325  clwwlkccat  30341  clwlkclwwlklem2fv2  30347  clwlkclwwlklem2a4  30348  clwlkclwwlklem2  30351  clwlkclwwlkflem  30355  clwwlknp  30388  clwwlkwwlksb  30405  clwwlkext2edg  30407  erclwwlkneqlen  30419  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  clwwlknonwwlknonb  30457  upgr1wlkdlem1  30496  upgr3v3e3cycl  30531  uhgr3cyclexlem  30532  1conngr  30545  conngrv2edg  30546  eupth2lem3lem4  30582  eulercrct  30593  isfrgr  30611  frgr3vlem2  30625  1to2vfriswmgr  30630  1to3vfriswmgr  30631  frgrncvvdeqlem9  30658  frgrwopreg  30674  frgr2wwlkeqm  30682  2wspmdisj  30688  numclwwlk1lem2f  30706  frgrreggt1  30744  frgrregord013  30746  frgrregord13  30747  l2p  30831  nmlno0lem  31145  normgt0  31479  ocin  31648  nmlnop0iALT  32347  nmopun  32366  cvpss  32637  cvnbtwn  32638  atcvati  32738  mdsymlem6  32760  iunrnmptss  32910  expgt0b  33161  wrdt2ind  33273  irngssv  34078  issgon  34513  mbfmcnt  34658  ballotlemfc0  34883  ballotlemfcc  34884  kardcard2b  35578  satfv0  35850  satfv0fun  35863  fmla1  35879  gonarlem  35886  gonar  35887  goalrlem  35888  goalr  35889  fmla0disjsuc  35890  satffunlem  35893  satffunlem1lem1  35894  satffunlem2lem1  35896  satfun  35903  satfv0fvfmla0  35905  sategoelfv  35912  mthmblem  36072  pprodss4v  36374  funpartfun  36435  funpartfv  36437  5segofs  36498  btwnxfr  36548  brofs2  36569  brifs2  36570  btwnconn1  36593  segleantisym  36607  broutsideof2  36614  outsidene1  36615  outsidene2  36616  funray  36632  lineunray  36639  cldbnd  36857  bj-imdirval3  37848  topdifinffinlem  38013  isbasisrelowllem1  38021  isbasisrelowllem2  38022  relowlpssretop  38030  inunissunidif  38041  pibt2  38083  matunitlindf  38289  poimir  38324  volsupnfl  38336  itg2addnclem  38342  cover2  38386  sdclem2  38413  fdc  38416  sstotbnd3  38447  heibor1  38481  clmgmOLD  38522  smgrpmgm  38535  smgrpassOLD  38536  dvrunz  38625  0rngo  38698  mopickr  39040  sucmapleftuniq  39159  lsatcvat  39844  lshpkrex  39912  cmtbr3N  40048  atn0  40102  atnle  40111  cvlsupr4  40139  cvlsupr5  40140  cvlsupr6  40141  cvrval4N  40208  cvratlem  40215  2llnjN  40361  2lplnj  40414  linepsubN  40546  elpaddatiN  40599  elpcliN  40687  pclcmpatN  40695  ldilval  40907  ltrnu  40915  cdleme18d  41089  tendotp  41555  tendof  41557  tendovalco  41559  diatrl  41838  diaintclN  41852  dvheveccl  41906  dibintclN  41961  dihord6apre  42050  dihmeetlem1N  42084  dihpN  42130  dihintcl  42138  dochkrshp4  42183  oexpreposd  43103  pw2f1ocnv  43784  iocinico  43959  onsucf1olem  44017  succlg  44075  oacl2g  44077  omabs2  44079  omcl2  44080  naddcnfcom  44113  naddcnfass  44116  safesnsupfidom1o  44163  infordmin  44278  pr2cv  44294  expgrowthi  45063  iotavalsb  45163  bi23imp1  45224  ioogtlb  46231  iocgtlb  46238  iocleub  46239  icoltub  46244  iooltub  46246  stoweidlem31  46765  oppr  47787  funressnfv  47800  fsetsniunop  47806  fsetsnf1  47809  eu2ndop1stv  47882  afvelrnb0  47921  otiunsndisjX  48036  el1fzopredsuc  48083  2ffzoeq  48085  uniimaprimaeqfv  48151  elsetpreimafveqfv  48161  iccpartimp  48186  iccpartrn  48199  iccpartf  48200  iccpartnel  48207  fargshiftf  48209  fargshiftfo  48211  ichnfimlem  48232  ichnfim  48233  ichreuopeq  48242  sprel  48253  sprsymrelfvlem  48259  sprsymrelfolem2  48262  prproropf1olem4  48275  prprelb  48285  poprelb  48293  fmtnofac1  48342  prmdvdsfmtnof1lem2  48357  31prm  48369  lighneallem3  48379  ppivalnnnprm  48400  nn0o1gt2ALTV  48479  nn0oALTV  48481  odd2prm2  48503  mogoldbblem  48505  fpprbasnn  48514  fpprnn  48515  sbgoldbaltlem1  48564  nnsum3primesle9  48579  bgoldbtbndlem1  48590  bgoldbtbndlem2  48591  elclnbgrelnbgr  48610  grimedgi  48721  grtriproplem  48724  grtriprop  48726  cycl3grtrilem  48731  cycl3grtri  48732  isubgr3stgrlem8  48758  gpgvtxel2  48833  gpgedgiov  48850  gpgedg2iv  48852  gpgprismgr4cycllem7  48886  pgnbgreunbgrlem1  48898  pgnbgreunbgrlem2lem1  48899  pgnbgreunbgrlem2lem2  48900  pgnbgreunbgrlem2lem3  48901  pgnbgreunbgrlem2  48902  pgnbgreunbgrlem4  48904  pgnbgreunbgrlem5  48908  upwlkbprop  48923  clcllaw  48976  intop  48988  assintop  48994  assintopcllaw  48997  elrngchomALTV  49054  rngccatidALTV  49057  rngcinvALTV  49061  rngcisoALTV  49062  rhmsubcALTVlem3  49068  rhmsubcALTVlem4  49069  funcringcsetcALTV2lem7  49081  elringchomALTV  49088  ringccatidALTV  49091  ringcisoALTV  49096  funcringcsetclem7ALTV  49104  prmringnzring  49122  ztprmneprm  49147  suppmptcfin  49176  linccl  49214  linc1  49225  lincolss  49234  ldepspr  49273  nn0sumshdiglem1  49421  0aryfvalelfv  49435  rrxlines  49533  rrxsphere  49548  itsclc0yqsol  49564  itschlc0xyqsol1  49566  fdomne0  49648  f002  49652  fvconstr2  49662  fullthinc  50248