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  2277  dvelimdf  2454  ceqsal1t  3463  gencl  3472  spsbc  3742  ssnelpss  4055  sscon34b  4245  dfnfc2  4873  uniintsn  4928  prexOLD  5386  copsexgwOLD  5445  copsexg  5446  posn  5717  optocl  5725  optoclOLD  5726  funimass1  6581  f1ocnvb  6794  eqfnfv2  6985  elpreima  7011  fconst5  7161  dff13  7209  f1ocnvfv  7233  f1ocnvfvb  7234  fliftfun  7267  eusvobj2  7359  sorpsscmpl  7688  ssonprc  7741  dmfex  7856  xpexr  7869  xpexcnv  7871  relcnvexb  7877  frxp  8076  mpoxopn0yelv  8163  rntpos  8189  oawordeulem  8489  oalimcl  8495  odi  8514  omeulem2  8518  oeeulem  8537  nnasmo  8599  erexb  8669  findcard2  9099  unxpdomlem2  9167  dif1ennnALT  9187  enp1ilem  9188  isfinite2  9208  fodomfib  9239  fodomfibOLD  9241  inf0  9542  rankxplim2  9804  scott0  9810  djuexb  9833  ficardom  9885  cardaleph  10011  dfac5  10051  cflim2  10185  fin23lem23  10248  fin23lem28  10262  isf32lem5  10279  domtriomlem  10364  ac6num  10401  zorn2lem5  10422  zorn2lem6  10423  iunfo  10461  axrepndlem2  10516  axregnd  10527  hargch  10596  addcanpi  10822  mulcanpi  10823  indpi  10830  ltaddnq  10897  ltexnq  10898  prlem934  10956  ltaddpr2  10958  ltaprlem  10967  supsrlem  11034  ssxr  11215  ltxrlt  11216  addcan  11330  addcan2  11331  neg11  11445  negreb  11459  mulcand  11783  receu  11795  ldiv  11989  lemul1a  12009  cju  12155  nn1suc  12196  nnaddcl  12197  nnaddcom  12201  nndivtr  12224  znegclb  12564  zmulcl  12576  zeo  12615  uz11  12813  uzp1  12825  eqreznegel  12884  rpnnen1lem6  12932  xrltne  13114  xneg11  13167  xnegdi  13200  xrsupss  13261  xrinfmss  13262  elfznelfzob  13729  modadd1  13867  modmul1  13886  om2uzlti  13912  bccmpl  14271  hashen  14309  fz1eqb  14316  hashfn  14337  hashnn0n0nn  14353  hashtpg  14447  eqwrd  14519  ccatopth  14678  ccatopth2  14679  swrdccatin2  14691  cj11  15124  rennim  15201  cnpart  15202  sqrmo  15213  sqrtgt0  15220  sqreulem  15322  sqreu  15323  cnsqrt00  15355  lo1o1  15494  lo1eq  15530  rlimeq  15531  sumss  15686  cvgcmp  15779  fprodser  15914  efne0d  16062  efne0OLD  16064  dvdsabseq  16282  divalglem8  16369  bitsinv1lem  16410  pcfac  16870  prmreclem3  16889  sectmon  17749  yoniso  18251  oduposb  18293  lublecllem  18324  chnrev  18593  mgmb1mgm1  18623  sgrp2rid2  18897  grpinveu  18950  grpinv11  18983  mulgass  19087  galcan  19279  symg1bas  19366  cayleylem2  19388  odbezout  19533  odeq1  19535  dprddomcld  19978  dvreq1  20391  unitrrg  20680  frgpcyg  21553  obslbs  21710  coe1tm  22238  tgss3  22951  uptx  23590  txindislem  23598  qtopeu  23681  hmeocnvb  23739  qtophmeo  23782  trufil  23875  ufinffr  23894  ghmcnp  24080  tgioo  24761  lmmcvg  25228  bcth3  25298  ovolunlem1a  25463  vitali  25580  ismbf  25595  ismbfcn  25596  rolle  25957  itgsubstlem  26015  vieta1lem2  26277  elqaalem3  26287  aacjcl  26293  efif1olem4  26509  lognegb  26554  logcj  26570  argimgt0  26576  logdmnrp  26605  logcnlem3  26608  logrec  26727  dcubic  26810  isppw  27077  rplogsumlem2  27448  pntpbnd1  27549  ltsres  27626  nosupno  27667  nosupres  27671  noinfno  27682  noinfres  27686  negs11  28041  divsmo  28176  n0subs  28355  n0ltsp1le  28357  z12negsclb  28473  axlowdimlem16  29026  usgr0vb  29306  nbgrssvwo2  29431  redwlk  29739  usgr2pthspth  29830  usgr2pth  29832  wlkswwlksf1o  29947  wlklnwwlkln2lem  29950  wpthswwlks2on  30032  clwlkclwwlkf  30078  wwlksubclwwlk  30128  frgr0v  30332  grpoinveu  30590  grpoinvf  30603  diporthcom  30787  norm1exi  31321  shmodsi  31460  shmodi  31461  dfch2  31478  orthin  31517  chssoc  31567  spansncvi  31723  kbpj  32027  lnopunilem1  32081  cnlnssadj  32151  bra11  32179  strlem4  32325  strlem5  32326  hstrlem4  32333  hstrlem5  32334  dmdmd  32371  mdslle1i  32388  mdslle2i  32389  mdslmd1lem1  32396  atcvatlem  32456  atcvat4i  32468  mdsymlem3  32476  bcm1n  32868  xmulcand  32980  xreceu  32981  tpr2rico  34056  bnj1125  35134  revwlkb  35308  umgr2cycllem  35322  mrsubff1  35696  mvhf1  35741  funpsstri  35948  btwnintr  36201  idinside  36266  btwnconn1lem13  36281  fneval  36534  bj-equsal1t  37129  bj-brrelex12ALT  37374  bj-elid6  37484  bj-isrvec2  37614  bj-bary1lem1  37625  bj-bary1  37626  fvineqsnf1  37726  wl-equsal1i  37869  uncf  37920  matunitlindflem2  37938  poimirlem4  37945  poimirlem9  37950  ismtybndlem  38127  grpoeqdivid  38202  0rngo  38348  dmqseqim  39062  eldisjdmqsim2  39137  qmapeldisjsim  39181  rnqmapeleldisjsim  39183  ax12indalem  39391  ax12inda2ALT  39392  lcvexchlem4  39483  lcvexchlem5  39484  opcon3b  39642  2dim  39916  ps-1  39923  paddclN  40288  ltrnnid  40582  cdleme22b  40787  dihmeetlem13N  41765  dih1dimatlem  41775  dihlspsnat  41779  eqresfnbd  42673  remulcan2d  42695  log11d  42778  sn-addcand  42852  sn-addcan2d  42854  rediveud  42875  onsupneqmaxlim0  43652  sqrtcval  44068  frege58c  44348  gneispa  44557  nzss  44744  expgrowth  44762  sbiota1  44861  ormkglobd  47303  f1cof1b  47519  f1ocof1ob2  47524  fafv2elrnb  47677  sbgoldbwt  48247  dignn0flhalflem1  49085  rrxlinesc  49205  oppff1  49617  aacllem  50270