Theorem syl5ibcom 154

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

Hypotheses

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

Assertion

Ref	Expression
syl5ibcom	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem syl5ibcom

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpcd  158  mob2  2892  rmob  3029  preqr1g  3731  issod  4281  sotritrieq  4287  nsuceq0g  4380  suctr  4383  nordeq  4505  suc11g  4518  iss  4914  poirr2  4980  xp11m  5026  tz6.12c  5500  fnbrfvb  5511  fvelimab  5526  foeqcnvco  5742  f1eqcocnv  5743  acexmidlemcase  5821  nna0r  6427  nnawordex  6477  ectocld  6548  ecoptocl  6569  mapsn  6637  eqeng  6713  fopwdom  6783  ordiso  6982  ltexnqq  7330  nsmallnqq  7334  nqprloc  7467  aptiprleml  7561  map2psrprg  7727  0re  7880  lttri3  7959  0cnALT  8069  reapti  8458  recnz  9262  zneo  9270  uzn0  9459  flqidz  10194  ceilqidz  10224  modqid2  10259  modqmuladdnn0  10276  frec2uzrand  10313  frecuzrdgtcl  10320  seq3id  10416  seq3z  10419  facdiv  10623  facwordi  10625  maxleb  11127  fsumf1o  11298  dvdsnegb  11715  odd2np1lem  11775  odd2np1  11776  ltoddhalfle  11796  halfleoddlt  11797  opoe  11798  omoe  11799  opeo  11800  omeo  11801  gcddiv  11918  gcdzeq  11921  dvdssqim  11923  lcmgcdeq  11975  coprmdvds2  11985  rpmul  11990  divgcdcoprmex  11994  cncongr2  11996  dvdsprm  12029  coprm  12034  prmdvdsexp  12038  prmdiv  12125  pythagtriplem19  12172  exmidunben  12225  baspartn  12518  bastop  12545  isopn3  12595  bj-peano4  13601  sbthomlem  13667