Theorem syl5ibcom 244

Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)

Hypotheses

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

Assertion

Ref	Expression
syl5ibcom	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		syl5ib.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl5ib.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	syl5ib 243	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	com12 32	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:  biimpcd  248  elrab3t  3616  mob2  3645  rmob  3819  sneqrg  4767  preq1b  4774  prel12g  4791  disjxun  5068  sotric  5522  sotrieq  5523  iss  5932  poirr2  6018  xp11  6067  nordeq  6270  nsuceq0  6331  ordequn  6351  tz6.12c  6781  fnbrfvb  6804  foeqcnvco  7152  f1eqcocnv  7153  f1eqcocnvOLD  7154  dfwe2  7602  releldmdifi  7859  mposn  7914  tfrlem15  8194  tz7.44-2  8209  tz7.48-1  8244  tz7.49  8246  oawordexr  8349  oewordi  8384  oeeulem  8394  nna0r  8402  nnawordex  8430  nnaordex  8431  oaabs  8438  oaabs2  8439  ectocld  8531  ecoptocl  8554  mapsnd  8632  eqeng  8729  difsnen  8794  fopwdom  8820  frfi  8989  elfiun  9119  ordiso  9205  ordtypelem7  9213  wemaplem2  9236  suc11reg  9307  inf3lem6  9321  noinfep  9348  cantnff  9362  cantnfp1lem2  9367  cantnfp1lem3  9368  cantnflem1  9377  cantnf  9381  r111  9464  rankc2  9560  tcrank  9573  cardnueq0  9653  fodomfi2  9747  alephinit  9782  dfac9  9823  dfac12k  9834  djuinf  9875  ackbij1  9925  ackbij2  9930  sornom  9964  fin23lem16  10022  fin23lem21  10026  isf32lem2  10041  fin1a2lem6  10092  itunitc  10108  zorn2lem4  10186  wunr1om  10406  tskr1om  10454  recmulnq  10651  ltexnq  10662  distrlem4pr  10713  1re  10906  0re  10908  0cnALT  11139  0cnALT2  11140  mulge0  11423  prodgt0  11752  peano2nn  11915  recnz  12325  zneo  12333  uzn0  12528  xlemul1a  12951  prunioo  13142  flidz  13458  ceilidz  13500  modid2  13546  modmuladdnn0  13563  om2uzrani  13600  uzrdgfni  13606  seqid  13696  seqz  13699  facdiv  13929  facwordi  13931  hashdom  14022  wrdnval  14176  wrdnfi  14179  wrdl1s1  14247  sqrmo  14891  fsumf1o  15363  isumltss  15488  supcvg  15496  dvdsnegb  15911  dvdsexp2im  15964  odd2np1lem  15977  odd2np1  15978  ltoddhalfle  15998  halfleoddlt  15999  opoe  16000  omoe  16001  opeo  16002  omeo  16003  bitsuz  16109  bezoutlem4  16178  gcddiv  16187  gcdzeq  16190  dvdssqim  16192  lcmgcdeq  16245  coprmdvds2  16287  rpmul  16292  divgcdcoprmex  16299  cncongr2  16301  dvdsprm  16336  coprm  16344  prmdvdsexp  16348  prmdiv  16414  pythagtriplem19  16462  pc2dvds  16508  pcadd  16518  prmpwdvds  16533  vdwlem11  16620  ramubcl  16647  0ram  16649  posasymb  17952  pleval2  17970  pltval3  17972  plttr  17975  pospo  17978  letsr  18226  intopsn  18253  ismgmid  18264  imasmnd2  18337  isgrpid2  18531  isgrpinv  18547  dfgrp3lem  18588  imasgrp2  18605  orbsta  18834  symgfix2  18939  pmtrfrn  18981  pmtrrn2  18983  odmulg  19078  odmulgeq  19079  gexdvdsi  19103  gexnnod  19108  pgpssslw  19134  sylow2alem1  19137  fislw  19145  lsmss1b  19187  lsmss2b  19189  efgrelexlemb  19271  torsubg  19370  ablfacrplem  19583  pgpfac1lem2  19593  pgpfac1lem3  19595  ablsimpnosubgd  19622  imasring  19773  dvdsrcl2  19807  dvdsrtr  19809  dvdsrmul1  19810  irredn0  19860  lspsneq0  20189  lmhmima  20224  lspsolv  20320  xrsdsreclblem  20556  dvdsrzring  20595  prmirredlem  20606  znunit  20683  pjdm2  20828  obselocv  20845  lindfrn  20938  opsrtoslem2  21173  mpfind  21227  mpfpf1  21427  pf1mpf  21428  cpmadugsumlemF  21933  baspartn  22012  bastop  22039  iscld3  22123  isopn3  22125  iscldtop  22154  ordtrest2lem  22262  2ndcredom  22509  2ndc1stc  22510  2ndcrest  22513  2ndcdisj  22515  2ndcsep  22518  kgenidm  22606  dfac14  22677  tx2ndc  22710  kqreglem1  22800  rnelfm  23012  fmfnfmlem2  23014  fmfnfmlem4  23016  fmfnfm  23017  flimtopon  23029  fclstopon  23071  xrsmopn  23881  icccmplem2  23892  reconnlem1  23895  iccpnfcnv  24013  cphsqrtcl2  24255  ivthlem3  24522  ivthicc  24527  ovolctb  24559  ioombl  24634  itgabs  24904  itgsplitioo  24907  dvlip  25062  c1liplem1  25065  c1lip1  25066  dvgt0lem1  25071  dvivthlem2  25078  dvne0  25080  lhop1lem  25082  lhop1  25083  lhop2  25084  lhop  25085  dvcvx  25089  itgsubstlem  25117  mdegnn0cl  25141  ig1peu  25241  elply2  25262  plypf1  25278  dgreq0  25331  aannenlem3  25395  abelthlem2  25496  lognegb  25650  eflogeq  25662  efopn  25718  cxpge0  25743  cxplea  25756  cxple2  25757  cxpcn3lem  25805  cxpaddlelem  25809  cxpaddle  25810  cxpeq  25815  asinsinb  25952  acoscosb  25953  atantanb  25979  wilthlem2  26123  sqf11  26193  sqff1o  26236  ppiublem1  26255  lgsdir  26385  lgsne0  26388  lgsquadlem3  26435  2sqblem  26484  dchrisum0flblem1  26561  ostth3  26691  ostth  26692  colinearalg  27181  axcontlem5  27239  axcontlem9  27243  uhgrn0  27340  upgrfn  27360  umgrfn  27372  uvtxnbgrvtx  27663  vtxduhgr0nedg  27762  pthdivtx  27998  iswwlksnx  28106  wpthswwlks2on  28227  clwwlkn  28291  clwwlknonwwlknonb  28371  eupth2lem2  28484  eupth2lem3lem6  28498  htthlem  29180  pjpreeq  29661  h1dn0  29815  spansneleqi  29832  rnbra  30370  dfpjop  30445  elpjrn  30453  stm1i  30506  mdbr2  30559  mdsl2i  30585  sumdmdlem  30681  dmdbr6ati  30686  ordtrest2NEWlem  31774  xrge0iifcnv  31785  eulerpartlemb  32235  erdszelem8  33060  cvmlift3lem4  33184  cvmlift3lem5  33185  fmlasucdisj  33261  mrsub0  33378  mrsubccat  33380  mrsubcn  33381  msubrn  33391  msrid  33407  elmthm  33438  eldifsucnn  33597  dfon2lem9  33673  ttrcltr  33702  poxp2  33717  poxp3  33723  poseq  33729  noseponlem  33794  nodenselem4  33817  nodenselem5  33818  nodenselem7  33820  nodenselem8  33821  nolt02o  33825  nogt01o  33826  nosupbnd2lem1  33845  noetasuplem4  33866  slerec  33940  madebdayim  33997  btwnconn1lem11  34326  broutsideof2  34351  opnbnd  34441  tailfb  34493  bj-ideqg1  35262  fin2so  35691  lindsadd  35697  poimirlem9  35713  poimirlem17  35721  poimirlem26  35730  poimirlem27  35731  poimirlem31  35735  itgabsnc  35773  ftc2nc  35786  sdclem2  35827  subspopn  35837  equivtotbnd  35863  rngosn3  36009  igenval2  36151  isfldidl  36153  relcnveq3  36383  ecex2  36390  iss2  36406  elrelscnveq3  36536  lshpinN  36930  lsatcv0eq  36988  lsatcv1  36989  cvrnbtwn3  37217  cvrnbtwn4  37220  cvrcmp  37224  atnlt  37254  cvlexchb1  37271  2llnne2N  37349  atcvr0eq  37367  lnnat  37368  cvrat4  37384  ps-1  37418  3at  37431  llncmp  37463  llnnlt  37464  llncvrlpln2  37498  llncvrlpln  37499  lplncmp  37503  lplnnlt  37506  lplncvrlvol2  37556  lplncvrlvol  37557  lvolcmp  37558  lvolnltN  37559  dalempnes  37592  dalemqnet  37593  dalem-cly  37612  dalem44  37657  lncmp  37724  cdlemblem  37734  llnexch2N  37811  osumcllem4N  37900  pexmidlem1N  37911  lhp2atnle  37974  cdleme11dN  38203  cdleme20k  38260  cdleme21at  38269  cdleme21ct  38270  cdleme32e  38386  cdleme35f  38395  tendoex  38916  dochexmidlem1  39401  lcfrlem9  39491  mapd1o  39589  mapdindp3  39663  elre0re  40212  dvdsexpim  40249  flt0  40390  ismrc  40439  pellexlem1  40567  aomclem4  40798  dfac21  40807  lsmfgcl  40815  lmhmfgima  40825  dfacbasgrp  40849  hbtlem6  40870  fiuneneq  40938  stoweidlem27  43458  stoweidlem29  43460  fcoresf1  44450  tz6.12c-afv2  44621  dfatbrafv2b  44624  fnbrafv2b  44627  iccpartrn  44770  prmdvdsfmtnof1lem2  44925  mod42tp1mod8  44942  assintopass  45296  rrxsphere  45982