Theorem syl5ibcom 248

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 247	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	com12 33	1 ⊢ (𝜑 → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimpcd  252  elrab3t  3643  mob2  3672  rmob  3836  sneqrg  4793  preq1b  4800  prel12g  4818  disjxun  5100  sotric  5588  sotrieq  5589  iss  6026  poirr2  6117  xp11  6166  nordeq  6381  nsuceq0  6448  ordequn  6468  fnbrfvb  6936  2f1fvneq  7265  foeqcnvco  7309  f1eqcocnv  7310  dfwe2  7789  releldmdifi  8057  mposn  8117  poxp2  8163  poxp3  8170  poseq  8178  tfrlem15  8404  tz7.44-2  8419  tz7.48-1  8457  tz7.49  8459  oawordexr  8568  oewordi  8604  oeeulem  8614  nna0r  8622  nnawordex  8650  nnaordex  8651  nnaordex2  8652  oaabs  8661  oaabs2  8662  eldifsucnn  8677  elecex  8772  ectocld  8807  ecoptocl  8832  mapsnd  8918  eqeng  9017  difsnen  9082  fopwdom  9108  nneneq  9225  frfi  9280  elfiun  9426  ordiso  9514  ordtypelem7  9522  wemaplem2  9545  suc11reg  9624  inf3lem6  9638  noinfep  9665  cantnff  9679  cantnfp1lem2  9684  cantnfp1lem3  9685  cantnflem1  9694  cantnf  9698  ttrcltr  9721  r111  9786  rankc2  9892  tcrank  9905  cardnueq0  10049  fodomfi2  10143  alephinit  10178  dfac9  10219  dfac12k  10230  djuinf  10271  ackbij1  10319  ackbij2  10324  sornom  10359  fin23lem16  10417  fin23lem21  10421  isf32lem2  10436  fin1a2lem6  10487  itunitc  10503  zorn2lem4  10581  wunr1om  10808  tskr1om  10856  recmulnq  11053  ltexnq  11064  distrlem4pr  11115  1re  11312  0re  11314  0cnALT  11549  0cnALT2  11550  mulge0  11838  prodgt0  12168  peano2nn  12351  recnz  12778  zneo  12786  uzn0  12986  xlemul1a  13422  prunioo  13616  flidz  13954  ceilidz  13996  modid2  14042  modmuladdnn0  14062  om2uzrani  14099  uzrdgfni  14105  seqid  14194  seqz  14197  facdiv  14435  facwordi  14437  hashdom  14527  wrdnval  14694  wrdnfi  14697  wrdl1s1  14767  sqrmo  15424  fsumf1o  15895  isumltss  16023  supcvg  16031  dvdsnegb  16449  dvdsexp2im  16503  odd2np1lem  16516  odd2np1  16517  ltoddhalfle  16537  halfleoddlt  16538  opoe  16539  omoe  16540  opeo  16541  omeo  16542  bitsuz  16650  bezoutlem4  16721  gcddiv  16730  gcdzeq  16731  dvdssqim  16733  dvdsexpim  16734  lcmgcdeq  16793  coprmdvds2  16835  rpmul  16840  divgcdcoprmex  16847  cncongr2  16849  dvdsprm  16885  coprm  16893  prmdvdsexp  16897  prmdiv  16968  pythagtriplem19  17017  pc2dvds  17063  pcadd  17073  prmpwdvds  17088  vdwlem11  17175  ramubcl  17202  0ram  17204  posasymb  18499  pleval2  18515  pltval3  18517  plttr  18520  pospo  18523  letsr  18773  intopsn  18838  ismgmid  18851  imasmgm2  18869  imasmnd2  18974  isgrpid2  19193  isgrpinv  19210  dfgrp3lem  19254  imasgrp2  19271  orbsta  19533  symgfix2  19636  pmtrfrn  19678  pmtrrn2  19680  odmulg  19776  odmulgeq  19777  gexdvdsi  19803  gexnnod  19808  pgpssslw  19834  sylow2alem1  19837  fislw  19845  lsmss1b  19886  lsmss2b  19888  efgrelexlemb  19970  torsubg  20074  ablfacrplem  20287  pgpfac1lem2  20297  pgpfac1lem3  20299  ablsimpnosubgd  20326  imasrng  20405  imasring  20566  dvdsrcl2  20602  dvdsrtr  20604  dvdsrmul1  20605  irredn0  20659  lspsneq0  21293  lmhmima  21328  lspsolv  21427  rspprop  21530  xrsdsreclblem  21725  dvdsrzring  21773  prmirredlem  21784  znunit  21875  pjdm2  22023  obselocv  22040  lindfrn  22133  opsrtoslem2  22371  mpfind  22430  psdmul  22493  mpfpf1  22675  pf1mpf  22676  cpmadugsumlemF  23200  baspartn  23278  bastop  23305  iscld3  23388  isopn3  23390  iscldtop  23419  ordtrest2lem  23527  2ndcredom  23774  2ndc1stc  23775  2ndcrest  23778  2ndcdisj  23781  2ndcsep  23784  kgenidm  23872  dfac14  23943  tx2ndc  23976  kqreglem1  24066  rnelfm  24278  fmfnfmlem2  24280  fmfnfmlem4  24282  fmfnfm  24283  flimtopon  24295  fclstopon  24337  xrsmopn  25138  icccmplem2  25149  reconnlem1  25152  iccpnfcnv  25271  cphsqrtcl2  25513  ivthlem3  25780  ivthicc  25785  ovolctb  25817  ioombl  25892  itgabs  26161  itgsplitioo  26164  dvlip  26319  c1liplem1  26322  c1lip1  26323  dvgt0lem1  26328  dvivthlem2  26335  dvne0  26337  lhop1lem  26339  lhop1  26340  lhop2  26341  lhop  26342  dvcvx  26346  itgsubstlem  26374  mdegnn0cl  26395  ig1peu  26499  elply2  26520  plypf1  26537  dgreq0  26590  aannenlem3  26663  abelthlem2  26765  lognegb  26924  eflogeq  26936  efopn  26992  cxpge0  27017  cxplea  27030  cxple2  27031  cxpcn3lem  27081  cxpaddlelem  27085  cxpaddle  27086  cxpeq  27091  asinsinb  27231  acoscosb  27232  atantanb  27258  wilthlem2  27402  sqf11  27472  sqff1o  27515  ppiublem1  27535  lgsdir  27665  lgsne0  27668  lgsquadlem3  27715  2sqblem  27764  dchrisum0flblem1  27841  ostth3  27971  ostth  27972  flt0  27975  fltoprm  28001  noseponlem  28027  nodenselem4  28050  nodenselem5  28051  nodenselem7  28053  nodenselem8  28054  nolt02o  28058  nogt01o  28059  nosupbnd2lem1  28078  noetasuplem4  28099  lesrec  28191  madebdayim  28280  negsproplem2  28421  negsunif  28447  negleft  28450  negright  28451  lemuls1ad  28574  precsexlem6  28604  precsexlem7  28605  noseqp1  28683  om2noseqlt  28691  noseqrdgfn  28698  bdayn0sf1o  28762  dfnns2  28764  bdayfinbndlem1  28859  colinearalg  29494  axcontlem5  29552  axcontlem9  29556  uhgrn0  29651  upgrfn  29671  umgrfn  29683  uvtxnbgrvtx  29980  vtxduhgr0nedg  30079  pthdivtx  30318  iswwlksnx  30435  wpthswwlks2on  30559  clwwlkn  30623  clwwlknonwwlknonb  30703  eupth2lem2  30826  eupth2lem3lem6  30840  htthlem  31525  pjpreeq  32006  h1dn0  32160  spansneleqi  32177  rnbra  32715  dfpjop  32790  elpjrn  32798  stm1i  32851  mdbr2  32904  mdsl2i  32930  sumdmdlem  33026  dmdbr6ati  33031  ordtrest2NEWlem  34601  xrge0iifcnv  34612  eulerpartlemb  35047  maxssj0  35946  onvf1odlem4  35954  erdszelem8  36050  cvmlift3lem4  36174  cvmlift3lem5  36175  fmlasucdisj  36251  mrsub0  36368  mrsubccat  36370  mrsubcn  36371  msubrn  36381  msrid  36397  elmthm  36428  dfon2lem9  36646  btwnconn1lem11  36955  broutsideof2  36980  opnbnd  37206  tailfb  37258  tr0elw  37365  tr0el  37366  bj-ideqg1  38179  fin2so  38624  lindsadd  38630  poimirlem9  38641  poimirlem17  38649  poimirlem26  38658  poimirlem27  38659  poimirlem31  38663  itgabsnc  38701  ftc2nc  38714  sdclem2  38770  subspopn  38780  equivtotbnd  38806  rngosn3  38952  igenval2  39094  isfldidl  39096  relcnveq3  39353  iss2  39370  elrelscnveq3  39653  lshpinN  40140  lsatcv0eq  40198  lsatcv1  40199  cvrnbtwn3  40427  cvrnbtwn4  40430  cvrcmp  40434  atnlt  40464  cvlexchb1  40481  2llnne2N  40559  atcvr0eq  40577  lnnat  40578  cvrat4  40594  ps-1  40628  3at  40641  llncmp  40673  llnnlt  40674  llncvrlpln2  40708  llncvrlpln  40709  lplncmp  40713  lplnnlt  40716  lplncvrlvol2  40766  lplncvrlvol  40767  lvolcmp  40768  lvolnltN  40769  dalempnes  40802  dalemqnet  40803  dalem-cly  40822  dalem44  40867  lncmp  40934  cdlemblem  40944  llnexch2N  41021  osumcllem4N  41110  pexmidlem1N  41121  lhp2atnle  41184  cdleme11dN  41413  cdleme20k  41470  cdleme21at  41479  cdleme21ct  41480  cdleme32e  41596  cdleme35f  41605  tendoex  42126  dochexmidlem1  42611  lcfrlem9  42701  mapd1o  42799  mapdindp3  42873  zndvdchrrhm  43117  elre0re  43399  mullt0b2d  43642  ismrc  43806  pellexlem1  43930  aomclem4  44153  dfac21  44162  lsmfgcl  44170  lmhmfgima  44180  dfacbasgrp  44204  hbtlem6  44225  fiuneneq  44288  oaabsb  44390  cantnfresb  44420  orbitcl  46041  stoweidlem27  47131  stoweidlem29  47133  fcoresf1  48233  tz6.12c-afv2  48406  dfatbrafv2b  48409  fnbrafv2b  48412  iccpartrn  48606  prmdvdsfmtnof1lem2  48764  mod42tp1mod8  48781  isubgredg  49058  grimuhgr  49079  grimcnv  49080  isuspgrim0  49086  assintopass  49405  rrxsphere  49954