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 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  syl5ibcom  248  imbitrrid  249  sbft  2307  dvelimdf  2483  ceqsal1t  3489  gencl  3498  spsbc  3760  ssnelpss  4071  sscon34b  4259  dfnfc2  4890  uniintsn  4946  prexOLD  5405  copsexgwOLD  5464  copsexg  5465  posn  5738  optocl  5746  optoclOLD  5747  funimass1  6607  f1ocnvb  6824  eqfnfv2  7016  elpreima  7043  fconst5  7194  dff13  7242  f1ocnvfv  7266  f1ocnvfvb  7267  fliftfun  7300  eusvobj2  7392  sorpsscmpl  7721  ssonprc  7774  dmfex  7890  xpexr  7903  xpexcnv  7905  relcnvexb  7911  frxp  8110  mpoxopn0yelv  8197  rntpos  8223  oawordeulem  8527  oalimcl  8533  odi  8552  omeulem2  8556  oeeulem  8575  nnasmo  8637  erexb  8708  findcard2  9137  unxpdomlem2  9205  dif1ennnALT  9225  enp1ilem  9226  isfinite2  9246  fodomfib  9276  inf0  9578  rankxplim2  9840  scott0  9848  djuexb  9883  ficardom  9935  cardaleph  10061  dfac5  10100  cflim2  10235  fin23lem23  10298  fin23lem28  10312  isf32lem5  10329  domtriomlem  10414  ac6num  10451  zorn2lem5  10472  zorn2lem6  10473  iunfo  10511  axrepndlem2  10566  axregnd  10577  hargch  10646  addcanpi  10872  mulcanpi  10873  indpi  10880  ltaddnq  10947  ltexnq  10948  prlem934  11006  ltaddpr2  11008  ltaprlem  11017  supsrlem  11084  ssxr  11267  ltxrlt  11268  addcan  11382  addcan2  11383  neg11  11497  negreb  11511  mulcand  11835  receu  11847  ldiv  12040  lemul1a  12060  cju  12205  nn1suc  12246  nnaddcl  12247  nnaddcom  12251  nndivtr  12274  znegclb  12622  zmulcl  12634  zeo  12673  uz11  12878  uzp1  12890  eqreznegel  12949  rpnnen1lem6  12997  xrltne  13179  xneg11  13232  xnegdi  13265  xrsupss  13326  xrinfmss  13327  elfznelfzob  13794  modadd1  13932  modmul1  13951  om2uzlti  13977  bccmpl  14336  hashen  14374  fz1eqb  14381  hashfn  14402  hashnn0n0nn  14418  hashtpg  14512  eqwrd  14584  ccatopth  14743  ccatopth2  14744  swrdccatin2  14756  cj11  15203  rennim  15280  cnpart  15281  sqrmo  15292  sqrtgt0  15299  sqreulem  15401  sqreu  15402  cnsqrt00  15434  lo1o1  15573  lo1eq  15609  rlimeq  15610  sumss  15765  cvgcmp  15858  fprodser  15993  efne0d  16141  efne0OLD  16143  dvdsabseq  16361  divalglem8  16448  bitsinv1lem  16489  pcfac  16949  prmreclem3  16968  sectmon  17829  yoniso  18331  oduposb  18373  lublecllem  18404  chnrev  18673  mgmb1mgm1  18703  sgrp2rid2  18978  grpinveu  19031  grpinv11  19064  mulgass  19168  galcan  19365  symg1bas  19452  cayleylem2  19474  odbezout  19619  odeq1  19621  dprddomcld  20064  dvreq1  20484  unitrrg  20779  frgpcyg  21683  obslbs  21840  coe1tm  22394  tgss3  23104  uptx  23743  txindislem  23751  qtopeu  23834  hmeocnvb  23892  qtophmeo  23935  trufil  24028  ufinffr  24047  ghmcnp  24233  tgioo  24914  lmmcvg  25381  bcth3  25451  ovolunlem1a  25616  vitali  25733  ismbf  25748  ismbfcn  25749  rolle  26110  itgsubstlem  26168  vieta1lem2  26433  elqaalem3  26443  aacjcl  26449  efif1olem4  26668  lognegb  26713  logcj  26729  argimgt0  26735  logdmnrp  26764  logcnlem3  26767  logrec  26886  dcubic  26969  isppw  27236  rplogsumlem2  27607  pntpbnd1  27708  ltsres  27784  nosupno  27825  nosupres  27829  noinfno  27840  noinfres  27844  negs11  28200  divsmo  28335  n0subs  28514  n0ltsp1le  28516  z12negsclb  28632  axlowdimlem16  29216  usgr0vb  29496  nbgrssvwo2  29621  redwlk  29929  usgr2pthspth  30020  usgr2pth  30022  wlkswwlksf1o  30137  wlklnwwlkln2lem  30140  wpthswwlks2on  30222  clwlkclwwlkf  30268  wwlksubclwwlk  30318  frgr0v  30522  grpoinveu  30780  grpoinvf  30793  diporthcom  30977  norm1exi  31511  shmodsi  31650  shmodi  31651  dfch2  31668  orthin  31707  chssoc  31757  spansncvi  31913  kbpj  32217  lnopunilem1  32271  cnlnssadj  32341  bra11  32369  strlem4  32515  strlem5  32516  hstrlem4  32523  hstrlem5  32524  dmdmd  32561  mdslle1i  32578  mdslle2i  32579  mdslmd1lem1  32586  atcvatlem  32646  atcvat4i  32658  mdsymlem3  32666  bcm1n  33052  xmulcand  33153  xreceu  33154  tpr2rico  34219  bnj1125  35297  revwlkb  35489  umgr2cycllem  35503  mrsubff1  35877  mvhf1  35922  funpsstri  36129  btwnintr  36382  idinside  36447  btwnconn1lem13  36462  fneval  36725  bj-equsal1t  37319  bj-brrelex12ALT  37564  bj-elid6  37674  bj-isrvec2  37804  bj-bary1lem1  37815  bj-bary1  37816  fvineqsnf1  37916  wl-equsal1i  38059  uncf  38110  matunitlindflem2  38128  poimirlem4  38135  poimirlem9  38140  ismtybndlem  38317  grpoeqdivid  38392  0rngo  38538  dmqseqim  39252  eldisjdmqsim2  39327  qmapeldisjsim  39371  rnqmapeleldisjsim  39373  ax12indalem  39581  ax12inda2ALT  39582  lcvexchlem4  39673  lcvexchlem5  39674  opcon3b  39832  2dim  40106  ps-1  40113  paddclN  40478  ltrnnid  40772  cdleme22b  40977  dihmeetlem13N  41955  dih1dimatlem  41965  dihlspsnat  41969  eqresfnbd  42863  remulcan2d  42884  log11d  42967  sn-addcand  43041  sn-addcan2d  43043  rediveud  43064  onsupneqmaxlim0  43813  sqrtcval  44229  frege58c  44509  gneispa  44718  nzss  44891  expgrowth  44909  sbiota1  45008  ormkglobd  47449  f1cof1b  47669  f1ocof1ob2  47674  fafv2elrnb  47827  sbgoldbwt  48397  dignn0flhalflem1  49246  rrxlinesc  49366  oppff1  49777  aacllem  50430