Theorem imbitrid 244

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 229	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 3	syl5 34	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  syl5ibcom  245  imbitrrid  246  sbft  2271  dvelimdf  2457  ceqsal1t  3522  gencl  3533  spsbc  3817  ssnelpss  4137  sscon34b  4323  dfnfc2  4953  uniintsn  5009  prex  5452  copsexgw  5510  copsexg  5511  posn  5785  optocl  5794  funimass1  6660  f1ocnvb  6875  eqfnfv2  7065  elpreima  7091  fconst5  7243  dff13  7292  f1ocnvfv  7314  f1ocnvfvb  7315  fliftfun  7348  eusvobj2  7440  sorpsscmpl  7769  ssonprc  7823  dmfex  7945  xpexr  7958  xpexcnv  7960  relcnvexb  7966  frxp  8167  mpoxopn0yelv  8254  rntpos  8280  oawordeulem  8610  oalimcl  8616  odi  8635  omeulem2  8639  oeeulem  8657  nnasmo  8719  erexb  8788  findcard2  9230  unxpdomlem2  9314  dif1ennnALT  9339  enp1ilem  9340  isfinite2  9362  fodomfib  9397  fodomfibOLD  9399  inf0  9690  rankxplim2  9949  scott0  9955  djuexb  9978  ficardom  10030  cardaleph  10158  dfac5  10198  cflim2  10332  fin23lem23  10395  fin23lem28  10409  isf32lem5  10426  domtriomlem  10511  ac6num  10548  zorn2lem5  10569  zorn2lem6  10570  iunfo  10608  axrepndlem2  10662  axregnd  10673  hargch  10742  addcanpi  10968  mulcanpi  10969  indpi  10976  ltaddnq  11043  ltexnq  11044  prlem934  11102  ltaddpr2  11104  ltaprlem  11113  supsrlem  11180  ssxr  11359  ltxrlt  11360  addcan  11474  addcan2  11475  neg11  11587  negreb  11601  mulcand  11923  receu  11935  ldiv  12128  lemul1a  12148  cju  12289  nn1suc  12315  nnaddcl  12316  nndivtr  12340  znegclb  12680  zmulcl  12692  zeo  12729  uz11  12928  uzp1  12944  eqreznegel  12999  rpnnen1lem6  13047  xrltne  13225  xneg11  13277  xnegdi  13310  xrsupss  13371  xrinfmss  13372  elfznelfzob  13823  modadd1  13959  modmul1  13975  om2uzlti  14001  bccmpl  14358  hashen  14396  fz1eqb  14403  hashfn  14424  hashnn0n0nn  14440  hashtpg  14534  eqwrd  14605  ccatopth  14764  ccatopth2  14765  swrdccatin2  14777  cj11  15211  rennim  15288  cnpart  15289  sqrmo  15300  sqrtgt0  15307  sqreulem  15408  sqreu  15409  cnsqrt00  15441  lo1o1  15578  lo1eq  15614  rlimeq  15615  sumss  15772  cvgcmp  15864  fprodser  15997  efne0  16145  dvdsabseq  16361  divalglem8  16448  bitsinv1lem  16487  pcfac  16946  prmreclem3  16965  sectmon  17843  yoniso  18355  oduposb  18399  lublecllem  18430  mgmb1mgm1  18693  sgrp2rid2  18961  grpinveu  19014  grpinv11  19047  mulgass  19151  galcan  19344  symg1bas  19432  cayleylem2  19455  odbezout  19600  odeq1  19602  dprddomcld  20045  dvreq1  20437  unitrrg  20725  frgpcyg  21615  obslbs  21773  coe1tm  22297  tgss3  23014  uptx  23654  txindislem  23662  qtopeu  23745  hmeocnvb  23803  qtophmeo  23846  trufil  23939  ufinffr  23958  ghmcnp  24144  tgioo  24837  lmmcvg  25314  bcth3  25384  ovolunlem1a  25550  vitali  25667  ismbf  25682  ismbfcn  25683  rolle  26048  itgsubstlem  26109  vieta1lem2  26371  elqaalem3  26381  aacjcl  26387  efif1olem4  26605  lognegb  26650  logcj  26666  argimgt0  26672  logdmnrp  26701  logcnlem3  26704  logrec  26824  dcubic  26907  isppw  27175  rplogsumlem2  27547  pntpbnd1  27648  sltres  27725  nosupno  27766  nosupres  27770  noinfno  27781  noinfres  27785  negs11  28099  divsmo  28228  n0subs  28378  axlowdimlem16  28990  usgr0vb  29272  nbgrssvwo2  29397  redwlk  29708  usgr2pthspth  29798  usgr2pth  29800  wlkswwlksf1o  29912  wlklnwwlkln2lem  29915  wpthswwlks2on  29994  clwlkclwwlkf  30040  wwlksubclwwlk  30090  frgr0v  30294  grpoinveu  30551  grpoinvf  30564  diporthcom  30748  norm1exi  31282  shmodsi  31421  shmodi  31422  dfch2  31439  orthin  31478  chssoc  31528  spansncvi  31684  kbpj  31988  lnopunilem1  32042  cnlnssadj  32112  bra11  32140  strlem4  32286  strlem5  32287  hstrlem4  32294  hstrlem5  32295  dmdmd  32332  mdslle1i  32349  mdslle2i  32350  mdslmd1lem1  32357  atcvatlem  32417  atcvat4i  32429  mdsymlem3  32437  bcm1n  32800  xmulcand  32885  xreceu  32886  tpr2rico  33858  bnj1125  34968  revwlkb  35093  umgr2cycllem  35108  mrsubff1  35482  mvhf1  35527  funpsstri  35729  btwnintr  35983  idinside  36048  btwnconn1lem13  36063  fneval  36318  bj-equsal1t  36788  bj-brrelex12ALT  37033  bj-elid6  37136  bj-isrvec2  37266  bj-bary1lem1  37277  bj-bary1  37278  fvineqsnf1  37376  wl-equsal1i  37498  uncf  37559  matunitlindflem2  37577  poimirlem4  37584  poimirlem9  37589  ismtybndlem  37766  grpoeqdivid  37841  0rngo  37987  imaexALTV  38286  dmqseqim  38612  ax12indalem  38901  ax12inda2ALT  38902  lcvexchlem4  38993  lcvexchlem5  38994  opcon3b  39152  2dim  39427  ps-1  39434  paddclN  39799  ltrnnid  40093  cdleme22b  40298  dihmeetlem13N  41276  dih1dimatlem  41286  dihlspsnat  41290  eqresfnbd  42227  remulcan2d  42252  nnaddcom  42257  efne0d  42325  log11d  42334  sn-addcand  42395  sn-addcan2d  42397  onsupneqmaxlim0  43185  sqrtcval  43603  frege58c  43883  gneispa  44092  nzss  44286  expgrowth  44304  sbiota1  44403  f1cof1b  46992  f1ocof1ob2  46997  fafv2elrnb  47150  sbgoldbwt  47651  dignn0flhalflem1  48349  rrxlinesc  48469  aacllem  48895