Theorem imbitrid 245

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  syl5ibcom  246  imbitrrid  247  sbft  2281  dvelimdf  2457  ceqsal1t  3465  gencl  3474  spsbc  3743  ssnelpss  4052  sscon34b  4239  dfnfc2  4867  uniintsn  4922  prexOLD  5379  copsexgwOLD  5438  copsexg  5439  posn  5711  optocl  5719  optoclOLD  5720  funimass1  6574  f1ocnvb  6787  eqfnfv2  6979  elpreima  7006  fconst5  7157  dff13  7205  f1ocnvfv  7229  f1ocnvfvb  7230  fliftfun  7263  eusvobj2  7355  sorpsscmpl  7684  ssonprc  7737  dmfex  7852  xpexr  7865  xpexcnv  7867  relcnvexb  7873  frxp  8073  mpoxopn0yelv  8160  rntpos  8186  oawordeulem  8486  oalimcl  8492  odi  8511  omeulem2  8515  oeeulem  8534  nnasmo  8596  erexb  8666  findcard2  9096  unxpdomlem2  9164  dif1ennnALT  9184  enp1ilem  9185  isfinite2  9205  fodomfib  9236  fodomfibOLD  9238  inf0  9540  rankxplim2  9802  scott0  9808  djuexb  9831  ficardom  9883  cardaleph  10009  dfac5  10049  cflim2  10183  fin23lem23  10246  fin23lem28  10260  isf32lem5  10277  domtriomlem  10362  ac6num  10399  zorn2lem5  10420  zorn2lem6  10421  iunfo  10459  axrepndlem2  10514  axregnd  10525  hargch  10594  addcanpi  10820  mulcanpi  10821  indpi  10828  ltaddnq  10895  ltexnq  10896  prlem934  10954  ltaddpr2  10956  ltaprlem  10965  supsrlem  11032  ssxr  11213  ltxrlt  11214  addcan  11328  addcan2  11329  neg11  11443  negreb  11457  mulcand  11781  receu  11793  ldiv  11987  lemul1a  12007  cju  12153  nn1suc  12194  nnaddcl  12195  nnaddcom  12199  nndivtr  12222  znegclb  12562  zmulcl  12574  zeo  12613  uz11  12811  uzp1  12823  eqreznegel  12882  rpnnen1lem6  12930  xrltne  13112  xneg11  13165  xnegdi  13198  xrsupss  13259  xrinfmss  13260  elfznelfzob  13727  modadd1  13865  modmul1  13884  om2uzlti  13910  bccmpl  14269  hashen  14307  fz1eqb  14314  hashfn  14335  hashnn0n0nn  14351  hashtpg  14445  eqwrd  14517  ccatopth  14676  ccatopth2  14677  swrdccatin2  14689  cj11  15122  rennim  15199  cnpart  15200  sqrmo  15211  sqrtgt0  15218  sqreulem  15320  sqreu  15321  cnsqrt00  15353  lo1o1  15492  lo1eq  15528  rlimeq  15529  sumss  15684  cvgcmp  15777  fprodser  15912  efne0d  16060  efne0OLD  16062  dvdsabseq  16280  divalglem8  16367  bitsinv1lem  16408  pcfac  16868  prmreclem3  16887  sectmon  17747  yoniso  18249  oduposb  18291  lublecllem  18322  chnrev  18591  mgmb1mgm1  18621  sgrp2rid2  18895  grpinveu  18948  grpinv11  18981  mulgass  19085  galcan  19277  symg1bas  19364  cayleylem2  19386  odbezout  19531  odeq1  19533  dprddomcld  19976  dvreq1  20389  unitrrg  20682  frgpcyg  21555  obslbs  21712  coe1tm  22266  tgss3  22976  uptx  23615  txindislem  23623  qtopeu  23706  hmeocnvb  23764  qtophmeo  23807  trufil  23900  ufinffr  23919  ghmcnp  24105  tgioo  24786  lmmcvg  25253  bcth3  25323  ovolunlem1a  25488  vitali  25605  ismbf  25620  ismbfcn  25621  rolle  25982  itgsubstlem  26040  vieta1lem2  26302  elqaalem3  26312  aacjcl  26318  efif1olem4  26534  lognegb  26579  logcj  26595  argimgt0  26601  logdmnrp  26630  logcnlem3  26633  logrec  26752  dcubic  26835  isppw  27102  rplogsumlem2  27473  pntpbnd1  27574  ltsres  27651  nosupno  27692  nosupres  27696  noinfno  27707  noinfres  27711  negs11  28066  divsmo  28201  n0subs  28380  n0ltsp1le  28382  z12negsclb  28498  axlowdimlem16  29051  usgr0vb  29331  nbgrssvwo2  29456  redwlk  29764  usgr2pthspth  29855  usgr2pth  29857  wlkswwlksf1o  29972  wlklnwwlkln2lem  29975  wpthswwlks2on  30057  clwlkclwwlkf  30103  wwlksubclwwlk  30153  frgr0v  30357  grpoinveu  30615  grpoinvf  30628  diporthcom  30812  norm1exi  31346  shmodsi  31485  shmodi  31486  dfch2  31503  orthin  31542  chssoc  31592  spansncvi  31748  kbpj  32052  lnopunilem1  32106  cnlnssadj  32176  bra11  32204  strlem4  32350  strlem5  32351  hstrlem4  32358  hstrlem5  32359  dmdmd  32396  mdslle1i  32413  mdslle2i  32414  mdslmd1lem1  32421  atcvatlem  32481  atcvat4i  32493  mdsymlem3  32501  bcm1n  32894  xmulcand  33006  xreceu  33007  tpr2rico  34103  bnj1125  35181  revwlkb  35355  umgr2cycllem  35369  mrsubff1  35743  mvhf1  35788  funpsstri  35995  btwnintr  36248  idinside  36313  btwnconn1lem13  36328  fneval  36581  bj-equsal1t  37176  bj-brrelex12ALT  37421  bj-elid6  37531  bj-isrvec2  37661  bj-bary1lem1  37672  bj-bary1  37673  fvineqsnf1  37773  wl-equsal1i  37916  uncf  37967  matunitlindflem2  37985  poimirlem4  37992  poimirlem9  37997  ismtybndlem  38174  grpoeqdivid  38249  0rngo  38395  dmqseqim  39109  eldisjdmqsim2  39184  qmapeldisjsim  39228  rnqmapeleldisjsim  39230  ax12indalem  39438  ax12inda2ALT  39439  lcvexchlem4  39530  lcvexchlem5  39531  opcon3b  39689  2dim  39963  ps-1  39970  paddclN  40335  ltrnnid  40629  cdleme22b  40834  dihmeetlem13N  41812  dih1dimatlem  41822  dihlspsnat  41826  eqresfnbd  42720  remulcan2d  42741  log11d  42824  sn-addcand  42898  sn-addcan2d  42900  rediveud  42921  onsupneqmaxlim0  43670  sqrtcval  44086  frege58c  44366  gneispa  44575  nzss  44762  expgrowth  44780  sbiota1  44879  ormkglobd  47321  f1cof1b  47541  f1ocof1ob2  47546  fafv2elrnb  47699  sbgoldbwt  48269  dignn0flhalflem1  49107  rrxlinesc  49227  oppff1  49639  aacllem  50292