Theorem syl6bi 256

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 232	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		syl6bi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	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  1969  sb3OLD  2494  sb1OLD  2496  sb4a  2498  hbsb2  2500  dfsb2  2511  2eu2  2714  nfabdw  2976  reu6  3665  2reu2  3827  sseq0  4307  disjel  4364  disjpss  4368  preq12b  4741  prneimg  4745  preqsnd  4749  elinti  4847  zfrepclf  5162  dtru  5236  opth1g  5335  sbcop1  5344  snopeqop  5361  propeqop  5362  otsndisj  5374  otiunsndisj  5375  iunopeqop  5376  po2ne  5453  soasym  5468  elreldm  5769  dfres3  5823  relcnvtrg  6086  relresfld  6095  ordtr2  6203  ordssun  6258  funopg  6358  funimass2  6407  f0dom0  6537  elfv2ex  6686  fveqdmss  6823  eldmrexrnb  6835  fvcofneq  6836  funopsn  6887  funopdmsn  6889  funsndifnop  6890  elunirn  6988  2f1fvneq  6996  oprabidw  7166  oprabid  7167  brfvopab  7190  limuni3  7547  peano5  7585  op1steq  7715  el2mpocsbcl  7763  bropopvvv  7768  bropfvvvv  7770  f1o2ndf1  7801  frxp  7803  fnwelem  7808  suppimacnv  7824  fvn0elsuppb  7830  suppfnss  7838  reldmtpos  7883  rntpos  7888  seqomlem2  8070  oaordi  8155  oa00  8168  oalimcl  8169  omeulem1  8191  nnaordi  8227  ecopovtrn  8383  undifixp  8481  mapdom2  8672  unxpdomlem3  8708  enp1i  8737  findcard2  8742  infssuni  8799  wdompwdom  9026  preleqg  9062  opthreg  9065  inf3lemd  9074  inf3lem2  9076  inf3lem6  9080  cnfcomlem  9146  cnfcom3  9151  karden  9308  carden2a  9379  alephdom  9492  dfac5lem4  9537  dfac12r  9557  kmlem2  9562  kmlem12  9572  cfslb2n  9679  alephsing  9687  fin23lem30  9753  fin1a2lem6  9816  fin1a2lem13  9823  axcc2lem  9847  domtriomlem  9853  axdc3lem2  9862  axdc4lem  9866  brdom6disj  9943  alephexp1  9990  pwfseq  10075  addnidpi  10312  indpi  10318  nqereu  10340  ltsonq  10380  distrlem5pr  10438  addcanpr  10457  suplem1pr  10463  suplem2pr  10464  ltsrpr  10488  ltsosr  10505  sqgt0sr  10517  leltne  10719  ltnsym  10727  ltlen  10730  eqlei  10739  eqlei2  10740  infm3  11587  nnunb  11881  0mnnnnn0  11917  elnnnn0b  11929  nn0ge2m1nn  11952  nn0le2is012  12034  btwnz  12072  uz11  12255  xrleltne  12526  xltnegi  12597  xnn0lenn0nn0  12626  xnn0xadd0  12628  xmulasslem2  12663  reltxrnmnf  12723  icogelb  12776  iccleub  12780  uznfz  12985  2ffzeq  13023  elfzonlteqm1  13108  elfzo0l  13122  elfznelfzob  13138  elfzr  13145  elfzlmr  13146  injresinjlem  13152  injresinj  13153  fleqceilz  13217  modadd1  13271  modmul1  13287  modirr  13305  addmodlteq  13309  uzrdgfni  13321  fsuppmapnn0fiub0  13356  fsuppmapnn0ub  13358  seqf1o  13407  expnngt1  13598  hashrabsn01  13730  hashrabsn1  13731  hash1snb  13776  hash1n0  13778  hashf1lem2  13810  hash2prde  13824  hash2prd  13829  hash2pwpr  13830  hashle2pr  13831  hashle2prv  13832  hashge2el2dif  13834  hashge2el2difr  13835  fundmge2nop0  13846  ffz0iswrd  13884  ccatrcl1  13939  pfxsuff1eqwrdeq  14052  wrdind  14075  wrd2ind  14076  swrdccatin1  14078  swrdccat3blem  14092  2cshwcshw  14178  cshwcsh2id  14181  cshimadifsn  14182  2swrd2eqwrdeq  14306  wwlktovf  14311  wwlktovfo  14313  s3sndisj  14318  s3iunsndisj  14319  relexpindlem  14414  rexico  14705  lo1le  15000  fsum2dlem  15117  ntrivcvg  15245  fprodss  15294  fprod2dlem  15326  0dvds  15622  mod2eq1n2dvds  15688  opoe  15704  omoe  15705  opeo  15706  omeo  15707  m1exp1  15717  nn0enne  15718  nn0o1gt2  15722  gcdneg  15860  dfgcd2  15884  algcvga  15913  eucalglt  15919  lcmf  15967  coprmdvds  15987  divgcdcoprmex  16000  cncongr1  16001  prm2orodd  16025  prm23lt5  16141  pockthi  16233  prmreclem5  16246  ramtcl2  16337  cshwrepswhash1  16428  f1ocpbl  16790  f1ovscpbl  16791  f1olecpbl  16792  monhom  16997  epihom  17004  inveq  17036  invcoisoid  17054  isocoinvid  17055  ciclcl  17064  cicrcl  17065  isinitoi  17255  istermoi  17256  2initoinv  17262  2termoinv  17269  setciso  17343  embedsetcestrclem  17399  ipopos  17762  gsumval2a  17887  ismnddef  17905  dfgrp2e  18121  symg2bas  18513  snsymgefmndeq  18515  symgvalstruct  18517  symgfix2  18536  gsmsymgreq  18552  pmtrdifellem4  18599  mndodcongi  18663  pj1eu  18814  cycsubmcmn  19001  dprd2da  19157  rimf1o  19482  rimrhm  19483  brric2  19493  lmodfopnelem1  19663  lspdisjb  19891  lspsnsubn0  19905  0ring01eq  20037  obs2ss  20418  psrbaglefi  20610  mamufacex  20996  mat0dim0  21072  mat0dimid  21073  mat0dimscm  21074  dmatmat  21099  scmatmat  21114  mat1scmat  21144  1mavmul  21153  mavmulsolcl  21156  gsummatr01  21264  cpmatpmat  21315  cpmadugsumlemF  21481  tg2  21570  tgcl  21574  neii1  21711  neii2  21713  neindisj2  21728  perfopn  21790  ordtbas2  21796  pnfnei  21825  mnfnei  21826  llyidm  22093  txlm  22253  qtopuni  22307  tgqtop  22317  isfild  22463  snfil  22469  fbunfip  22474  fgss2  22479  fmco  22566  fbflim2  22582  cnpflf2  22605  fcfelbas  22641  fcfneii  22642  alexsubALTlem2  22653  alexsubALT  22656  tgpconncompeqg  22717  tsmscl  22740  tngngpim  23265  tgioo  23401  xrsmopn  23417  iccntr  23426  reconnlem2  23432  addcnlem  23469  htpycn  23578  phtpyhtpy  23587  pi1blem  23644  fgcfil  23875  ioombl1lem4  24165  dyadmbl  24204  itg2gt0  24364  ditgneg  24460  dvivthlem1  24611  coeeq2  24839  aannenlem2  24925  sineq0  25116  efif1o  25138  xrlimcnp  25554  vmacl  25703  efvmacl  25705  vmalelog  25789  dchrelbasd  25823  lgsqr  25935  lgsqrmodndvds  25937  gausslemma2dlem0i  25948  2lgslem2  25979  2lgs  25991  2lgsoddprmlem3  25998  2sqnn  26023  2sqreultlem  26031  2sqreultblem  26032  2sqreunnltlem  26034  2sqreunnltblem  26035  elntg2  26779  uhgr0vb  26865  umgrupgr  26896  umgrnloopv  26899  umgredgprv  26900  umgrislfupgrlem  26915  umgredg  26931  uspgrushgr  26968  uspgrupgr  26969  usgruspgr  26971  usgredgprvALT  26985  usgrnloopvALT  26991  uhgr2edg  26998  edg0usgr  27043  egrsubgr  27067  0uhgrsubgr  27069  uhgrspansubgrlem  27080  nbuhgr  27133  cusgrsize2inds  27243  cusgrfilem2  27246  vtxdg0v  27263  1loopgrnb0  27292  vtxdginducedm1lem4  27332  wlkvtxeledg  27413  wlkeq  27423  wlkl1loop  27427  wlk1walk  27428  upgrwlkedg  27431  uspgr2wlkeq  27435  wlkv0  27440  wlkonl1iedg  27455  wlkon2n0  27456  wlkp1lem8  27470  wlkp1  27471  lfgrwlkprop  27477  lfgrwlknloop  27479  2pthnloop  27520  upgrwlkdvde  27526  spthonepeq  27541  uhgrwkspthlem2  27543  usgr2wlkneq  27545  usgr2trlncl  27549  usgr2trlspth  27550  pthdlem2lem  27556  clwlkcompbp  27571  uspgrn2crct  27594  wwlks  27621  wwlknbp  27628  0enwwlksnge1  27650  wwlkswwlksn  27651  wlklnwwlkln1  27654  wwlksnextproplem3  27697  wwlksnextprop  27698  wspthsnonn0vne  27703  wspn0  27710  2pthon3v  27729  umgr2adedgspth  27734  rusgr0edg  27759  clwwlkccat  27775  clwlkclwwlklem2fv2  27781  clwlkclwwlklem2a4  27782  clwlkclwwlklem2  27785  clwlkclwwlkflem  27789  clwwlknp  27822  clwwlkwwlksb  27839  clwwlkext2edg  27841  erclwwlkneqlen  27853  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  clwwlknonwwlknonb  27891  upgr1wlkdlem1  27930  upgr3v3e3cycl  27965  uhgr3cyclexlem  27966  1conngr  27979  conngrv2edg  27980  eupth2lem3lem4  28016  eulercrct  28027  isfrgr  28045  frgr3vlem2  28059  1to2vfriswmgr  28064  1to3vfriswmgr  28065  frgrncvvdeqlem9  28092  frgrwopreg  28108  frgr2wwlkeqm  28116  2wspmdisj  28122  numclwwlk1lem2f  28140  frgrreggt1  28178  frgrregord013  28180  frgrregord13  28181  l2p  28262  nmlno0lem  28576  normgt0  28910  ocin  29079  nmlnop0iALT  29778  nmopun  29797  cvpss  30068  cvnbtwn  30069  atcvati  30169  mdsymlem6  30191  iunrnmptss  30329  wrdt2ind  30653  issgon  31492  mbfmcnt  31636  ballotlemfc0  31860  ballotlemfcc  31861  satfv0  32718  satfv0fun  32731  fmla1  32747  gonarlem  32754  gonar  32755  goalrlem  32756  goalr  32757  fmla0disjsuc  32758  satffunlem  32761  satffunlem1lem1  32762  satffunlem2lem1  32764  satfun  32771  satfv0fvfmla0  32773  sategoelfv  32780  mthmblem  32940  sltintdifex  33281  sltres  33282  nosepnelem  33297  nolt02o  33312  pprodss4v  33458  funpartfun  33517  funpartfv  33519  5segofs  33580  btwnxfr  33630  brofs2  33651  brifs2  33652  btwnconn1  33675  segleantisym  33689  broutsideof2  33696  outsidene1  33697  outsidene2  33698  funray  33714  lineunray  33721  cldbnd  33787  bj-dtru  34254  bj-imdirval3  34599  topdifinffinlem  34764  isbasisrelowllem1  34772  isbasisrelowllem2  34773  relowlpssretop  34781  inunissunidif  34792  pibt2  34834  matunitlindf  35055  poimir  35090  volsupnfl  35102  itg2addnclem  35108  cover2  35152  sdclem2  35180  fdc  35183  sstotbnd3  35214  heibor1  35248  clmgmOLD  35289  smgrpmgm  35302  smgrpassOLD  35303  dvrunz  35392  0rngo  35465  lsatcvat  36346  lshpkrex  36414  cmtbr3N  36550  atn0  36604  atnle  36613  cvlsupr4  36641  cvlsupr5  36642  cvlsupr6  36643  cvrval4N  36710  cvratlem  36717  2llnjN  36863  2lplnj  36916  linepsubN  37048  elpaddatiN  37101  elpcliN  37189  pclcmpatN  37197  ldilval  37409  ltrnu  37417  cdleme18d  37591  tendotp  38057  tendof  38059  tendovalco  38061  diatrl  38340  diaintclN  38354  dvheveccl  38408  dibintclN  38463  dihord6apre  38552  dihmeetlem1N  38586  dihpN  38632  dihintcl  38640  dochkrshp4  38685  oexpreposd  39487  pw2f1ocnv  39978  iocinico  40162  infordmin  40240  pr2cv  40247  expgrowthi  41037  iotavalsb  41137  bi23imp1  41201  ioogtlb  42132  iocgtlb  42139  iocleub  42140  icoltub  42145  iooltub  42147  stoweidlem31  42673  oppr  43622  funressnfv  43635  eu2ndop1stv  43681  afvelrnb0  43720  otiunsndisjX  43835  el1fzopredsuc  43882  fzoopth  43884  2ffzoeq  43885  uniimaprimaeqfv  43899  elsetpreimafveqfv  43909  iccpartimp  43934  iccpartrn  43947  iccpartf  43948  iccpartnel  43955  fargshiftf  43957  fargshiftfo  43959  ichnfimlem  43980  ichnfim  43981  ichreuopeq  43990  sprel  44001  sprsymrelfvlem  44007  sprsymrelfolem2  44010  prproropf1olem4  44023  prprelb  44033  poprelb  44041  fmtnofac1  44087  prmdvdsfmtnof1lem2  44102  31prm  44114  lighneallem3  44125  nn0o1gt2ALTV  44212  nn0oALTV  44214  odd2prm2  44236  mogoldbblem  44238  fpprbasnn  44247  fpprnn  44248  sbgoldbaltlem1  44297  nnsum3primesle9  44312  bgoldbtbndlem1  44323  bgoldbtbndlem2  44324  isomuspgrlem2d  44349  upwlkbprop  44366  mgmpropd  44395  clcllaw  44451  intop  44463  assintop  44469  assintopcllaw  44472  rngimf1o  44529  rngimrnghm  44530  c0snmgmhm  44538  elrngchom  44592  rnghmsubcsetclem1  44599  rnghmsubcsetclem2  44600  rngcid  44603  rngcinv  44605  rngciso  44606  elrngchomALTV  44610  rngccatidALTV  44613  rngcinvALTV  44617  rngcisoALTV  44618  funcrngcsetcALT  44623  zrinitorngc  44624  zrtermorngc  44625  elringchom  44638  rhmsubcsetclem1  44645  rhmsubcsetclem2  44646  ringcid  44649  rhmsubcrngclem1  44651  rhmsubcrngclem2  44652  ringcinv  44656  ringciso  44657  funcringcsetcALTV2lem7  44666  elringchomALTV  44673  ringccatidALTV  44676  ringcinvALTV  44680  ringcisoALTV  44681  funcringcsetclem7ALTV  44689  irinitoringc  44693  zrtermoringc  44694  rhmsubclem3  44712  rhmsubclem4  44713  rhmsubcALTVlem3  44730  rhmsubcALTVlem4  44731  ztprmneprm  44749  suppmptcfin  44781  linccl  44823  linc1  44834  lincolss  44843  ldepspr  44882  nn0sumshdiglem1  45035  0aryfvalelfv  45049  rrxlines  45147  rrxsphere  45162  itsclc0yqsol  45178  itschlc0xyqsol1  45180