Theorem imbitrid 247

Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem imbitrid

Step	Hyp	Ref	Expression
1		imbitrid.1	. 2 ⊢ (𝜑 → 𝜓)
2		imbitrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	biimpd 232	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 3	syl5 35	1 ⊢ (𝜒 → (𝜑 → 𝜃))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  syl5ibcom  248  imbitrrid  249  sbft  2305  dvelimdf  2480  ceqsal1t  3485  gencl  3494  spsbc  3755  ssnelpss  4066  sscon34b  4253  dfnfc2  4892  uniintsn  4948  prexOLD  5412  copsexgwOLD  5471  copsexg  5472  posn  5745  optocl  5753  optoclOLD  5754  funimass1  6619  f1ocnvb  6835  eqfnfv2  7027  elpreima  7054  fconst5  7209  dff13  7255  f1ocnvfv  7283  f1ocnvfvb  7284  fliftfun  7317  eusvobj2  7409  sorpsscmpl  7739  ssonprc  7790  dmfex  7906  xpexr  7919  xpexcnv  7921  relcnvexb  7927  frxp  8128  mpoxopn0yelv  8215  rntpos  8241  oawordeulem  8545  oalimcl  8551  odi  8570  omeulem2  8574  oeeulem  8593  nnasmo  8655  erexb  8726  uncf  8874  findcard2  9163  unxpdomlem2  9231  dif1ennnALT  9251  enp1ilem  9252  isfinite2  9272  fodomfib  9302  inf0  9604  rankxplim2  9866  scott0b  9880  scott0OLD  9881  djuexb  9918  ficardom  9970  cardaleph  10096  dfac5  10135  cflim2  10269  fin23lem23  10332  fin23lem28  10346  isf32lem5  10363  domtriomlem  10448  ac6num  10485  zorn2lem5  10506  zorn2lem6  10507  iunfo  10551  axrepndlem2  10606  axregnd  10617  hargch  10686  addcanpi  10912  mulcanpi  10913  indpi  10920  ltaddnq  10987  ltexnq  10988  prlem934  11046  ltaddpr2  11048  ltaprlem  11057  supsrlem  11124  ssxr  11307  ltxrlt  11308  addcan  11422  addcan2  11423  neg11  11537  negreb  11551  mulcand  11875  receu  11887  ldiv  12077  lemul1a  12097  cju  12242  nn1suc  12283  nnaddcl  12284  nnaddcom  12288  nndivtr  12311  znegclb  12659  zmulcl  12671  zeo  12711  uz11  12916  uzp1  12928  eqreznegel  12987  rpnnen1lem6  13036  xrltne  13218  xneg11  13271  xnegdi  13304  xrsupss  13365  xrinfmss  13366  elfznelfzob  13834  modadd1  13973  modmul1  13992  om2uzlti  14018  bccmpl  14377  hashen  14415  fz1eqb  14422  hashfn  14443  hashnn0n0nn  14459  hashtpg  14554  eqwrd  14626  ccatopth  14789  ccatopth2  14790  swrdccatin2  14802  cj11  15253  rennim  15330  cnpart  15331  sqrmo  15342  sqrtgt0  15349  sqreulem  15451  sqreu  15452  cnsqrt00  15484  lo1o1  15623  lo1eq  15659  rlimeq  15660  sumss  15814  cvgcmp  15907  fprodser  16042  efne0d  16189  efne0OLD  16191  dvdsabseq  16409  divalglem8  16496  bitsinv1lem  16537  pcfac  16997  prmreclem3  17016  sectmon  17877  yoniso  18379  oduposb  18421  lublecllem  18452  chnrev  18721  mgmb1mgm1  18753  sgrp2rid2  19044  grpinveu  19104  grpinv11  19137  mulgass  19240  galcan  19437  symg1bas  19524  cayleylem2  19546  odbezout  19691  odeq1  19693  dprddomcld  20136  dvreq1  20558  unitrrg  20871  frgpcyg  21792  obslbs  21949  coe1tm  22505  matunitlindflem2  22908  tgss3  23217  uptx  23857  txindislem  23865  qtopeu  23948  hmeocnvb  24006  qtophmeo  24049  trufil  24142  ufinffr  24161  ghmcnp  24347  tgioo  25028  lmmcvg  25495  bcth3  25565  ovolunlem1a  25730  vitali  25847  ismbf  25862  ismbfcn  25863  rolle  26224  itgsubstlem  26282  vieta1lem2  26550  elqaalem3  26560  aacjcl  26570  efif1olem4  26790  lognegb  26835  logcj  26851  argimgt0  26857  logdmnrp  26886  logcnlem3  26889  logrec  27008  dcubic  27091  isppw  27358  rplogsumlem2  27729  pntpbnd1  27830  ltsres  27906  nosupno  27947  nosupres  27951  noinfno  27962  noinfres  27966  negs11  28322  divsmo  28457  n0subs  28636  n0ltsp1le  28638  z12negsclb  28754  axlowdimlem16  29422  usgr0vb  29705  nbgrssvwo2  29830  redwlk  30138  usgr2pthspth  30235  usgr2pth  30237  wlkswwlksf1o  30355  wlklnwwlkln2lem  30358  wpthswwlks2on  30440  clwlkclwwlkf  30486  wwlksubclwwlk  30536  frgr0v  30750  grpoinveu  31008  grpoinvf  31021  diporthcom  31205  norm1exi  31739  shmodsi  31878  shmodi  31879  dfch2  31896  orthin  31935  chssoc  31985  spansncvi  32141  kbpj  32445  lnopunilem1  32499  cnlnssadj  32569  bra11  32597  strlem4  32743  strlem5  32744  hstrlem4  32751  hstrlem5  32752  dmdmd  32789  mdslle1i  32806  mdslle2i  32807  mdslmd1lem1  32814  atcvatlem  32874  atcvat4i  32886  mdsymlem3  32894  bcm1n  33274  xmulcand  33374  xreceu  33375  tpr2rico  34430  bnj1125  35509  fnfvintima  35599  revwlkb  35730  mrsubff1  36101  mvhf1  36146  funpsstri  36353  btwnintr  36607  idinside  36672  btwnconn1lem13  36687  fneval  36979  bj-equsal1t  37573  bj-brrelex12ALT  37819  bj-elid6  37930  bj-isrvec2  38060  bj-bary1lem1  38071  bj-bary1  38072  fvineqsnf1  38172  wl-equsal1i  38315  poimirlem4  38381  poimirlem9  38386  ismtybndlem  38564  grpoeqdivid  38639  0rngo  38785  dmqseqim  39497  eldisjdmqsim2  39572  qmapeldisjsim  39616  rnqmapeleldisjsim  39618  ax12indalem  39826  ax12inda2ALT  39827  lcvexchlem4  39918  lcvexchlem5  39919  opcon3b  40077  2dim  40351  ps-1  40358  paddclN  40723  ltrnnid  41017  cdleme22b  41222  dihmeetlem13N  42200  dih1dimatlem  42210  dihlspsnat  42214  eqresfnbd  43110  remulcan2d  43131  log11d  43229  sn-addcand  43303  sn-addcan2d  43305  rediveud  43326  onsupneqmaxlim0  44073  sqrtcval  44489  frege58c  44769  gneispa  44978  nzss  45149  expgrowth  45167  sbiota1  45266  ormkglobd  47713  f1cof1b  47973  f1ocof1ob2  47978  fafv2elrnb  48131  sbgoldbwt  48701  dignn0flhalflem1  49553  rrxlinesc  49673  oppff1  50082  aacllem  50780