Theorem syl5ibcom 245

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

Hypotheses

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

Assertion

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

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		imbitrid.1	. . 3 ⊢ (𝜑 → 𝜓)
2		imbitrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	imbitrid 244	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	com12 32	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:  biimpcd  249  elrab3t  3634  mob2  3662  rmob  3829  sneqrg  4783  preq1b  4790  prel12g  4808  disjxun  5084  sotric  5562  sotrieq  5563  iss  5994  poirr2  6081  xp11  6133  nordeq  6336  nsuceq0  6402  ordequn  6422  fnbrfvb  6884  2f1fvneq  7208  foeqcnvco  7248  f1eqcocnv  7249  dfwe2  7721  releldmdifi  7991  mposn  8046  poxp2  8086  poxp3  8093  poseq  8101  tfrlem15  8324  tz7.44-2  8339  tz7.48-1  8375  tz7.49  8377  oawordexr  8484  oewordi  8520  oeeulem  8530  nna0r  8538  nnawordex  8566  nnaordex  8567  nnaordex2  8568  oaabs  8577  oaabs2  8578  eldifsucnn  8593  elecex  8687  ectocld  8722  ecoptocl  8747  mapsnd  8827  eqeng  8926  difsnen  8990  fopwdom  9016  nneneq  9133  frfi  9188  elfiun  9336  ordiso  9424  ordtypelem7  9432  wemaplem2  9455  suc11reg  9531  inf3lem6  9545  noinfep  9572  cantnff  9586  cantnfp1lem2  9591  cantnfp1lem3  9592  cantnflem1  9601  cantnf  9605  ttrcltr  9628  r111  9690  rankc2  9786  tcrank  9799  cardnueq0  9879  fodomfi2  9973  alephinit  10008  dfac9  10050  dfac12k  10061  djuinf  10102  ackbij1  10150  ackbij2  10155  sornom  10190  fin23lem16  10248  fin23lem21  10252  isf32lem2  10267  fin1a2lem6  10318  itunitc  10334  zorn2lem4  10412  wunr1om  10633  tskr1om  10681  recmulnq  10878  ltexnq  10889  distrlem4pr  10940  1re  11135  0re  11137  0cnALT  11372  0cnALT2  11373  mulge0  11659  prodgt0  11993  peano2nn  12177  recnz  12595  zneo  12603  uzn0  12796  xlemul1a  13231  prunioo  13425  flidz  13760  ceilidz  13802  modid2  13848  modmuladdnn0  13868  om2uzrani  13905  uzrdgfni  13911  seqid  14000  seqz  14003  facdiv  14240  facwordi  14242  hashdom  14332  wrdnval  14498  wrdnfi  14501  wrdl1s1  14568  sqrmo  15204  fsumf1o  15676  isumltss  15804  supcvg  15812  dvdsnegb  16233  dvdsexp2im  16287  odd2np1lem  16300  odd2np1  16301  ltoddhalfle  16321  halfleoddlt  16322  opoe  16323  omoe  16324  opeo  16325  omeo  16326  bitsuz  16434  bezoutlem4  16502  gcddiv  16511  gcdzeq  16512  dvdssqim  16514  dvdsexpim  16515  lcmgcdeq  16572  coprmdvds2  16614  rpmul  16619  divgcdcoprmex  16626  cncongr2  16628  dvdsprm  16664  coprm  16672  prmdvdsexp  16676  prmdiv  16746  pythagtriplem19  16795  pc2dvds  16841  pcadd  16851  prmpwdvds  16866  vdwlem11  16953  ramubcl  16980  0ram  16982  posasymb  18276  pleval2  18292  pltval3  18294  plttr  18297  pospo  18300  letsr  18550  intopsn  18613  ismgmid  18624  imasmnd2  18733  isgrpid2  18943  isgrpinv  18960  dfgrp3lem  19005  imasgrp2  19022  orbsta  19279  symgfix2  19382  pmtrfrn  19424  pmtrrn2  19426  odmulg  19522  odmulgeq  19523  gexdvdsi  19549  gexnnod  19554  pgpssslw  19580  sylow2alem1  19583  fislw  19591  lsmss1b  19632  lsmss2b  19634  efgrelexlemb  19716  torsubg  19820  ablfacrplem  20033  pgpfac1lem2  20043  pgpfac1lem3  20045  ablsimpnosubgd  20072  imasrng  20149  imasring  20301  dvdsrcl2  20337  dvdsrtr  20339  dvdsrmul1  20340  irredn0  20394  lspsneq0  20998  lmhmima  21034  lspsolv  21133  xrsdsreclblem  21402  dvdsrzring  21451  prmirredlem  21462  znunit  21553  pjdm2  21701  obselocv  21718  lindfrn  21811  opsrtoslem2  22044  mpfind  22103  psdmul  22142  mpfpf1  22326  pf1mpf  22327  cpmadugsumlemF  22851  baspartn  22929  bastop  22956  iscld3  23039  isopn3  23041  iscldtop  23070  ordtrest2lem  23178  2ndcredom  23425  2ndc1stc  23426  2ndcrest  23429  2ndcdisj  23431  2ndcsep  23434  kgenidm  23522  dfac14  23593  tx2ndc  23626  kqreglem1  23716  rnelfm  23928  fmfnfmlem2  23930  fmfnfmlem4  23932  fmfnfm  23933  flimtopon  23945  fclstopon  23987  xrsmopn  24788  icccmplem2  24799  reconnlem1  24802  iccpnfcnv  24921  cphsqrtcl2  25163  ivthlem3  25430  ivthicc  25435  ovolctb  25467  ioombl  25542  itgabs  25812  itgsplitioo  25815  dvlip  25970  c1liplem1  25973  c1lip1  25974  dvgt0lem1  25979  dvivthlem2  25986  dvne0  25988  lhop1lem  25990  lhop1  25991  lhop2  25992  lhop  25993  dvcvx  25997  itgsubstlem  26025  mdegnn0cl  26046  ig1peu  26150  elply2  26171  plypf1  26187  dgreq0  26240  aannenlem3  26307  abelthlem2  26410  lognegb  26567  eflogeq  26579  efopn  26635  cxpge0  26660  cxplea  26673  cxple2  26674  cxpcn3lem  26724  cxpaddlelem  26728  cxpaddle  26729  cxpeq  26734  asinsinb  26874  acoscosb  26875  atantanb  26901  wilthlem2  27046  sqf11  27116  sqff1o  27159  ppiublem1  27179  lgsdir  27309  lgsne0  27312  lgsquadlem3  27359  2sqblem  27408  dchrisum0flblem1  27485  ostth3  27615  ostth  27616  noseponlem  27642  nodenselem4  27665  nodenselem5  27666  nodenselem7  27668  nodenselem8  27669  nolt02o  27673  nogt01o  27674  nosupbnd2lem1  27693  noetasuplem4  27714  lesrec  27805  madebdayim  27894  negsproplem2  28035  negsunif  28061  negleft  28064  negright  28065  lemuls1ad  28188  precsexlem6  28218  precsexlem7  28219  noseqp1  28297  om2noseqlt  28305  noseqrdgfn  28312  bdayn0sf1o  28376  dfnns2  28378  bdayfinbndlem1  28473  colinearalg  28993  axcontlem5  29051  axcontlem9  29055  uhgrn0  29150  upgrfn  29170  umgrfn  29182  uvtxnbgrvtx  29476  vtxduhgr0nedg  29576  pthdivtx  29810  iswwlksnx  29923  wpthswwlks2on  30047  clwwlkn  30111  clwwlknonwwlknonb  30191  eupth2lem2  30304  eupth2lem3lem6  30318  htthlem  31003  pjpreeq  31484  h1dn0  31638  spansneleqi  31655  rnbra  32193  dfpjop  32268  elpjrn  32276  stm1i  32329  mdbr2  32382  mdsl2i  32408  sumdmdlem  32504  dmdbr6ati  32509  ordtrest2NEWlem  34082  xrge0iifcnv  34093  eulerpartlemb  34528  onvf1odlem4  35304  erdszelem8  35396  cvmlift3lem4  35520  cvmlift3lem5  35521  fmlasucdisj  35597  mrsub0  35714  mrsubccat  35716  mrsubcn  35717  msubrn  35727  msrid  35743  elmthm  35774  dfon2lem9  35987  btwnconn1lem11  36295  broutsideof2  36320  opnbnd  36523  tailfb  36575  tr0elw  36682  tr0el  36683  bj-ideqg1  37494  fin2so  37942  lindsadd  37948  poimirlem9  37964  poimirlem17  37972  poimirlem26  37981  poimirlem27  37982  poimirlem31  37986  itgabsnc  38024  ftc2nc  38037  sdclem2  38077  subspopn  38087  equivtotbnd  38113  rngosn3  38259  igenval2  38401  isfldidl  38403  relcnveq3  38662  iss2  38679  elrelscnveq3  38962  lshpinN  39449  lsatcv0eq  39507  lsatcv1  39508  cvrnbtwn3  39736  cvrnbtwn4  39739  cvrcmp  39743  atnlt  39773  cvlexchb1  39790  2llnne2N  39868  atcvr0eq  39886  lnnat  39887  cvrat4  39903  ps-1  39937  3at  39950  llncmp  39982  llnnlt  39983  llncvrlpln2  40017  llncvrlpln  40018  lplncmp  40022  lplnnlt  40025  lplncvrlvol2  40075  lplncvrlvol  40076  lvolcmp  40077  lvolnltN  40078  dalempnes  40111  dalemqnet  40112  dalem-cly  40131  dalem44  40176  lncmp  40243  cdlemblem  40253  llnexch2N  40330  osumcllem4N  40419  pexmidlem1N  40430  lhp2atnle  40493  cdleme11dN  40722  cdleme20k  40779  cdleme21at  40788  cdleme21ct  40789  cdleme32e  40905  cdleme35f  40914  tendoex  41435  dochexmidlem1  41920  lcfrlem9  42010  mapd1o  42108  mapdindp3  42182  zndvdchrrhm  42426  elre0re  42707  mullt0b2d  42943  flt0  43084  ismrc  43147  pellexlem1  43275  aomclem4  43503  dfac21  43512  lsmfgcl  43520  lmhmfgima  43530  dfacbasgrp  43554  hbtlem6  43575  fiuneneq  43638  oaabsb  43740  cantnfresb  43770  orbitcl  45402  stoweidlem27  46473  stoweidlem29  46475  fcoresf1  47529  tz6.12c-afv2  47702  dfatbrafv2b  47705  fnbrafv2b  47708  iccpartrn  47902  prmdvdsfmtnof1lem2  48060  mod42tp1mod8  48077  isubgredg  48354  grimuhgr  48375  grimcnv  48376  isuspgrim0  48382  assintopass  48702  rrxsphere  49236