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  2983  rmob  3122  preqr1g  3844  issod  4411  sotritrieq  4417  nsuceq0g  4510  suctr  4513  nordeq  4637  suc11g  4650  iss  5054  poirr2  5124  xp11m  5170  tz6.12c  5662  fnbrfvb  5677  fvelimab  5695  foeqcnvco  5923  f1eqcocnv  5924  acexmidlemcase  6005  nna0r  6637  nnawordex  6688  ectocld  6761  ecoptocl  6782  mapsn  6850  eqeng  6930  fopwdom  7010  ordiso  7219  ltexnqq  7611  nsmallnqq  7615  nqprloc  7748  aptiprleml  7842  map2psrprg  8008  0re  8162  lttri3  8242  0cnALT  8352  reapti  8742  recnz  9556  zneo  9564  uzn0  9755  flqidz  10523  ceilqidz  10555  modqid2  10590  modqmuladdnn0  10607  frec2uzrand  10644  frecuzrdgtcl  10651  seq3id  10764  seq3z  10767  facdiv  10977  facwordi  10979  wrdnval  11120  wrdl1s1  11183  maxleb  11748  fsumf1o  11922  dvdsnegb  12340  odd2np1lem  12404  odd2np1  12405  ltoddhalfle  12425  halfleoddlt  12426  opoe  12427  omoe  12428  opeo  12429  omeo  12430  gcddiv  12561  gcdzeq  12564  dvdssqim  12566  lcmgcdeq  12626  coprmdvds2  12636  rpmul  12641  divgcdcoprmex  12645  cncongr2  12647  dvdsprm  12680  coprm  12687  prmdvdsexp  12691  prmdiv  12778  pythagtriplem19  12826  pc2dvds  12874  pcadd  12884  prmpwdvds  12899  exmidunben  13018  intopsn  13421  ismgmid  13431  imasmnd2  13506  isgrpid2  13594  isgrpinv  13608  dfgrp3mlem  13652  imasgrp2  13668  imasrng  13940  imasring  14048  dvdsrcl2  14084  dvdsrtr  14086  dvdsrmul1  14087  lspsneq0  14411  dvdsrzring  14588  znunit  14644  baspartn  14745  bastop  14770  isopn3  14820  lgsdir  15735  lgsne0  15738  lgsquadlem3  15779  uhgrm  15899  upgrfnen  15919  umgrfnen  15929  bj-peano4  16427  sbthomlem  16507