Theorem syl5ibrcom 157

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

Hypotheses

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

Assertion

Ref	Expression
syl5ibrcom	⊢ (𝜑 → (𝜒 → 𝜓))

Proof of Theorem syl5ibrcom

Step	Hyp	Ref	Expression
1		imbitrrid.1	. . 3 ⊢ (𝜑 → 𝜃)
2		imbitrrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	imbitrrid 156	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
4	3	com12 30	1 ⊢ (𝜑 → (𝜒 → 𝜓))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimprcd  160  elsn2g  3742  preqr1g  3891  opth1  4378  euotd  4397  tz7.2  4501  reusv3  4608  alxfr  4609  reuhypd  4619  ordsucim  4649  suc11g  4706  nlimsucg  4715  xpsspw  4889  funcnvuni  5453  fvmptdv2  5798  fsn  5883  fconst2g  5933  funfvima  5953  foco2  5962  isores3  6024  riotaeqimp  6066  eusvobj2  6074  ovmpodv2  6225  ovelrn  6241  f1opw2  6299  suppssov1  6302  suppssfvg  6507  nnmordi  6793  nnmord  6794  qsss  6872  eroveu  6904  th3qlem1  6915  mapsncnv  6982  elixpsn  7022  ixpsnf1o  7023  en1bg  7092  pw2f1odclem  7139  mapxpen  7153  mapunen  7156  en1eqsnbi  7272  updjud  7429  addnidpig  7710  enq0tr  7808  prcdnql  7858  prcunqu  7859  genipv  7883  genpelvl  7886  genpelvu  7887  distrlem5prl  7960  distrlem5pru  7961  aptiprlemu  8014  mulrid  8330  ltne  8417  cnegex  8512  creur  9298  creui  9299  cju  9300  nnsub  9353  un0addcl  9608  un0mulcl  9609  zaddcl  9696  elz2  9728  qmulz  10040  qre  10042  qnegcl  10053  elpqb  10068  xrltne  10233  xlesubadd  10303  iccid  10345  fzsn  10490  fzsuc2  10504  fz1sbc  10521  elfzp12  10524  modqmuladd  10825  bcval5  11224  bcpasc  11227  hashprg  11272  hashfzo  11286  wrdl1s1  11421  cats1un  11516  swrdccat3blem  11534  shftlem  11604  replim  11647  sqrtsq  11833  absle  11879  maxabslemval  11998  negfi  12018  xrmaxiflemval  12042  summodclem2  12175  summodc  12176  zsumdc  12177  fsum3  12180  fsummulc2  12241  fsum00  12255  isumsplit  12284  prodmodclem2  12370  prodmodc  12371  zproddc  12372  fprodseq  12376  prodsnf  12385  fzo0dvdseq  12650  divalgmod  12720  gcdabs1  12792  dvdsgcd  12815  dvdsmulgcd  12828  lcmgcdeq  12887  isprm2lem  12920  dvdsprime  12926  coprm  12949  prmdvdsexpr  12955  rpexp  12958  phibndlem  13024  dfphi2  13028  hashgcdlem  13046  odzdvds  13054  nnoddn2prm  13069  pythagtriplem1  13074  pceulem  13103  pcqmul  13112  pcqcl  13115  pcxnn0cl  13119  pcxcl  13120  pcneg  13134  pcabs  13135  pcgcd1  13137  pcz  13141  pcprmpw2  13142  pcprmpw  13143  dvdsprmpweqle  13146  difsqpwdvds  13147  pcaddlem  13148  pcadd  13149  pcmpt  13152  pockthg  13166  4sqlem2  13198  4sqlem4  13201  mul4sq  13203  prmlem1a  13251  ballotfilemfc0  13291  ballotfilemfcc  13292  mnd1id  13823  0subm  13851  mulgnn0p1  13996  mulgnn0ass  14021  dvreq1  14559  nzrunit  14605  rrgeq0  14683  domneq0  14691  lmodfopnelem2  14772  lss1d  14830  lspsneq0  14873  gsumfsum  15033  znidom  15102  znunit  15104  znrrg  15105  istopon  15251  eltg3  15295  tgidm  15312  restbasg  15406  tgrest  15407  tgcn  15446  cnconst  15472  lmss  15484  txbas  15496  txbasval  15505  upxp  15510  blssps  15665  blss  15666  metrest  15744  blssioo  15791  elcncf1di  15817  elply2  15973  plyf  15975  efnthr  16188  dvdsppwf1o  16295  ppiublem1  16303  chtublem  16307  perfectlem2  16312  perfect  16313  bposlem1  16323  lgsmod  16362  lgsne0  16374  lgsdirnn0  16383  gausslemma2dlem1a  16394  gausslemma2dlem6  16403  lgseisenlem2  16407  lgsquadlem1  16413  lgsquadlem2  16414  2lgslem1b  16425  2sqlem2  16451  mul2sq  16452  2sqlem7  16457  lpvtx  16537  usgredgop  16631  uhgrspansubgrlem  16734  vtxd0nedgbfi  16757  wlk1walkdom  16817  upgrwlkvtxedg  16822  clwwlkext2edg  16880  clwwlknonccat  16891  bj-peano4  17198