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  3642  mob2  3670  rmob  3837  sneqrg  4792  preq1b  4799  prel12g  4817  disjxun  5093  sotric  5559  sotrieq  5560  iss  5990  poirr2  6077  xp11  6129  nordeq  6332  nsuceq0  6398  ordequn  6418  fnbrfvb  6880  2f1fvneq  7202  foeqcnvco  7242  f1eqcocnv  7243  dfwe2  7715  releldmdifi  7985  mposn  8041  poxp2  8081  poxp3  8088  poseq  8096  tfrlem15  8319  tz7.44-2  8334  tz7.48-1  8370  tz7.49  8372  oawordexr  8479  oewordi  8514  oeeulem  8524  nna0r  8532  nnawordex  8560  nnaordex  8561  nnaordex2  8562  oaabs  8571  oaabs2  8572  eldifsucnn  8587  elecex  8680  ectocld  8714  ecoptocl  8739  mapsnd  8818  eqeng  8917  difsnen  8981  fopwdom  9007  nneneq  9124  frfi  9178  elfiun  9323  ordiso  9411  ordtypelem7  9419  wemaplem2  9442  suc11reg  9518  inf3lem6  9532  noinfep  9559  cantnff  9573  cantnfp1lem2  9578  cantnfp1lem3  9579  cantnflem1  9588  cantnf  9592  ttrcltr  9615  r111  9677  rankc2  9773  tcrank  9786  cardnueq0  9866  fodomfi2  9960  alephinit  9995  dfac9  10037  dfac12k  10048  djuinf  10089  ackbij1  10137  ackbij2  10142  sornom  10177  fin23lem16  10235  fin23lem21  10239  isf32lem2  10254  fin1a2lem6  10305  itunitc  10321  zorn2lem4  10399  wunr1om  10619  tskr1om  10667  recmulnq  10864  ltexnq  10875  distrlem4pr  10926  1re  11121  0re  11123  0cnALT  11357  0cnALT2  11358  mulge0  11644  prodgt0  11977  peano2nn  12146  recnz  12556  zneo  12564  uzn0  12757  xlemul1a  13191  prunioo  13385  flidz  13718  ceilidz  13760  modid2  13806  modmuladdnn0  13826  om2uzrani  13863  uzrdgfni  13869  seqid  13958  seqz  13961  facdiv  14198  facwordi  14200  hashdom  14290  wrdnval  14456  wrdnfi  14459  wrdl1s1  14526  sqrmo  15162  fsumf1o  15634  isumltss  15759  supcvg  15767  dvdsnegb  16188  dvdsexp2im  16242  odd2np1lem  16255  odd2np1  16256  ltoddhalfle  16276  halfleoddlt  16277  opoe  16278  omoe  16279  opeo  16280  omeo  16281  bitsuz  16389  bezoutlem4  16457  gcddiv  16466  gcdzeq  16467  dvdssqim  16469  dvdsexpim  16470  lcmgcdeq  16527  coprmdvds2  16569  rpmul  16574  divgcdcoprmex  16581  cncongr2  16583  dvdsprm  16618  coprm  16626  prmdvdsexp  16630  prmdiv  16700  pythagtriplem19  16749  pc2dvds  16795  pcadd  16805  prmpwdvds  16820  vdwlem11  16907  ramubcl  16934  0ram  16936  posasymb  18229  pleval2  18245  pltval3  18247  plttr  18250  pospo  18253  letsr  18503  intopsn  18566  ismgmid  18577  imasmnd2  18686  isgrpid2  18893  isgrpinv  18910  dfgrp3lem  18955  imasgrp2  18972  orbsta  19229  symgfix2  19332  pmtrfrn  19374  pmtrrn2  19376  odmulg  19472  odmulgeq  19473  gexdvdsi  19499  gexnnod  19504  pgpssslw  19530  sylow2alem1  19533  fislw  19541  lsmss1b  19582  lsmss2b  19584  efgrelexlemb  19666  torsubg  19770  ablfacrplem  19983  pgpfac1lem2  19993  pgpfac1lem3  19995  ablsimpnosubgd  20022  imasrng  20099  imasring  20252  dvdsrcl2  20288  dvdsrtr  20290  dvdsrmul1  20291  irredn0  20345  lspsneq0  20949  lmhmima  20985  lspsolv  21084  xrsdsreclblem  21353  dvdsrzring  21402  prmirredlem  21413  znunit  21504  pjdm2  21652  obselocv  21669  lindfrn  21762  opsrtoslem2  21994  mpfind  22045  psdmul  22084  mpfpf1  22269  pf1mpf  22270  cpmadugsumlemF  22794  baspartn  22872  bastop  22899  iscld3  22982  isopn3  22984  iscldtop  23013  ordtrest2lem  23121  2ndcredom  23368  2ndc1stc  23369  2ndcrest  23372  2ndcdisj  23374  2ndcsep  23377  kgenidm  23465  dfac14  23536  tx2ndc  23569  kqreglem1  23659  rnelfm  23871  fmfnfmlem2  23873  fmfnfmlem4  23875  fmfnfm  23876  flimtopon  23888  fclstopon  23930  xrsmopn  24731  icccmplem2  24742  reconnlem1  24745  iccpnfcnv  24872  cphsqrtcl2  25116  ivthlem3  25384  ivthicc  25389  ovolctb  25421  ioombl  25496  itgabs  25766  itgsplitioo  25769  dvlip  25928  c1liplem1  25931  c1lip1  25932  dvgt0lem1  25937  dvivthlem2  25944  dvne0  25946  lhop1lem  25948  lhop1  25949  lhop2  25950  lhop  25951  dvcvx  25955  itgsubstlem  25985  mdegnn0cl  26006  ig1peu  26110  elply2  26131  plypf1  26147  dgreq0  26201  aannenlem3  26268  abelthlem2  26372  lognegb  26529  eflogeq  26541  efopn  26597  cxpge0  26622  cxplea  26635  cxple2  26636  cxpcn3lem  26687  cxpaddlelem  26691  cxpaddle  26692  cxpeq  26697  asinsinb  26837  acoscosb  26838  atantanb  26864  wilthlem2  27009  sqf11  27079  sqff1o  27122  ppiublem1  27143  lgsdir  27273  lgsne0  27276  lgsquadlem3  27323  2sqblem  27372  dchrisum0flblem1  27449  ostth3  27579  ostth  27580  noseponlem  27606  nodenselem4  27629  nodenselem5  27630  nodenselem7  27632  nodenselem8  27633  nolt02o  27637  nogt01o  27638  nosupbnd2lem1  27657  noetasuplem4  27678  slerec  27763  madebdayim  27836  negsproplem2  27974  negsunif  28000  slemul1ad  28124  precsexlem6  28153  precsexlem7  28154  noseqp1  28224  om2noseqlt  28232  noseqrdgfn  28239  bdayn0sf1o  28298  dfnns2  28300  colinearalg  28892  axcontlem5  28950  axcontlem9  28954  uhgrn0  29049  upgrfn  29069  umgrfn  29081  uvtxnbgrvtx  29375  vtxduhgr0nedg  29475  pthdivtx  29709  iswwlksnx  29822  wpthswwlks2on  29946  clwwlkn  30010  clwwlknonwwlknonb  30090  eupth2lem2  30203  eupth2lem3lem6  30217  htthlem  30901  pjpreeq  31382  h1dn0  31536  spansneleqi  31553  rnbra  32091  dfpjop  32166  elpjrn  32174  stm1i  32227  mdbr2  32280  mdsl2i  32306  sumdmdlem  32402  dmdbr6ati  32407  ordtrest2NEWlem  33958  xrge0iifcnv  33969  eulerpartlemb  34404  onvf1odlem4  35173  erdszelem8  35265  cvmlift3lem4  35389  cvmlift3lem5  35390  fmlasucdisj  35466  mrsub0  35583  mrsubccat  35585  mrsubcn  35586  msubrn  35596  msrid  35612  elmthm  35643  dfon2lem9  35856  btwnconn1lem11  36164  broutsideof2  36189  opnbnd  36392  tailfb  36444  bj-ideqg1  37231  fin2so  37670  lindsadd  37676  poimirlem9  37692  poimirlem17  37700  poimirlem26  37709  poimirlem27  37710  poimirlem31  37714  itgabsnc  37752  ftc2nc  37765  sdclem2  37805  subspopn  37815  equivtotbnd  37841  rngosn3  37987  igenval2  38129  isfldidl  38131  relcnveq3  38382  iss2  38399  elrelscnveq3  38662  lshpinN  39111  lsatcv0eq  39169  lsatcv1  39170  cvrnbtwn3  39398  cvrnbtwn4  39401  cvrcmp  39405  atnlt  39435  cvlexchb1  39452  2llnne2N  39530  atcvr0eq  39548  lnnat  39549  cvrat4  39565  ps-1  39599  3at  39612  llncmp  39644  llnnlt  39645  llncvrlpln2  39679  llncvrlpln  39680  lplncmp  39684  lplnnlt  39687  lplncvrlvol2  39737  lplncvrlvol  39738  lvolcmp  39739  lvolnltN  39740  dalempnes  39773  dalemqnet  39774  dalem-cly  39793  dalem44  39838  lncmp  39905  cdlemblem  39915  llnexch2N  39992  osumcllem4N  40081  pexmidlem1N  40092  lhp2atnle  40155  cdleme11dN  40384  cdleme20k  40441  cdleme21at  40450  cdleme21ct  40451  cdleme32e  40567  cdleme35f  40576  tendoex  41097  dochexmidlem1  41582  lcfrlem9  41672  mapd1o  41770  mapdindp3  41844  zndvdchrrhm  42088  elre0re  42375  mullt0b2d  42605  flt0  42758  ismrc  42821  pellexlem1  42949  aomclem4  43177  dfac21  43186  lsmfgcl  43194  lmhmfgima  43204  dfacbasgrp  43228  hbtlem6  43249  fiuneneq  43312  oaabsb  43414  cantnfresb  43444  orbitcl  45077  stoweidlem27  46152  stoweidlem29  46154  fcoresf1  47196  tz6.12c-afv2  47369  dfatbrafv2b  47372  fnbrafv2b  47375  iccpartrn  47557  prmdvdsfmtnof1lem2  47712  mod42tp1mod8  47729  isubgredg  47993  grimuhgr  48014  grimcnv  48015  isuspgrim0  48021  assintopass  48341  rrxsphere  48876