Theorem imbitrid 243

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  syl5ibcom  244  imbitrrid  245  sbft  2262  dvelimdf  2449  ceqsalt  3505  gencl  3515  vtoclgft  3539  spsbc  3788  ssnelpss  4109  sscon34b  4292  dfnfc2  4929  uniintsn  4987  prex  5428  copsexgw  5486  copsexg  5487  posn  5756  optocl  5765  funimass1  6622  f1ocnvb  6836  eqfnfv2  7022  elpreima  7047  fconst5  7194  dff13  7241  f1ocnvfv  7263  f1ocnvfvb  7264  fliftfun  7296  eusvobj2  7388  sorpsscmpl  7711  ssonprc  7762  dmfex  7885  xpexr  7896  xpexcnv  7898  relcnvexb  7904  frxp  8099  mpoxopn0yelv  8185  rntpos  8211  oawordeulem  8542  oalimcl  8548  odi  8567  omeulem2  8571  oeeulem  8589  nnasmo  8650  erexb  8716  findcard2  9152  unxpdomlem2  9239  dif1ennnALT  9265  enp1ilem  9266  findcard2OLD  9272  isfinite2  9289  unfiOLD  9301  fodomfib  9314  inf0  9603  rankxplim2  9862  scott0  9868  djuexb  9891  ficardom  9943  cardaleph  10071  dfac5  10110  cflim2  10245  fin23lem23  10308  fin23lem28  10322  isf32lem5  10339  domtriomlem  10424  ac6num  10461  zorn2lem5  10482  zorn2lem6  10483  iunfo  10521  axrepndlem2  10575  axregnd  10586  hargch  10655  addcanpi  10881  mulcanpi  10882  indpi  10889  ltaddnq  10956  ltexnq  10957  prlem934  11015  ltaddpr2  11017  ltaprlem  11026  supsrlem  11093  ssxr  11270  ltxrlt  11271  addcan  11385  addcan2  11386  neg11  11498  negreb  11512  mulcand  11834  receu  11846  ldiv  12035  lemul1a  12055  cju  12195  nn1suc  12221  nnaddcl  12222  nndivtr  12246  znegclb  12586  zmulcl  12598  zeo  12635  uz11  12834  uzp1  12850  eqreznegel  12905  rpnnen1lem6  12953  xrltne  13129  xneg11  13181  xnegdi  13214  xrsupss  13275  xrinfmss  13276  elfznelfzob  13725  modadd1  13860  modmul1  13876  om2uzlti  13902  bccmpl  14256  hashen  14294  fz1eqb  14301  hashfn  14322  hashnn0n0nn  14338  hashtpg  14433  eqwrd  14494  ccatopth  14653  ccatopth2  14654  swrdccatin2  14666  cj11  15096  rennim  15173  cnpart  15174  sqrmo  15185  sqrtgt0  15192  sqreulem  15293  sqreu  15294  cnsqrt00  15326  lo1o1  15463  lo1eq  15499  rlimeq  15500  sumss  15657  cvgcmp  15749  fprodser  15880  efne0  16027  dvdsabseq  16243  divalglem8  16330  bitsinv1lem  16369  pcfac  16819  prmreclem3  16838  sectmon  17716  yoniso  18225  oduposb  18269  lublecllem  18300  mgmb1mgm1  18561  sgrp2rid2  18794  grpinveu  18846  mulgass  18976  galcan  19153  symg1bas  19242  cayleylem2  19265  odbezout  19410  odeq1  19412  dprddomcld  19854  dvreq1  20203  unitrrg  20885  frgpcyg  21102  obslbs  21258  coe1tm  21766  tgss3  22458  uptx  23098  txindislem  23106  qtopeu  23189  hmeocnvb  23247  qtophmeo  23290  trufil  23383  ufinffr  23402  ghmcnp  23588  tgioo  24281  lmmcvg  24747  bcth3  24817  ovolunlem1a  24982  vitali  25099  ismbf  25114  ismbfcn  25115  rolle  25476  itgsubstlem  25534  vieta1lem2  25793  elqaalem3  25803  aacjcl  25809  efif1olem4  26023  lognegb  26067  logcj  26083  argimgt0  26089  logdmnrp  26118  logcnlem3  26121  logrec  26235  dcubic  26318  isppw  26585  rplogsumlem2  26955  pntpbnd1  27056  sltres  27132  nosupno  27173  nosupres  27177  noinfno  27188  noinfres  27192  negs11  27490  divsmo  27601  axlowdimlem16  28182  usgr0vb  28461  nbgrssvwo2  28586  redwlk  28896  usgr2pthspth  28986  usgr2pth  28988  wlkswwlksf1o  29100  wlklnwwlkln2lem  29103  wpthswwlks2on  29182  clwlkclwwlkf  29228  wwlksubclwwlk  29278  frgr0v  29482  grpoinveu  29737  grpoinvf  29750  diporthcom  29934  norm1exi  30468  shmodsi  30607  shmodi  30608  dfch2  30625  orthin  30664  chssoc  30714  spansncvi  30870  kbpj  31174  lnopunilem1  31228  cnlnssadj  31298  bra11  31326  strlem4  31472  strlem5  31473  hstrlem4  31480  hstrlem5  31481  dmdmd  31518  mdslle1i  31535  mdslle2i  31536  mdslmd1lem1  31543  atcvatlem  31603  atcvat4i  31615  mdsymlem3  31623  bcm1n  31977  xmulcand  32058  xreceu  32059  tpr2rico  32823  bnj1125  33934  revwlkb  34047  umgr2cycllem  34062  mrsubff1  34436  mvhf1  34481  funpsstri  34668  btwnintr  34922  idinside  34987  btwnconn1lem13  35002  fneval  35142  bj-equsal1t  35605  bj-brrelex12ALT  35853  bj-elid6  35956  bj-isrvec2  36086  bj-bary1lem1  36097  bj-bary1  36098  fvineqsnf1  36196  wl-equsal1i  36317  uncf  36372  matunitlindflem2  36390  poimirlem4  36397  poimirlem9  36402  ismtybndlem  36580  grpoeqdivid  36655  0rngo  36801  imaexALTV  37105  dmqseqim  37432  ax12indalem  37721  ax12inda2ALT  37722  lcvexchlem4  37813  lcvexchlem5  37814  opcon3b  37972  2dim  38247  ps-1  38254  paddclN  38619  ltrnnid  38913  cdleme22b  39118  dihmeetlem13N  40096  dih1dimatlem  40106  dihlspsnat  40110  remulcan2d  41065  nnaddcom  41070  sn-addcand  41174  sn-addcan2d  41176  onsupneqmaxlim0  41844  sqrtcval  42263  frege58c  42543  gneispa  42752  nzss  42947  expgrowth  42965  sbiota1  43064  f1cof1b  45658  f1ocof1ob2  45663  fafv2elrnb  45816  sbgoldbwt  46318  dignn0flhalflem1  47141  rrxlinesc  47261  aacllem  47688