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  2910  rmob  3047  preqr1g  3753  issod  4304  sotritrieq  4310  nsuceq0g  4403  suctr  4406  nordeq  4528  suc11g  4541  iss  4937  poirr2  5003  xp11m  5049  tz6.12c  5526  fnbrfvb  5537  fvelimab  5552  foeqcnvco  5769  f1eqcocnv  5770  acexmidlemcase  5848  nna0r  6457  nnawordex  6508  ectocld  6579  ecoptocl  6600  mapsn  6668  eqeng  6744  fopwdom  6814  ordiso  7013  ltexnqq  7370  nsmallnqq  7374  nqprloc  7507  aptiprleml  7601  map2psrprg  7767  0re  7920  lttri3  7999  0cnALT  8109  reapti  8498  recnz  9305  zneo  9313  uzn0  9502  flqidz  10242  ceilqidz  10272  modqid2  10307  modqmuladdnn0  10324  frec2uzrand  10361  frecuzrdgtcl  10368  seq3id  10464  seq3z  10467  facdiv  10672  facwordi  10674  maxleb  11180  fsumf1o  11353  dvdsnegb  11770  odd2np1lem  11831  odd2np1  11832  ltoddhalfle  11852  halfleoddlt  11853  opoe  11854  omoe  11855  opeo  11856  omeo  11857  gcddiv  11974  gcdzeq  11977  dvdssqim  11979  lcmgcdeq  12037  coprmdvds2  12047  rpmul  12052  divgcdcoprmex  12056  cncongr2  12058  dvdsprm  12091  coprm  12098  prmdvdsexp  12102  prmdiv  12189  pythagtriplem19  12236  pc2dvds  12283  pcadd  12293  prmpwdvds  12307  exmidunben  12381  intopsn  12621  ismgmid  12631  isgrpid2  12743  isgrpinv  12756  baspartn  12842  bastop  12869  isopn3  12919  lgsdir  13730  lgsne0  13733  bj-peano4  13990  sbthomlem  14057