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  2917  rmob  3055  preqr1g  3766  issod  4319  sotritrieq  4325  nsuceq0g  4418  suctr  4421  nordeq  4543  suc11g  4556  iss  4953  poirr2  5021  xp11m  5067  tz6.12c  5545  fnbrfvb  5556  fvelimab  5572  foeqcnvco  5790  f1eqcocnv  5791  acexmidlemcase  5869  nna0r  6478  nnawordex  6529  ectocld  6600  ecoptocl  6621  mapsn  6689  eqeng  6765  fopwdom  6835  ordiso  7034  ltexnqq  7406  nsmallnqq  7410  nqprloc  7543  aptiprleml  7637  map2psrprg  7803  0re  7956  lttri3  8036  0cnALT  8146  reapti  8535  recnz  9345  zneo  9353  uzn0  9542  flqidz  10285  ceilqidz  10315  modqid2  10350  modqmuladdnn0  10367  frec2uzrand  10404  frecuzrdgtcl  10411  seq3id  10507  seq3z  10510  facdiv  10717  facwordi  10719  maxleb  11224  fsumf1o  11397  dvdsnegb  11814  odd2np1lem  11876  odd2np1  11877  ltoddhalfle  11897  halfleoddlt  11898  opoe  11899  omoe  11900  opeo  11901  omeo  11902  gcddiv  12019  gcdzeq  12022  dvdssqim  12024  lcmgcdeq  12082  coprmdvds2  12092  rpmul  12097  divgcdcoprmex  12101  cncongr2  12103  dvdsprm  12136  coprm  12143  prmdvdsexp  12147  prmdiv  12234  pythagtriplem19  12281  pc2dvds  12328  pcadd  12338  prmpwdvds  12352  exmidunben  12426  intopsn  12785  ismgmid  12795  isgrpid2  12912  isgrpinv  12925  dfgrp3mlem  12967  dvdsrcl2  13266  dvdsrtr  13268  dvdsrmul1  13269  dvdsrzring  13463  baspartn  13520  bastop  13545  isopn3  13595  lgsdir  14406  lgsne0  14409  bj-peano4  14677  sbthomlem  14743