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  3475  gencl  3484  spsbc  3755  ssnelpss  4068  sscon34b  4258  dfnfc2  4887  uniintsn  4942  prexOLD  5389  copsexgw  5446  copsexg  5447  posn  5718  optocl  5726  optoclOLD  5727  funimass1  6582  f1ocnvb  6795  eqfnfv2  6986  elpreima  7012  fconst5  7162  dff13  7210  f1ocnvfv  7234  f1ocnvfvb  7235  fliftfun  7268  eusvobj2  7360  sorpsscmpl  7689  ssonprc  7742  dmfex  7857  xpexr  7870  xpexcnv  7872  relcnvexb  7878  frxp  8078  mpoxopn0yelv  8165  rntpos  8191  oawordeulem  8491  oalimcl  8497  odi  8516  omeulem2  8520  oeeulem  8539  nnasmo  8601  erexb  8671  findcard2  9101  unxpdomlem2  9169  dif1ennnALT  9189  enp1ilem  9190  isfinite2  9210  fodomfib  9241  fodomfibOLD  9243  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  11214  ltxrlt  11215  addcan  11329  addcan2  11330  neg11  11444  negreb  11458  mulcand  11782  receu  11794  ldiv  11987  lemul1a  12007  cju  12153  nn1suc  12179  nnaddcl  12180  nndivtr  12204  znegclb  12540  zmulcl  12552  zeo  12590  uz11  12788  uzp1  12800  eqreznegel  12859  rpnnen1lem6  12907  xrltne  13089  xneg11  13142  xnegdi  13175  xrsupss  13236  xrinfmss  13237  elfznelfzob  13702  modadd1  13840  modmul1  13859  om2uzlti  13885  bccmpl  14244  hashen  14282  fz1eqb  14289  hashfn  14310  hashnn0n0nn  14326  hashtpg  14420  eqwrd  14492  ccatopth  14651  ccatopth2  14652  swrdccatin2  14664  cj11  15097  rennim  15174  cnpart  15175  sqrmo  15186  sqrtgt0  15193  sqreulem  15295  sqreu  15296  cnsqrt00  15328  lo1o1  15467  lo1eq  15503  rlimeq  15504  sumss  15659  cvgcmp  15751  fprodser  15884  efne0d  16032  efne0OLD  16034  dvdsabseq  16252  divalglem8  16339  bitsinv1lem  16380  pcfac  16839  prmreclem3  16858  sectmon  17718  yoniso  18220  oduposb  18262  lublecllem  18293  chnrev  18562  mgmb1mgm1  18592  sgrp2rid2  18863  grpinveu  18916  grpinv11  18949  mulgass  19053  galcan  19245  symg1bas  19332  cayleylem2  19354  odbezout  19499  odeq1  19501  dprddomcld  19944  dvreq1  20359  unitrrg  20648  frgpcyg  21540  obslbs  21697  coe1tm  22227  tgss3  22942  uptx  23581  txindislem  23589  qtopeu  23672  hmeocnvb  23730  qtophmeo  23773  trufil  23866  ufinffr  23885  ghmcnp  24071  tgioo  24752  lmmcvg  25229  bcth3  25299  ovolunlem1a  25465  vitali  25582  ismbf  25597  ismbfcn  25598  rolle  25962  itgsubstlem  26023  vieta1lem2  26287  elqaalem3  26297  aacjcl  26303  efif1olem4  26522  lognegb  26567  logcj  26583  argimgt0  26589  logdmnrp  26618  logcnlem3  26621  logrec  26741  dcubic  26824  isppw  27092  rplogsumlem2  27464  pntpbnd1  27565  ltsres  27642  nosupno  27683  nosupres  27687  noinfno  27698  noinfres  27702  negs11  28057  divsmo  28192  n0subs  28371  n0ltsp1le  28373  z12negsclb  28489  axlowdimlem16  29042  usgr0vb  29322  nbgrssvwo2  29447  redwlk  29756  usgr2pthspth  29847  usgr2pth  29849  wlkswwlksf1o  29964  wlklnwwlkln2lem  29967  wpthswwlks2on  30049  clwlkclwwlkf  30095  wwlksubclwwlk  30145  frgr0v  30349  grpoinveu  30606  grpoinvf  30619  diporthcom  30803  norm1exi  31337  shmodsi  31476  shmodi  31477  dfch2  31494  orthin  31533  chssoc  31583  spansncvi  31739  kbpj  32043  lnopunilem1  32097  cnlnssadj  32167  bra11  32195  strlem4  32341  strlem5  32342  hstrlem4  32349  hstrlem5  32350  dmdmd  32387  mdslle1i  32404  mdslle2i  32405  mdslmd1lem1  32412  atcvatlem  32472  atcvat4i  32484  mdsymlem3  32492  bcm1n  32885  xmulcand  33012  xreceu  33013  tpr2rico  34089  bnj1125  35167  revwlkb  35339  umgr2cycllem  35353  mrsubff1  35727  mvhf1  35772  funpsstri  35979  btwnintr  36232  idinside  36297  btwnconn1lem13  36312  fneval  36565  bj-equsal1t  37061  bj-brrelex12ALT  37306  bj-elid6  37414  bj-isrvec2  37544  bj-bary1lem1  37555  bj-bary1  37556  fvineqsnf1  37654  wl-equsal1i  37788  uncf  37839  matunitlindflem2  37857  poimirlem4  37864  poimirlem9  37869  ismtybndlem  38046  grpoeqdivid  38121  0rngo  38267  dmqseqim  38981  eldisjdmqsim2  39056  qmapeldisjsim  39100  rnqmapeleldisjsim  39102  ax12indalem  39310  ax12inda2ALT  39311  lcvexchlem4  39402  lcvexchlem5  39403  opcon3b  39561  2dim  39835  ps-1  39842  paddclN  40207  ltrnnid  40501  cdleme22b  40706  dihmeetlem13N  41684  dih1dimatlem  41694  dihlspsnat  41698  eqresfnbd  42593  remulcan2d  42616  nnaddcom  42627  log11d  42705  sn-addcand  42779  sn-addcan2d  42781  rediveud  42802  onsupneqmaxlim0  43570  sqrtcval  43986  frege58c  44266  gneispa  44475  nzss  44662  expgrowth  44680  sbiota1  44779  ormkglobd  47222  f1cof1b  47426  f1ocof1ob2  47431  fafv2elrnb  47584  sbgoldbwt  48126  dignn0flhalflem1  48964  rrxlinesc  49084  oppff1  49496  aacllem  50149