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  1968  sb4a  2485  hbsb2  2487  dfsb2  2498  2eu2  2654  reu6  3673  2reu2  3837  sseq0  4344  disjel  4398  disjpss  4402  preq12b  4794  prneimg  4798  preqsnd  4803  elinti  4899  zfrepclf  5227  exnelv  5249  dtruALT2  5308  opth1g  5427  sbcop1  5437  snopeqop  5455  propeqop  5456  otsndisj  5468  otiunsndisj  5469  iunopeqop  5470  po2ne  5549  soasym  5566  elreldm  5885  dfres3  5944  relcnvtrg  6226  relresfld  6235  elpredimg  6275  ordtr2  6363  ordssun  6422  funopg  6527  funimass2  6576  f1imadifssran  6579  f0dom0  6719  elfv2ex  6878  fveqdmss  7025  eldmrexrnb  7039  fvcofneq  7040  funopsn  7096  funopdmsn  7098  funsndifnop  7099  elunirn  7200  oprabidw  7392  oprabid  7393  brfvopab  7418  limuni3  7797  peano5  7838  resf1ext2b  7880  op1steq  7980  el2mpocsbcl  8029  bropopvvv  8034  bropfvvvv  8036  f1o2ndf1  8066  frxp  8070  fnwelem  8075  poxp2  8087  suppimacnv  8118  fvn0elsuppb  8125  suppfnss  8133  reldmtpos  8178  rntpos  8183  seqomlem2  8384  oaordi  8475  oa00  8488  oalimcl  8489  omeulem1  8511  nnaordi  8548  ecopovtrn  8761  undifixp  8876  mapdom2  9080  unxpdomlem3  9162  en1eqsn  9179  infssuni  9250  wdompwdom  9487  preleqg  9530  opthreg  9533  inf3lemd  9542  inf3lem2  9544  inf3lem6  9548  cnfcomlem  9614  cnfcom3  9619  karden  9813  carden2a  9884  alephdom  9997  dfac5lem4  10042  dfac5lem4OLD  10044  dfac12r  10063  kmlem2  10068  kmlem12  10078  cfslb2n  10184  alephsing  10192  fin23lem30  10258  fin1a2lem6  10321  fin1a2lem13  10328  axcc2lem  10352  domtriomlem  10358  axdc3lem2  10367  axdc4lem  10371  brdom6disj  10448  alephexp1  10496  pwfseq  10581  addnidpi  10818  indpi  10824  nqereu  10846  ltsonq  10886  distrlem5pr  10944  addcanpr  10963  suplem1pr  10969  suplem2pr  10970  ltsrpr  10994  ltsosr  11011  sqgt0sr  11023  leltne  11229  ltnsym  11238  ltlen  11241  eqlei  11250  eqlei2  11251  infm3  12109  nnunb  12427  0mnnnnn0  12463  elnnnn0b  12475  nn0ge2m1nn  12501  nn0le2is012  12587  btwnz  12626  uz11  12807  xrleltne  13090  xltnegi  13162  xnn0lenn0nn0  13191  xnn0xadd0  13193  xmulasslem2  13228  reltxrnmnf  13289  icogelb  13343  iccleub  13348  uznfz  13558  2ffzeq  13597  elfzonlteqm1  13690  elfzo0l  13705  fzoopth  13711  elfznelfzob  13723  elfzr  13730  elfzlmr  13731  injresinjlem  13739  injresinj  13740  fleqceilz  13807  modadd1  13861  modmul1  13880  modirr  13898  addmodlteq  13902  uzrdgfni  13914  fsuppmapnn0fiub0  13949  fsuppmapnn0ub  13951  seqf1o  13999  expnngt1  14197  hashrabsn01  14329  hashrabsn1  14330  hash1snb  14375  hash1n0  14377  hashf1lem2  14412  hash2prde  14426  hash2prd  14431  hash2pwpr  14432  hashle2pr  14433  hashle2prv  14434  hashge2el2dif  14436  hashge2el2difr  14437  hash3tpde  14449  fundmge2nop0  14458  ffz0iswrd  14497  ccatrcl1  14551  pfxsuff1eqwrdeq  14655  wrdind  14678  wrd2ind  14679  swrdccatin1  14681  swrdccat3blem  14695  2cshwcshw  14781  cshwcsh2id  14784  cshimadifsn  14785  2swrd2eqwrdeq  14909  wwlktovf  14912  wwlktovfo  14914  s3sndisj  14923  s3iunsndisj  14924  relexpindlem  15019  rexico  15310  lo1le  15608  fsum2dlem  15726  ntrivcvg  15856  fprodss  15907  fprod2dlem  15939  0dvds  16239  mod2eq1n2dvds  16310  opoe  16326  omoe  16327  opeo  16328  omeo  16329  m1exp1  16339  nn0enne  16340  nn0o1gt2  16344  gcdneg  16485  dfgcd2  16509  algcvga  16542  eucalglt  16548  lcmf  16596  coprmdvds  16616  divgcdcoprmex  16629  cncongr1  16630  prm2orodd  16654  prm23lt5  16779  pockthi  16872  prmreclem5  16885  ramtcl2  16976  cshwrepswhash1  17067  f1ocpbl  17483  f1ovscpbl  17484  f1olecpbl  17485  monhom  17696  epihom  17703  inveq  17735  invcoisoid  17753  isocoinvid  17754  ciclcl  17763  cicrcl  17764  isinitoi  17960  istermoi  17961  2initoinv  17971  2termoinv  17978  setciso  18052  embedsetcestrclem  18117  ipopos  18496  mgmpropd  18613  gsumval2a  18647  ismnddef  18698  dfgrp2e  18933  symg2bas  19362  snsymgefmndeq  19364  symgvalstruct  19366  symgfix2  19385  gsmsymgreq  19401  pmtrdifellem4  19448  mndodcongi  19512  pj1eu  19665  cycsubmcmn  19858  dprd2da  20013  rngimf1o  20428  rngimrnghm  20429  c0snmgmhm  20436  0ring01eq  20500  elrngchom  20595  rnghmsubcsetclem1  20602  rnghmsubcsetclem2  20603  rngcid  20606  rngcinv  20608  rngciso  20609  funcrngcsetcALT  20612  zrinitorngc  20613  zrtermorngc  20614  elringchom  20624  rhmsubcsetclem1  20631  rhmsubcsetclem2  20632  ringcid  20635  rhmsubcrngclem1  20637  rhmsubcrngclem2  20638  ringciso  20643  zrtermoringc  20646  rhmsubclem3  20658  rhmsubclem4  20659  lmodfopnelem1  20887  lspdisjb  21119  lspsnsubn0  21133  rngqiprngfulem2  21305  irinitoringc  21472  obs2ss  21722  mamufacex  22374  mat0dim0  22445  mat0dimid  22446  mat0dimscm  22447  dmatmat  22472  scmatmat  22487  mat1scmat  22517  1mavmul  22526  mavmulsolcl  22529  gsummatr01  22637  cpmatpmat  22688  cpmadugsumlemF  22854  tg2  22943  tgcl  22947  neii1  23084  neii2  23086  neindisj2  23101  perfopn  23163  ordtbas2  23169  pnfnei  23198  mnfnei  23199  llyidm  23466  txlm  23626  qtopuni  23680  tgqtop  23690  isfild  23836  snfil  23842  fbunfip  23847  fgss2  23852  fmco  23939  fbflim2  23955  cnpflf2  23978  fcfelbas  24014  fcfneii  24015  alexsubALTlem2  24026  alexsubALT  24029  tgpconncompeqg  24090  tsmscl  24113  tngngpim  24637  tgioo  24774  xrsmopn  24791  iccntr  24800  reconnlem2  24806  addcnlem  24843  htpycn  24953  phtpyhtpy  24962  pi1blem  25019  fgcfil  25251  ioombl1lem4  25541  dyadmbl  25580  itg2gt0  25740  ditgneg  25837  dvivthlem1  25988  coeeq2  26220  aannenlem2  26309  sineq0  26504  efif1o  26526  xrlimcnp  26948  vmacl  27098  efvmacl  27100  vmalelog  27185  dchrelbasd  27219  lgsqr  27331  lgsqrmodndvds  27333  gausslemma2dlem0i  27344  2lgslem2  27375  2lgs  27387  2lgsoddprmlem3  27394  2sqnn  27419  2sqreultlem  27427  2sqreultblem  27428  2sqreunnltlem  27430  2sqreunnltblem  27431  ltsintdifex  27642  ltsres  27643  nosepnelem  27660  nolt02o  27676  ltlesnd  27756  negsprop  28044  mulsprop  28139  onnolt  28275  onlts  28276  n0subs  28372  bdaypw2n0bndlem  28472  bdaypw2n0bnd  28473  bdayfinbndlem2  28477  elntg2  29071  uhgr0vb  29158  umgrupgr  29189  umgrnloopv  29192  umgredgprv  29193  umgrislfupgrlem  29208  umgredg  29224  uspgrushgr  29263  uspgrupgr  29264  usgruspgr  29266  usgredgprvALT  29281  usgrnloopvALT  29287  uhgr2edg  29294  edg0usgr  29339  egrsubgr  29363  0uhgrsubgr  29365  uhgrspansubgrlem  29376  nbuhgr  29429  cusgrsize2inds  29540  cusgrfilem2  29543  vtxdg0v  29560  1loopgrnb0  29589  vtxdginducedm1lem4  29629  wlkvtxeledg  29710  wlkeq  29720  wlkl1loop  29724  wlk1walk  29725  upgrwlkedg  29728  uspgr2wlkeq  29732  wlkv0  29736  wlkonl1iedg  29750  wlkon2n0  29751  wlkp1lem8  29765  wlkp1  29766  lfgrwlkprop  29772  lfgrwlknloop  29774  2pthnloop  29817  upgrwlkdvde  29823  spthonepeq  29838  uhgrwkspthlem2  29840  usgr2wlkneq  29842  usgr2trlncl  29846  usgr2trlspth  29847  pthdlem2lem  29853  clwlkcompbp  29868  uspgrn2crct  29894  wwlks  29921  wwlknbp  29928  0enwwlksnge1  29950  wwlkswwlksn  29951  wlklnwwlkln1  29954  wwlksnextproplem3  29997  wwlksnextprop  29998  wspthsnonn0vne  30003  wspn0  30010  2pthon3v  30029  umgr2adedgspth  30034  rusgr0edg  30062  clwwlkccat  30078  clwlkclwwlklem2fv2  30084  clwlkclwwlklem2a4  30085  clwlkclwwlklem2  30088  clwlkclwwlkflem  30092  clwwlknp  30125  clwwlkwwlksb  30142  clwwlkext2edg  30144  erclwwlkneqlen  30156  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  clwwlknonwwlknonb  30194  upgr1wlkdlem1  30233  upgr3v3e3cycl  30268  uhgr3cyclexlem  30269  1conngr  30282  conngrv2edg  30283  eupth2lem3lem4  30319  eulercrct  30330  isfrgr  30348  frgr3vlem2  30362  1to2vfriswmgr  30367  1to3vfriswmgr  30368  frgrncvvdeqlem9  30395  frgrwopreg  30411  frgr2wwlkeqm  30419  2wspmdisj  30425  numclwwlk1lem2f  30443  frgrreggt1  30481  frgrregord013  30483  frgrregord13  30484  l2p  30568  nmlno0lem  30882  normgt0  31216  ocin  31385  nmlnop0iALT  32084  nmopun  32103  cvpss  32374  cvnbtwn  32375  atcvati  32475  mdsymlem6  32497  iunrnmptss  32653  expgt0b  32908  wrdt2ind  33031  irngssv  33851  issgon  34286  mbfmcnt  34431  ballotlemfc0  34656  ballotlemfcc  34657  satfv0  35559  satfv0fun  35572  fmla1  35588  gonarlem  35595  gonar  35596  goalrlem  35597  goalr  35598  fmla0disjsuc  35599  satffunlem  35602  satffunlem1lem1  35603  satffunlem2lem1  35605  satfun  35612  satfv0fvfmla0  35614  sategoelfv  35621  mthmblem  35781  pprodss4v  36083  funpartfun  36144  funpartfv  36146  5segofs  36207  btwnxfr  36257  brofs2  36278  brifs2  36279  btwnconn1  36302  segleantisym  36316  broutsideof2  36323  outsidene1  36324  outsidene2  36325  funray  36341  lineunray  36348  cldbnd  36527  bj-imdirval3  37517  topdifinffinlem  37680  isbasisrelowllem1  37688  isbasisrelowllem2  37689  relowlpssretop  37697  inunissunidif  37708  pibt2  37750  matunitlindf  37956  poimir  37991  volsupnfl  38003  itg2addnclem  38009  cover2  38053  sdclem2  38080  fdc  38083  sstotbnd3  38114  heibor1  38148  clmgmOLD  38189  smgrpmgm  38202  smgrpassOLD  38203  dvrunz  38292  0rngo  38365  mopickr  38709  sucmapleftuniq  38828  lsatcvat  39513  lshpkrex  39581  cmtbr3N  39717  atn0  39771  atnle  39780  cvlsupr4  39808  cvlsupr5  39809  cvlsupr6  39810  cvrval4N  39877  cvratlem  39884  2llnjN  40030  2lplnj  40083  linepsubN  40215  elpaddatiN  40268  elpcliN  40356  pclcmpatN  40364  ldilval  40576  ltrnu  40584  cdleme18d  40758  tendotp  41224  tendof  41226  tendovalco  41228  diatrl  41507  diaintclN  41521  dvheveccl  41575  dibintclN  41630  dihord6apre  41719  dihmeetlem1N  41753  dihpN  41799  dihintcl  41807  dochkrshp4  41852  oexpreposd  42771  pw2f1ocnv  43486  iocinico  43661  onsucf1olem  43719  succlg  43777  oacl2g  43779  omabs2  43781  omcl2  43782  naddcnfcom  43815  naddcnfass  43818  safesnsupfidom1o  43865  infordmin  43980  pr2cv  43996  expgrowthi  44781  iotavalsb  44881  bi23imp1  44943  ioogtlb  45946  iocgtlb  45953  iocleub  45954  icoltub  45959  iooltub  45961  stoweidlem31  46480  oppr  47493  funressnfv  47506  fsetsniunop  47512  fsetsnf1  47515  eu2ndop1stv  47588  afvelrnb0  47627  otiunsndisjX  47742  el1fzopredsuc  47789  2ffzoeq  47791  uniimaprimaeqfv  47857  elsetpreimafveqfv  47867  iccpartimp  47892  iccpartrn  47905  iccpartf  47906  iccpartnel  47913  fargshiftf  47915  fargshiftfo  47917  ichnfimlem  47938  ichnfim  47939  ichreuopeq  47948  sprel  47959  sprsymrelfvlem  47965  sprsymrelfolem2  47968  prproropf1olem4  47981  prprelb  47991  poprelb  47999  fmtnofac1  48048  prmdvdsfmtnof1lem2  48063  31prm  48075  lighneallem3  48085  ppivalnnnprm  48106  nn0o1gt2ALTV  48185  nn0oALTV  48187  odd2prm2  48209  mogoldbblem  48211  fpprbasnn  48220  fpprnn  48221  sbgoldbaltlem1  48270  nnsum3primesle9  48285  bgoldbtbndlem1  48296  bgoldbtbndlem2  48297  grimedgi  48427  grtriproplem  48430  grtriprop  48432  cycl3grtrilem  48437  cycl3grtri  48438  isubgr3stgrlem8  48464  gpgvtxel2  48539  gpgedgiov  48556  gpgedg2iv  48558  gpgprismgr4cycllem7  48592  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  pgnbgreunbgrlem2  48608  pgnbgreunbgrlem4  48610  pgnbgreunbgrlem5  48614  upwlkbprop  48629  clcllaw  48682  intop  48694  assintop  48700  assintopcllaw  48703  elrngchomALTV  48760  rngccatidALTV  48763  rngcinvALTV  48767  rngcisoALTV  48768  rhmsubcALTVlem3  48774  rhmsubcALTVlem4  48775  funcringcsetcALTV2lem7  48787  elringchomALTV  48794  ringccatidALTV  48797  ringcisoALTV  48802  funcringcsetclem7ALTV  48810  ztprmneprm  48838  suppmptcfin  48867  linccl  48905  linc1  48916  lincolss  48925  ldepspr  48964  nn0sumshdiglem1  49112  0aryfvalelfv  49126  rrxlines  49224  rrxsphere  49239  itsclc0yqsol  49255  itschlc0xyqsol1  49257  fdomne0  49340  f002  49344  fvconstr2  49354  fullthinc  49940