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 ⊢ (𝜑 → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimpcd  159  mob2  3006  rmob  3145  preqr1g  3891  issod  4466  sotritrieq  4472  nsuceq0g  4565  suctr  4568  nordeq  4693  suc11g  4706  iss  5112  poirr2  5183  xp11m  5229  tz6.12c  5728  fnbrfvb  5744  fvelimab  5762  foeqcnvco  5999  f1eqcocnv  6000  acexmidlemcase  6083  nna0r  6755  nnawordex  6806  ectocld  6879  ecoptocl  6900  mapsnd  6974  mapsn  6976  eqeng  7056  fopwdom  7140  ordiso  7382  ltexnqq  7781  nsmallnqq  7785  nqprloc  7918  aptiprleml  8012  map2psrprg  8178  0re  8332  lttri3  8411  0cnALT  8523  reapti  8915  recnz  9750  zneo  9758  uzn0  9954  flqidz  10742  ceilqidz  10774  modqid2  10809  modqmuladdnn0  10826  frec2uzrand  10863  frecuzrdgtcl  10870  seq3id  10983  seq3z  10986  facdiv  11198  facwordi  11200  wrdnval  11357  wrdl1s1  11420  maxleb  12005  fsumf1o  12182  dvdsnegb  12600  odd2np1lem  12664  odd2np1  12665  ltoddhalfle  12685  halfleoddlt  12686  opoe  12687  omoe  12688  opeo  12689  omeo  12690  gcddiv  12821  gcdzeq  12824  dvdssqim  12826  lcmgcdeq  12886  coprmdvds2  12896  rpmul  12901  divgcdcoprmex  12905  cncongr2  12907  dvdsprm  12941  coprm  12948  prmdvdsexp  12952  prmdiv  13042  pythagtriplem19  13090  pc2dvds  13138  pcadd  13148  prmpwdvds  13163  exmidunben  13375  intopsn  13746  ismgmid  13756  imasmnd2  13818  isgrpid2  13904  isgrpinv  13918  dfgrp3mlem  13962  imasgrp2  13972  imasrng  14362  imasring  14478  dvdsrcl2  14515  dvdsrtr  14517  dvdsrmul1  14518  lspsneq0  14872  dvdsrzring  15047  znunit  15103  baspartn  15276  bastop  15301  isopn3  15351  pellexlem1  16229  ppiublem1  16291  lgsdir  16359  lgsne0  16362  lgsquadlem3  16403  uhgrm  16524  upgrfnen  16544  umgrfnen  16554  eupth2lem2dc  16905  eupth2lem3lem6fi  16917  bj-peano4  17186  sbthomlem  17276