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  4376  euotd  4395  tz7.2  4499  reusv3  4606  alxfr  4607  reuhypd  4617  ordsucim  4647  suc11g  4704  nlimsucg  4713  xpsspw  4887  funcnvuni  5450  fvmptdv2  5795  fsn  5880  fconst2g  5930  funfvima  5950  foco2  5959  isores3  6021  riotaeqimp  6063  eusvobj2  6071  ovmpodv2  6222  ovelrn  6238  f1opw2  6296  suppssov1  6299  suppssfvg  6503  nnmordi  6789  nnmord  6790  qsss  6868  eroveu  6900  th3qlem1  6911  mapsncnv  6977  elixpsn  7017  ixpsnf1o  7018  en1bg  7087  pw2f1odclem  7134  mapxpen  7148  mapunen  7151  en1eqsnbi  7266  updjud  7423  addnidpig  7704  enq0tr  7802  prcdnql  7852  prcunqu  7853  genipv  7877  genpelvl  7880  genpelvu  7881  distrlem5prl  7954  distrlem5pru  7955  aptiprlemu  8008  mulrid  8324  ltne  8411  cnegex  8506  creur  9292  creui  9293  cju  9294  nnsub  9346  un0addcl  9601  un0mulcl  9602  zaddcl  9689  elz2  9721  qmulz  10033  qre  10035  qnegcl  10046  elpqb  10061  xrltne  10226  xlesubadd  10296  iccid  10338  fzsn  10483  fzsuc2  10497  fz1sbc  10514  elfzp12  10517  modqmuladd  10817  bcval5  11216  bcpasc  11219  hashprg  11264  hashfzo  11278  wrdl1s1  11413  cats1un  11508  swrdccat3blem  11526  shftlem  11596  replim  11639  sqrtsq  11825  absle  11871  maxabslemval  11990  negfi  12010  xrmaxiflemval  12034  summodclem2  12167  summodc  12168  zsumdc  12169  fsum3  12172  fsummulc2  12233  fsum00  12247  isumsplit  12276  prodmodclem2  12362  prodmodc  12363  zproddc  12364  fprodseq  12368  prodsnf  12377  fzo0dvdseq  12642  divalgmod  12712  gcdabs1  12784  dvdsgcd  12807  dvdsmulgcd  12820  lcmgcdeq  12879  isprm2lem  12912  dvdsprime  12918  coprm  12941  prmdvdsexpr  12947  rpexp  12950  phibndlem  13016  dfphi2  13020  hashgcdlem  13038  odzdvds  13046  nnoddn2prm  13061  pythagtriplem1  13066  pceulem  13095  pcqmul  13104  pcqcl  13107  pcxnn0cl  13111  pcxcl  13112  pcneg  13126  pcabs  13127  pcgcd1  13129  pcz  13133  pcprmpw2  13134  pcprmpw  13135  dvdsprmpweqle  13138  difsqpwdvds  13139  pcaddlem  13140  pcadd  13141  pcmpt  13144  pockthg  13158  4sqlem2  13190  4sqlem4  13193  mul4sq  13195  prmlem1a  13243  ballotfilemfc0  13283  ballotfilemfcc  13284  mnd1id  13814  0subm  13842  mulgnn0p1  13987  mulgnn0ass  14012  dvreq1  14500  nzrunit  14546  rrgeq0  14624  domneq0  14632  lmodfopnelem2  14713  lss1d  14771  lspsneq0  14814  gsumfsum  14974  znidom  15043  znunit  15045  znrrg  15046  istopon  15166  eltg3  15210  tgidm  15227  restbasg  15321  tgrest  15322  tgcn  15361  cnconst  15387  lmss  15399  txbas  15411  txbasval  15420  upxp  15425  blssps  15580  blss  15581  metrest  15659  blssioo  15706  elcncf1di  15732  elply2  15888  plyf  15890  dvdsppwf1o  16205  ppiublem1  16213  chtublem  16217  perfectlem2  16222  perfect  16223  bposlem1  16233  lgsmod  16267  lgsne0  16279  lgsdirnn0  16288  gausslemma2dlem1a  16299  gausslemma2dlem6  16308  lgseisenlem2  16312  lgsquadlem1  16318  lgsquadlem2  16319  2lgslem1b  16330  2sqlem2  16356  mul2sq  16357  2sqlem7  16362  lpvtx  16442  usgredgop  16536  uhgrspansubgrlem  16639  vtxd0nedgbfi  16662  wlk1walkdom  16722  upgrwlkvtxedg  16727  clwwlkext2edg  16785  clwwlknonccat  16796  bj-peano4  17103