Theorem syl5ibcom 144

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

Syntax hints:   → wi 4   ↔ wb 98

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  biimpcd  148  mob2  2721  rmob  2850  preqr1g  3537  issod  4056  sotritrieq  4062  nsuceq0g  4155  suctr  4158  nordeq  4268  suc11g  4281  iss  4654  poirr2  4717  xp11m  4759  tz6.12c  5203  fnbrfvb  5214  fvelimab  5229  foeqcnvco  5430  f1eqcocnv  5431  acexmidlemcase  5507  nna0r  6057  nnawordex  6101  ectocld  6172  ecoptocl  6193  eqeng  6246  fopwdom  6310  ordiso  6358  ltexnqq  6506  nsmallnqq  6510  nqprloc  6643  aptiprleml  6737  0re  7027  lttri3  7098  0cnALT  7201  reapti  7570  recnz  8333  zneo  8339  uzn0  8488  flqidz  9128  ceilqidz  9158  frec2uzrand  9191  frecuzrdgfn  9198  iseqid  9247  bj-peano4  10080