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  3646  mob2  3674  rmob  3841  sneqrg  4791  preq1b  4798  prel12g  4816  disjxun  5089  sotric  5554  sotrieq  5555  iss  5984  poirr2  6071  xp11  6122  nordeq  6325  nsuceq0  6391  ordequn  6411  fnbrfvb  6872  2f1fvneq  7194  foeqcnvco  7234  f1eqcocnv  7235  dfwe2  7707  releldmdifi  7977  mposn  8033  poxp2  8073  poxp3  8080  poseq  8088  tfrlem15  8311  tz7.44-2  8326  tz7.48-1  8362  tz7.49  8364  oawordexr  8471  oewordi  8506  oeeulem  8516  nna0r  8524  nnawordex  8552  nnaordex  8553  nnaordex2  8554  oaabs  8563  oaabs2  8564  eldifsucnn  8579  elecex  8672  ectocld  8706  ecoptocl  8731  mapsnd  8810  eqeng  8908  difsnen  8972  fopwdom  8998  nneneq  9115  frfi  9169  elfiun  9314  ordiso  9402  ordtypelem7  9410  wemaplem2  9433  suc11reg  9509  inf3lem6  9523  noinfep  9550  cantnff  9564  cantnfp1lem2  9569  cantnfp1lem3  9570  cantnflem1  9579  cantnf  9583  ttrcltr  9606  r111  9668  rankc2  9764  tcrank  9777  cardnueq0  9857  fodomfi2  9951  alephinit  9986  dfac9  10028  dfac12k  10039  djuinf  10080  ackbij1  10128  ackbij2  10133  sornom  10168  fin23lem16  10226  fin23lem21  10230  isf32lem2  10245  fin1a2lem6  10296  itunitc  10312  zorn2lem4  10390  wunr1om  10610  tskr1om  10658  recmulnq  10855  ltexnq  10866  distrlem4pr  10917  1re  11112  0re  11114  0cnALT  11348  0cnALT2  11349  mulge0  11635  prodgt0  11968  peano2nn  12137  recnz  12548  zneo  12556  uzn0  12749  xlemul1a  13187  prunioo  13381  flidz  13714  ceilidz  13756  modid2  13802  modmuladdnn0  13822  om2uzrani  13859  uzrdgfni  13865  seqid  13954  seqz  13957  facdiv  14194  facwordi  14196  hashdom  14286  wrdnval  14452  wrdnfi  14455  wrdl1s1  14522  sqrmo  15158  fsumf1o  15630  isumltss  15755  supcvg  15763  dvdsnegb  16184  dvdsexp2im  16238  odd2np1lem  16251  odd2np1  16252  ltoddhalfle  16272  halfleoddlt  16273  opoe  16274  omoe  16275  opeo  16276  omeo  16277  bitsuz  16385  bezoutlem4  16453  gcddiv  16462  gcdzeq  16463  dvdssqim  16465  dvdsexpim  16466  lcmgcdeq  16523  coprmdvds2  16565  rpmul  16570  divgcdcoprmex  16577  cncongr2  16579  dvdsprm  16614  coprm  16622  prmdvdsexp  16626  prmdiv  16696  pythagtriplem19  16745  pc2dvds  16791  pcadd  16801  prmpwdvds  16816  vdwlem11  16903  ramubcl  16930  0ram  16932  posasymb  18225  pleval2  18241  pltval3  18243  plttr  18246  pospo  18249  letsr  18499  intopsn  18562  ismgmid  18573  imasmnd2  18682  isgrpid2  18889  isgrpinv  18906  dfgrp3lem  18951  imasgrp2  18968  orbsta  19226  symgfix2  19329  pmtrfrn  19371  pmtrrn2  19373  odmulg  19469  odmulgeq  19470  gexdvdsi  19496  gexnnod  19501  pgpssslw  19527  sylow2alem1  19530  fislw  19538  lsmss1b  19579  lsmss2b  19581  efgrelexlemb  19663  torsubg  19767  ablfacrplem  19980  pgpfac1lem2  19990  pgpfac1lem3  19992  ablsimpnosubgd  20019  imasrng  20096  imasring  20249  dvdsrcl2  20285  dvdsrtr  20287  dvdsrmul1  20288  irredn0  20342  lspsneq0  20946  lmhmima  20982  lspsolv  21081  xrsdsreclblem  21350  dvdsrzring  21399  prmirredlem  21410  znunit  21501  pjdm2  21649  obselocv  21666  lindfrn  21759  opsrtoslem2  21992  mpfind  22043  psdmul  22082  mpfpf1  22267  pf1mpf  22268  cpmadugsumlemF  22792  baspartn  22870  bastop  22897  iscld3  22980  isopn3  22982  iscldtop  23011  ordtrest2lem  23119  2ndcredom  23366  2ndc1stc  23367  2ndcrest  23370  2ndcdisj  23372  2ndcsep  23375  kgenidm  23463  dfac14  23534  tx2ndc  23567  kqreglem1  23657  rnelfm  23869  fmfnfmlem2  23871  fmfnfmlem4  23873  fmfnfm  23874  flimtopon  23886  fclstopon  23928  xrsmopn  24729  icccmplem2  24740  reconnlem1  24743  iccpnfcnv  24870  cphsqrtcl2  25114  ivthlem3  25382  ivthicc  25387  ovolctb  25419  ioombl  25494  itgabs  25764  itgsplitioo  25767  dvlip  25926  c1liplem1  25929  c1lip1  25930  dvgt0lem1  25935  dvivthlem2  25942  dvne0  25944  lhop1lem  25946  lhop1  25947  lhop2  25948  lhop  25949  dvcvx  25953  itgsubstlem  25983  mdegnn0cl  26004  ig1peu  26108  elply2  26129  plypf1  26145  dgreq0  26199  aannenlem3  26266  abelthlem2  26370  lognegb  26527  eflogeq  26539  efopn  26595  cxpge0  26620  cxplea  26633  cxple2  26634  cxpcn3lem  26685  cxpaddlelem  26689  cxpaddle  26690  cxpeq  26695  asinsinb  26835  acoscosb  26836  atantanb  26862  wilthlem2  27007  sqf11  27077  sqff1o  27120  ppiublem1  27141  lgsdir  27271  lgsne0  27274  lgsquadlem3  27321  2sqblem  27370  dchrisum0flblem1  27447  ostth3  27577  ostth  27578  noseponlem  27604  nodenselem4  27627  nodenselem5  27628  nodenselem7  27630  nodenselem8  27631  nolt02o  27635  nogt01o  27636  nosupbnd2lem1  27655  noetasuplem4  27676  slerec  27761  madebdayim  27834  negsproplem2  27972  negsunif  27998  slemul1ad  28122  precsexlem6  28151  precsexlem7  28152  noseqp1  28222  om2noseqlt  28230  noseqrdgfn  28237  bdayn0sf1o  28296  dfnns2  28298  colinearalg  28889  axcontlem5  28947  axcontlem9  28951  uhgrn0  29046  upgrfn  29066  umgrfn  29078  uvtxnbgrvtx  29372  vtxduhgr0nedg  29472  pthdivtx  29706  iswwlksnx  29819  wpthswwlks2on  29940  clwwlkn  30004  clwwlknonwwlknonb  30084  eupth2lem2  30197  eupth2lem3lem6  30211  htthlem  30895  pjpreeq  31376  h1dn0  31530  spansneleqi  31547  rnbra  32085  dfpjop  32160  elpjrn  32168  stm1i  32221  mdbr2  32274  mdsl2i  32300  sumdmdlem  32396  dmdbr6ati  32401  ordtrest2NEWlem  33933  xrge0iifcnv  33944  eulerpartlemb  34379  onvf1odlem4  35148  erdszelem8  35240  cvmlift3lem4  35364  cvmlift3lem5  35365  fmlasucdisj  35441  mrsub0  35558  mrsubccat  35560  mrsubcn  35561  msubrn  35571  msrid  35587  elmthm  35618  dfon2lem9  35831  btwnconn1lem11  36137  broutsideof2  36162  opnbnd  36365  tailfb  36417  bj-ideqg1  37204  fin2so  37653  lindsadd  37659  poimirlem9  37675  poimirlem17  37683  poimirlem26  37692  poimirlem27  37693  poimirlem31  37697  itgabsnc  37735  ftc2nc  37748  sdclem2  37788  subspopn  37798  equivtotbnd  37824  rngosn3  37970  igenval2  38112  isfldidl  38114  relcnveq3  38361  iss2  38378  elrelscnveq3  38534  lshpinN  39034  lsatcv0eq  39092  lsatcv1  39093  cvrnbtwn3  39321  cvrnbtwn4  39324  cvrcmp  39328  atnlt  39358  cvlexchb1  39375  2llnne2N  39453  atcvr0eq  39471  lnnat  39472  cvrat4  39488  ps-1  39522  3at  39535  llncmp  39567  llnnlt  39568  llncvrlpln2  39602  llncvrlpln  39603  lplncmp  39607  lplnnlt  39610  lplncvrlvol2  39660  lplncvrlvol  39661  lvolcmp  39662  lvolnltN  39663  dalempnes  39696  dalemqnet  39697  dalem-cly  39716  dalem44  39761  lncmp  39828  cdlemblem  39838  llnexch2N  39915  osumcllem4N  40004  pexmidlem1N  40015  lhp2atnle  40078  cdleme11dN  40307  cdleme20k  40364  cdleme21at  40373  cdleme21ct  40374  cdleme32e  40490  cdleme35f  40499  tendoex  41020  dochexmidlem1  41505  lcfrlem9  41595  mapd1o  41693  mapdindp3  41767  zndvdchrrhm  42011  elre0re  42293  mullt0b2d  42523  flt0  42676  ismrc  42740  pellexlem1  42868  aomclem4  43096  dfac21  43105  lsmfgcl  43113  lmhmfgima  43123  dfacbasgrp  43147  hbtlem6  43168  fiuneneq  43231  oaabsb  43333  cantnfresb  43363  orbitcl  44996  stoweidlem27  46071  stoweidlem29  46073  fcoresf1  47106  tz6.12c-afv2  47279  dfatbrafv2b  47282  fnbrafv2b  47285  iccpartrn  47467  prmdvdsfmtnof1lem2  47622  mod42tp1mod8  47639  isubgredg  47903  grimuhgr  47924  grimcnv  47925  isuspgrim0  47931  assintopass  48251  rrxsphere  48786