Theorem syl5ibcom 155

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

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimpcd  159  mob2  3000  rmob  3139  preqr1g  3875  issod  4445  sotritrieq  4451  nsuceq0g  4544  suctr  4547  nordeq  4671  suc11g  4684  iss  5089  poirr2  5160  xp11m  5206  tz6.12c  5705  fnbrfvb  5720  fvelimab  5738  foeqcnvco  5969  f1eqcocnv  5970  acexmidlemcase  6053  nna0r  6724  nnawordex  6775  ectocld  6848  ecoptocl  6869  mapsnd  6936  mapsn  6938  eqeng  7018  fopwdom  7102  ordiso  7340  ltexnqq  7739  nsmallnqq  7743  nqprloc  7876  aptiprleml  7970  map2psrprg  8136  0re  8290  lttri3  8369  0cnALT  8480  reapti  8871  recnz  9692  zneo  9700  uzn0  9891  flqidz  10673  ceilqidz  10705  modqid2  10740  modqmuladdnn0  10757  frec2uzrand  10794  frecuzrdgtcl  10801  seq3id  10914  seq3z  10917  facdiv  11128  facwordi  11130  wrdnval  11283  wrdl1s1  11346  maxleb  11930  fsumf1o  12105  dvdsnegb  12523  odd2np1lem  12587  odd2np1  12588  ltoddhalfle  12608  halfleoddlt  12609  opoe  12610  omoe  12611  opeo  12612  omeo  12613  gcddiv  12744  gcdzeq  12747  dvdssqim  12749  lcmgcdeq  12809  coprmdvds2  12819  rpmul  12824  divgcdcoprmex  12828  cncongr2  12830  dvdsprm  12863  coprm  12870  prmdvdsexp  12874  prmdiv  12961  pythagtriplem19  13009  pc2dvds  13057  pcadd  13067  prmpwdvds  13082  exmidunben  13265  intopsn  13634  ismgmid  13644  imasmnd2  13711  isgrpid2  13799  isgrpinv  13813  dfgrp3mlem  13857  imasgrp2  13867  imasrng  14199  imasring  14311  dvdsrcl2  14348  dvdsrtr  14350  dvdsrmul1  14351  lspsneq0  14704  dvdsrzring  14881  znunit  14937  baspartn  15045  bastop  15070  isopn3  15120  pellexlem1  15975  lgsdir  16038  lgsne0  16041  lgsquadlem3  16082  uhgrm  16203  upgrfnen  16223  umgrfnen  16233  eupth2lem2dc  16584  eupth2lem3lem6fi  16596  bj-peano4  16865  sbthomlem  16945