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  2267  dvelimdf  2451  ceqsal1t  3511  gencl  3520  spsbc  3803  ssnelpss  4123  sscon34b  4309  dfnfc2  4933  uniintsn  4989  prex  5442  copsexgw  5500  copsexg  5501  posn  5773  optocl  5782  funimass1  6649  f1ocnvb  6861  eqfnfv2  7051  elpreima  7077  fconst5  7225  dff13  7274  f1ocnvfv  7297  f1ocnvfvb  7298  fliftfun  7331  eusvobj2  7422  sorpsscmpl  7752  ssonprc  7806  dmfex  7927  xpexr  7940  xpexcnv  7942  relcnvexb  7948  frxp  8149  mpoxopn0yelv  8236  rntpos  8262  oawordeulem  8590  oalimcl  8596  odi  8615  omeulem2  8619  oeeulem  8637  nnasmo  8699  erexb  8768  findcard2  9202  unxpdomlem2  9284  dif1ennnALT  9308  enp1ilem  9309  isfinite2  9331  fodomfib  9366  fodomfibOLD  9368  inf0  9658  rankxplim2  9917  scott0  9923  djuexb  9946  ficardom  9998  cardaleph  10126  dfac5  10166  cflim2  10300  fin23lem23  10363  fin23lem28  10377  isf32lem5  10394  domtriomlem  10479  ac6num  10516  zorn2lem5  10537  zorn2lem6  10538  iunfo  10576  axrepndlem2  10630  axregnd  10641  hargch  10710  addcanpi  10936  mulcanpi  10937  indpi  10944  ltaddnq  11011  ltexnq  11012  prlem934  11070  ltaddpr2  11072  ltaprlem  11081  supsrlem  11148  ssxr  11327  ltxrlt  11328  addcan  11442  addcan2  11443  neg11  11557  negreb  11571  mulcand  11893  receu  11905  ldiv  12098  lemul1a  12118  cju  12259  nn1suc  12285  nnaddcl  12286  nndivtr  12310  znegclb  12651  zmulcl  12663  zeo  12701  uz11  12900  uzp1  12916  eqreznegel  12973  rpnnen1lem6  13021  xrltne  13201  xneg11  13253  xnegdi  13286  xrsupss  13347  xrinfmss  13348  elfznelfzob  13808  modadd1  13944  modmul1  13961  om2uzlti  13987  bccmpl  14344  hashen  14382  fz1eqb  14389  hashfn  14410  hashnn0n0nn  14426  hashtpg  14520  eqwrd  14591  ccatopth  14750  ccatopth2  14751  swrdccatin2  14763  cj11  15197  rennim  15274  cnpart  15275  sqrmo  15286  sqrtgt0  15293  sqreulem  15394  sqreu  15395  cnsqrt00  15427  lo1o1  15564  lo1eq  15600  rlimeq  15601  sumss  15756  cvgcmp  15848  fprodser  15981  efne0  16129  dvdsabseq  16346  divalglem8  16433  bitsinv1lem  16474  pcfac  16932  prmreclem3  16951  sectmon  17829  yoniso  18341  oduposb  18386  lublecllem  18417  mgmb1mgm1  18680  sgrp2rid2  18951  grpinveu  19004  grpinv11  19037  mulgass  19141  galcan  19334  symg1bas  19422  cayleylem2  19445  odbezout  19590  odeq1  19592  dprddomcld  20035  dvreq1  20427  unitrrg  20719  frgpcyg  21609  obslbs  21767  coe1tm  22291  tgss3  23008  uptx  23648  txindislem  23656  qtopeu  23739  hmeocnvb  23797  qtophmeo  23840  trufil  23933  ufinffr  23952  ghmcnp  24138  tgioo  24831  lmmcvg  25308  bcth3  25378  ovolunlem1a  25544  vitali  25661  ismbf  25676  ismbfcn  25677  rolle  26042  itgsubstlem  26103  vieta1lem2  26367  elqaalem3  26377  aacjcl  26383  efif1olem4  26601  lognegb  26646  logcj  26662  argimgt0  26668  logdmnrp  26697  logcnlem3  26700  logrec  26820  dcubic  26903  isppw  27171  rplogsumlem2  27543  pntpbnd1  27644  sltres  27721  nosupno  27762  nosupres  27766  noinfno  27777  noinfres  27781  negs11  28095  divsmo  28224  n0subs  28374  axlowdimlem16  28986  usgr0vb  29268  nbgrssvwo2  29393  redwlk  29704  usgr2pthspth  29794  usgr2pth  29796  wlkswwlksf1o  29908  wlklnwwlkln2lem  29911  wpthswwlks2on  29990  clwlkclwwlkf  30036  wwlksubclwwlk  30086  frgr0v  30290  grpoinveu  30547  grpoinvf  30560  diporthcom  30744  norm1exi  31278  shmodsi  31417  shmodi  31418  dfch2  31435  orthin  31474  chssoc  31524  spansncvi  31680  kbpj  31984  lnopunilem1  32038  cnlnssadj  32108  bra11  32136  strlem4  32282  strlem5  32283  hstrlem4  32290  hstrlem5  32291  dmdmd  32328  mdslle1i  32345  mdslle2i  32346  mdslmd1lem1  32353  atcvatlem  32413  atcvat4i  32425  mdsymlem3  32433  bcm1n  32802  xmulcand  32887  xreceu  32888  tpr2rico  33872  bnj1125  34984  revwlkb  35109  umgr2cycllem  35124  mrsubff1  35498  mvhf1  35543  funpsstri  35746  btwnintr  36000  idinside  36065  btwnconn1lem13  36080  fneval  36334  bj-equsal1t  36804  bj-brrelex12ALT  37049  bj-elid6  37152  bj-isrvec2  37282  bj-bary1lem1  37293  bj-bary1  37294  fvineqsnf1  37392  wl-equsal1i  37524  uncf  37585  matunitlindflem2  37603  poimirlem4  37610  poimirlem9  37615  ismtybndlem  37792  grpoeqdivid  37867  0rngo  38013  imaexALTV  38311  dmqseqim  38637  ax12indalem  38926  ax12inda2ALT  38927  lcvexchlem4  39018  lcvexchlem5  39019  opcon3b  39177  2dim  39452  ps-1  39459  paddclN  39824  ltrnnid  40118  cdleme22b  40323  dihmeetlem13N  41301  dih1dimatlem  41311  dihlspsnat  41315  eqresfnbd  42251  remulcan2d  42276  nnaddcom  42281  efne0d  42351  log11d  42360  sn-addcand  42425  sn-addcan2d  42427  onsupneqmaxlim0  43212  sqrtcval  43630  frege58c  43910  gneispa  44119  nzss  44312  expgrowth  44330  sbiota1  44429  f1cof1b  47026  f1ocof1ob2  47031  fafv2elrnb  47184  sbgoldbwt  47701  dignn0flhalflem1  48464  rrxlinesc  48584  aacllem  49031