Theorem syl6bi 252

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

Ref	Expression
syl6bi.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
syl6bi.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
syl6bi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6bi

Step	Hyp	Ref	Expression
1		syl6bi.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 228	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		syl6bi.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  1971  sb3OLD  2482  sb1OLD  2483  sb4a  2485  hbsb2  2487  dfsb2  2498  2eu2  2655  nfabdwOLD  2932  reu6  3662  2reu2  3832  sseq0  4334  disjel  4391  disjpss  4395  preq12b  4782  prneimg  4786  preqsnd  4790  elinti  4889  zfrepclf  5219  dtruALT2  5294  dtru  5360  opth1g  5394  sbcop1  5403  snopeqop  5421  propeqop  5422  otsndisj  5434  otiunsndisj  5435  iunopeqop  5436  po2ne  5520  soasym  5535  elreldm  5847  dfres3  5899  relcnvtrg  6174  relresfld  6183  elpredimg  6221  ordtr2  6314  ordssun  6369  funopg  6475  funimass2  6524  f0dom0  6667  elfv2ex  6824  fveqdmss  6965  eldmrexrnb  6977  fvcofneq  6978  funopsn  7029  funopdmsn  7031  funsndifnop  7032  elunirn  7133  2f1fvneq  7142  oprabidw  7315  oprabid  7316  brfvopab  7341  limuni3  7708  peano5  7749  peano5OLD  7750  op1steq  7884  el2mpocsbcl  7934  bropopvvv  7939  bropfvvvv  7941  f1o2ndf1  7972  frxp  7976  fnwelem  7981  suppimacnv  7999  fvn0elsuppb  8006  suppfnss  8014  reldmtpos  8059  rntpos  8064  seqomlem2  8291  oaordi  8386  oa00  8399  oalimcl  8400  omeulem1  8422  nnaordi  8458  ecopovtrn  8618  undifixp  8731  mapdom2  8944  unxpdomlem3  9038  enp1i  9061  findcard2OLD  9065  infssuni  9119  wdompwdom  9346  preleqg  9382  opthreg  9385  inf3lemd  9394  inf3lem2  9396  inf3lem6  9400  cnfcomlem  9466  cnfcom3  9471  karden  9662  carden2a  9733  alephdom  9846  dfac5lem4  9891  dfac12r  9911  kmlem2  9916  kmlem12  9926  cfslb2n  10033  alephsing  10041  fin23lem30  10107  fin1a2lem6  10170  fin1a2lem13  10177  axcc2lem  10201  domtriomlem  10207  axdc3lem2  10216  axdc4lem  10220  brdom6disj  10297  alephexp1  10344  pwfseq  10429  addnidpi  10666  indpi  10672  nqereu  10694  ltsonq  10734  distrlem5pr  10792  addcanpr  10811  suplem1pr  10817  suplem2pr  10818  ltsrpr  10842  ltsosr  10859  sqgt0sr  10871  leltne  11073  ltnsym  11082  ltlen  11085  eqlei  11094  eqlei2  11095  infm3  11943  nnunb  12238  0mnnnnn0  12274  elnnnn0b  12286  nn0ge2m1nn  12311  nn0le2is012  12393  btwnz  12432  uz11  12616  xrleltne  12888  xltnegi  12959  xnn0lenn0nn0  12988  xnn0xadd0  12990  xmulasslem2  13025  reltxrnmnf  13085  icogelb  13139  iccleub  13143  uznfz  13348  2ffzeq  13386  elfzonlteqm1  13472  elfzo0l  13486  elfznelfzob  13502  elfzr  13509  elfzlmr  13510  injresinjlem  13516  injresinj  13517  fleqceilz  13583  modadd1  13637  modmul1  13653  modirr  13671  addmodlteq  13675  uzrdgfni  13687  fsuppmapnn0fiub0  13722  fsuppmapnn0ub  13724  seqf1o  13773  expnngt1  13965  hashrabsn01  14097  hashrabsn1  14098  hash1snb  14143  hash1n0  14145  hashf1lem2  14179  hash2prde  14193  hash2prd  14198  hash2pwpr  14199  hashle2pr  14200  hashle2prv  14201  hashge2el2dif  14203  hashge2el2difr  14204  fundmge2nop0  14215  ffz0iswrd  14253  ccatrcl1  14308  pfxsuff1eqwrdeq  14421  wrdind  14444  wrd2ind  14445  swrdccatin1  14447  swrdccat3blem  14461  2cshwcshw  14547  cshwcsh2id  14550  cshimadifsn  14551  2swrd2eqwrdeq  14675  wwlktovf  14680  wwlktovfo  14682  s3sndisj  14687  s3iunsndisj  14688  relexpindlem  14783  rexico  15074  lo1le  15372  fsum2dlem  15491  ntrivcvg  15618  fprodss  15667  fprod2dlem  15699  0dvds  15995  mod2eq1n2dvds  16065  opoe  16081  omoe  16082  opeo  16083  omeo  16084  m1exp1  16094  nn0enne  16095  nn0o1gt2  16099  gcdneg  16238  dfgcd2  16263  algcvga  16293  eucalglt  16299  lcmf  16347  coprmdvds  16367  divgcdcoprmex  16380  cncongr1  16381  prm2orodd  16405  prm23lt5  16524  pockthi  16617  prmreclem5  16630  ramtcl2  16721  cshwrepswhash1  16813  f1ocpbl  17245  f1ovscpbl  17246  f1olecpbl  17247  monhom  17456  epihom  17463  inveq  17495  invcoisoid  17513  isocoinvid  17514  ciclcl  17523  cicrcl  17524  isinitoi  17723  istermoi  17724  2initoinv  17734  2termoinv  17741  setciso  17815  embedsetcestrclem  17883  ipopos  18263  gsumval2a  18378  ismnddef  18396  dfgrp2e  18614  symg2bas  19009  snsymgefmndeq  19011  symgvalstruct  19013  symgvalstructOLD  19014  symgfix2  19033  gsmsymgreq  19049  pmtrdifellem4  19096  mndodcongi  19160  pj1eu  19311  cycsubmcmn  19498  dprd2da  19654  rimf1o  19987  rimrhm  19988  brric2  19998  lmodfopnelem1  20168  lspdisjb  20397  lspsnsubn0  20411  0ring01eq  20551  obs2ss  20945  psrbaglefiOLD  21145  mamufacex  21547  mat0dim0  21625  mat0dimid  21626  mat0dimscm  21627  dmatmat  21652  scmatmat  21667  mat1scmat  21697  1mavmul  21706  mavmulsolcl  21709  gsummatr01  21817  cpmatpmat  21868  cpmadugsumlemF  22034  tg2  22124  tgcl  22128  neii1  22266  neii2  22268  neindisj2  22283  perfopn  22345  ordtbas2  22351  pnfnei  22380  mnfnei  22381  llyidm  22648  txlm  22808  qtopuni  22862  tgqtop  22872  isfild  23018  snfil  23024  fbunfip  23029  fgss2  23034  fmco  23121  fbflim2  23137  cnpflf2  23160  fcfelbas  23196  fcfneii  23197  alexsubALTlem2  23208  alexsubALT  23211  tgpconncompeqg  23272  tsmscl  23295  tngngpim  23832  tgioo  23968  xrsmopn  23984  iccntr  23993  reconnlem2  23999  addcnlem  24036  htpycn  24145  phtpyhtpy  24154  pi1blem  24211  fgcfil  24444  ioombl1lem4  24734  dyadmbl  24773  itg2gt0  24934  ditgneg  25030  dvivthlem1  25181  coeeq2  25412  aannenlem2  25498  sineq0  25689  efif1o  25711  xrlimcnp  26127  vmacl  26276  efvmacl  26278  vmalelog  26362  dchrelbasd  26396  lgsqr  26508  lgsqrmodndvds  26510  gausslemma2dlem0i  26521  2lgslem2  26552  2lgs  26564  2lgsoddprmlem3  26571  2sqnn  26596  2sqreultlem  26604  2sqreultblem  26605  2sqreunnltlem  26607  2sqreunnltblem  26608  elntg2  27362  uhgr0vb  27451  umgrupgr  27482  umgrnloopv  27485  umgredgprv  27486  umgrislfupgrlem  27501  umgredg  27517  uspgrushgr  27554  uspgrupgr  27555  usgruspgr  27557  usgredgprvALT  27571  usgrnloopvALT  27577  uhgr2edg  27584  edg0usgr  27629  egrsubgr  27653  0uhgrsubgr  27655  uhgrspansubgrlem  27666  nbuhgr  27719  cusgrsize2inds  27829  cusgrfilem2  27832  vtxdg0v  27849  1loopgrnb0  27878  vtxdginducedm1lem4  27918  wlkvtxeledg  28000  wlkeq  28010  wlkl1loop  28014  wlk1walk  28015  upgrwlkedg  28018  uspgr2wlkeq  28022  wlkv0  28027  wlkonl1iedg  28042  wlkon2n0  28043  wlkp1lem8  28057  wlkp1  28058  lfgrwlkprop  28064  lfgrwlknloop  28066  2pthnloop  28108  upgrwlkdvde  28114  spthonepeq  28129  uhgrwkspthlem2  28131  usgr2wlkneq  28133  usgr2trlncl  28137  usgr2trlspth  28138  pthdlem2lem  28144  clwlkcompbp  28159  uspgrn2crct  28182  wwlks  28209  wwlknbp  28216  0enwwlksnge1  28238  wwlkswwlksn  28239  wlklnwwlkln1  28242  wwlksnextproplem3  28285  wwlksnextprop  28286  wspthsnonn0vne  28291  wspn0  28298  2pthon3v  28317  umgr2adedgspth  28322  rusgr0edg  28347  clwwlkccat  28363  clwlkclwwlklem2fv2  28369  clwlkclwwlklem2a4  28370  clwlkclwwlklem2  28373  clwlkclwwlkflem  28377  clwwlknp  28410  clwwlkwwlksb  28427  clwwlkext2edg  28429  erclwwlkneqlen  28441  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  clwwlknonwwlknonb  28479  upgr1wlkdlem1  28518  upgr3v3e3cycl  28553  uhgr3cyclexlem  28554  1conngr  28567  conngrv2edg  28568  eupth2lem3lem4  28604  eulercrct  28615  isfrgr  28633  frgr3vlem2  28647  1to2vfriswmgr  28652  1to3vfriswmgr  28653  frgrncvvdeqlem9  28680  frgrwopreg  28696  frgr2wwlkeqm  28704  2wspmdisj  28710  numclwwlk1lem2f  28728  frgrreggt1  28766  frgrregord013  28768  frgrregord13  28769  l2p  28850  nmlno0lem  29164  normgt0  29498  ocin  29667  nmlnop0iALT  30366  nmopun  30385  cvpss  30656  cvnbtwn  30657  atcvati  30757  mdsymlem6  30779  iunrnmptss  30914  wrdt2ind  31234  issgon  32100  mbfmcnt  32244  ballotlemfc0  32468  ballotlemfcc  32469  satfv0  33329  satfv0fun  33342  fmla1  33358  gonarlem  33365  gonar  33366  goalrlem  33367  goalr  33368  fmla0disjsuc  33369  satffunlem  33372  satffunlem1lem1  33373  satffunlem2lem1  33375  satfun  33382  satfv0fvfmla0  33384  sategoelfv  33391  mthmblem  33551  poxp2  33799  sltintdifex  33873  sltres  33874  nosepnelem  33891  nolt02o  33907  pprodss4v  34195  funpartfun  34254  funpartfv  34256  5segofs  34317  btwnxfr  34367  brofs2  34388  brifs2  34389  btwnconn1  34412  segleantisym  34426  broutsideof2  34433  outsidene1  34434  outsidene2  34435  funray  34451  lineunray  34458  cldbnd  34524  bj-dtru  35008  bj-imdirval3  35364  topdifinffinlem  35527  isbasisrelowllem1  35535  isbasisrelowllem2  35536  relowlpssretop  35544  inunissunidif  35555  pibt2  35597  matunitlindf  35784  poimir  35819  volsupnfl  35831  itg2addnclem  35837  cover2  35881  sdclem2  35909  fdc  35912  sstotbnd3  35943  heibor1  35977  clmgmOLD  36018  smgrpmgm  36031  smgrpassOLD  36032  dvrunz  36121  0rngo  36194  lsatcvat  37071  lshpkrex  37139  cmtbr3N  37275  atn0  37329  atnle  37338  cvlsupr4  37366  cvlsupr5  37367  cvlsupr6  37368  cvrval4N  37435  cvratlem  37442  2llnjN  37588  2lplnj  37641  linepsubN  37773  elpaddatiN  37826  elpcliN  37914  pclcmpatN  37922  ldilval  38134  ltrnu  38142  cdleme18d  38316  tendotp  38782  tendof  38784  tendovalco  38786  diatrl  39065  diaintclN  39079  dvheveccl  39133  dibintclN  39188  dihord6apre  39277  dihmeetlem1N  39311  dihpN  39357  dihintcl  39365  dochkrshp4  39410  oexpreposd  40328  pw2f1ocnv  40866  iocinico  41050  infordmin  41146  pr2cv  41162  expgrowthi  41958  iotavalsb  42058  bi23imp1  42122  ioogtlb  43040  iocgtlb  43047  iocleub  43048  icoltub  43053  iooltub  43055  stoweidlem31  43579  oppr  44535  funressnfv  44548  fsetsniunop  44554  fsetsnf1  44557  eu2ndop1stv  44628  afvelrnb0  44667  otiunsndisjX  44782  el1fzopredsuc  44828  fzoopth  44830  2ffzoeq  44831  uniimaprimaeqfv  44845  elsetpreimafveqfv  44855  iccpartimp  44880  iccpartrn  44893  iccpartf  44894  iccpartnel  44901  fargshiftf  44903  fargshiftfo  44905  ichnfimlem  44926  ichnfim  44927  ichreuopeq  44936  sprel  44947  sprsymrelfvlem  44953  sprsymrelfolem2  44956  prproropf1olem4  44969  prprelb  44979  poprelb  44987  fmtnofac1  45033  prmdvdsfmtnof1lem2  45048  31prm  45060  lighneallem3  45070  nn0o1gt2ALTV  45157  nn0oALTV  45159  odd2prm2  45181  mogoldbblem  45183  fpprbasnn  45192  fpprnn  45193  sbgoldbaltlem1  45242  nnsum3primesle9  45257  bgoldbtbndlem1  45268  bgoldbtbndlem2  45269  isomuspgrlem2d  45294  upwlkbprop  45311  mgmpropd  45340  clcllaw  45396  intop  45408  assintop  45414  assintopcllaw  45417  rngimf1o  45474  rngimrnghm  45475  c0snmgmhm  45483  elrngchom  45537  rnghmsubcsetclem1  45544  rnghmsubcsetclem2  45545  rngcid  45548  rngcinv  45550  rngciso  45551  elrngchomALTV  45555  rngccatidALTV  45558  rngcinvALTV  45562  rngcisoALTV  45563  funcrngcsetcALT  45568  zrinitorngc  45569  zrtermorngc  45570  elringchom  45583  rhmsubcsetclem1  45590  rhmsubcsetclem2  45591  ringcid  45594  rhmsubcrngclem1  45596  rhmsubcrngclem2  45597  ringcinv  45601  ringciso  45602  funcringcsetcALTV2lem7  45611  elringchomALTV  45618  ringccatidALTV  45621  ringcinvALTV  45625  ringcisoALTV  45626  funcringcsetclem7ALTV  45634  irinitoringc  45638  zrtermoringc  45639  rhmsubclem3  45657  rhmsubclem4  45658  rhmsubcALTVlem3  45675  rhmsubcALTVlem4  45676  ztprmneprm  45694  suppmptcfin  45726  linccl  45766  linc1  45777  lincolss  45786  ldepspr  45825  nn0sumshdiglem1  45978  0aryfvalelfv  45992  rrxlines  46090  rrxsphere  46105  itsclc0yqsol  46121  itschlc0xyqsol1  46123  fdomne0  46188  f002  46192  fvconstr2  46196  fullthinc  46338