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  2260  dvelimdf  2447  ceqsal1t  3504  gencl  3515  vtoclgft  3540  spsbc  3790  ssnelpss  4111  sscon34b  4294  dfnfc2  4933  uniintsn  4991  prex  5432  copsexgw  5490  copsexg  5491  posn  5761  optocl  5770  funimass1  6630  f1ocnvb  6846  eqfnfv2  7033  elpreima  7059  fconst5  7209  dff13  7257  f1ocnvfv  7279  f1ocnvfvb  7280  fliftfun  7312  eusvobj2  7404  sorpsscmpl  7727  ssonprc  7778  dmfex  7901  xpexr  7912  xpexcnv  7914  relcnvexb  7920  frxp  8115  mpoxopn0yelv  8201  rntpos  8227  oawordeulem  8557  oalimcl  8563  odi  8582  omeulem2  8586  oeeulem  8604  nnasmo  8665  erexb  8731  findcard2  9167  unxpdomlem2  9254  dif1ennnALT  9280  enp1ilem  9281  findcard2OLD  9287  isfinite2  9304  unfiOLD  9316  fodomfib  9329  inf0  9619  rankxplim2  9878  scott0  9884  djuexb  9907  ficardom  9959  cardaleph  10087  dfac5  10126  cflim2  10261  fin23lem23  10324  fin23lem28  10338  isf32lem5  10355  domtriomlem  10440  ac6num  10477  zorn2lem5  10498  zorn2lem6  10499  iunfo  10537  axrepndlem2  10591  axregnd  10602  hargch  10671  addcanpi  10897  mulcanpi  10898  indpi  10905  ltaddnq  10972  ltexnq  10973  prlem934  11031  ltaddpr2  11033  ltaprlem  11042  supsrlem  11109  ssxr  11288  ltxrlt  11289  addcan  11403  addcan2  11404  neg11  11516  negreb  11530  mulcand  11852  receu  11864  ldiv  12053  lemul1a  12073  cju  12213  nn1suc  12239  nnaddcl  12240  nndivtr  12264  znegclb  12604  zmulcl  12616  zeo  12653  uz11  12852  uzp1  12868  eqreznegel  12923  rpnnen1lem6  12971  xrltne  13147  xneg11  13199  xnegdi  13232  xrsupss  13293  xrinfmss  13294  elfznelfzob  13743  modadd1  13878  modmul1  13894  om2uzlti  13920  bccmpl  14274  hashen  14312  fz1eqb  14319  hashfn  14340  hashnn0n0nn  14356  hashtpg  14451  eqwrd  14512  ccatopth  14671  ccatopth2  14672  swrdccatin2  14684  cj11  15114  rennim  15191  cnpart  15192  sqrmo  15203  sqrtgt0  15210  sqreulem  15311  sqreu  15312  cnsqrt00  15344  lo1o1  15481  lo1eq  15517  rlimeq  15518  sumss  15675  cvgcmp  15767  fprodser  15898  efne0  16045  dvdsabseq  16261  divalglem8  16348  bitsinv1lem  16387  pcfac  16837  prmreclem3  16856  sectmon  17734  yoniso  18243  oduposb  18287  lublecllem  18318  mgmb1mgm1  18581  sgrp2rid2  18844  grpinveu  18896  mulgass  19028  galcan  19210  symg1bas  19300  cayleylem2  19323  odbezout  19468  odeq1  19470  dprddomcld  19913  dvreq1  20303  unitrrg  21110  frgpcyg  21349  obslbs  21505  coe1tm  22016  tgss3  22710  uptx  23350  txindislem  23358  qtopeu  23441  hmeocnvb  23499  qtophmeo  23542  trufil  23635  ufinffr  23654  ghmcnp  23840  tgioo  24533  lmmcvg  25010  bcth3  25080  ovolunlem1a  25246  vitali  25363  ismbf  25378  ismbfcn  25379  rolle  25743  itgsubstlem  25801  vieta1lem2  26061  elqaalem3  26071  aacjcl  26077  efif1olem4  26291  lognegb  26335  logcj  26351  argimgt0  26357  logdmnrp  26386  logcnlem3  26389  logrec  26505  dcubic  26588  isppw  26855  rplogsumlem2  27225  pntpbnd1  27326  sltres  27402  nosupno  27443  nosupres  27447  noinfno  27458  noinfres  27462  negs11  27763  divsmo  27874  axlowdimlem16  28483  usgr0vb  28762  nbgrssvwo2  28887  redwlk  29197  usgr2pthspth  29287  usgr2pth  29289  wlkswwlksf1o  29401  wlklnwwlkln2lem  29404  wpthswwlks2on  29483  clwlkclwwlkf  29529  wwlksubclwwlk  29579  frgr0v  29783  grpoinveu  30040  grpoinvf  30053  diporthcom  30237  norm1exi  30771  shmodsi  30910  shmodi  30911  dfch2  30928  orthin  30967  chssoc  31017  spansncvi  31173  kbpj  31477  lnopunilem1  31531  cnlnssadj  31601  bra11  31629  strlem4  31775  strlem5  31776  hstrlem4  31783  hstrlem5  31784  dmdmd  31821  mdslle1i  31838  mdslle2i  31839  mdslmd1lem1  31846  atcvatlem  31906  atcvat4i  31918  mdsymlem3  31926  bcm1n  32274  xmulcand  32355  xreceu  32356  tpr2rico  33191  bnj1125  34302  revwlkb  34415  umgr2cycllem  34430  mrsubff1  34804  mvhf1  34849  funpsstri  35042  btwnintr  35296  idinside  35361  btwnconn1lem13  35376  fneval  35541  bj-equsal1t  36004  bj-brrelex12ALT  36252  bj-elid6  36355  bj-isrvec2  36485  bj-bary1lem1  36496  bj-bary1  36497  fvineqsnf1  36595  wl-equsal1i  36716  uncf  36771  matunitlindflem2  36789  poimirlem4  36796  poimirlem9  36801  ismtybndlem  36978  grpoeqdivid  37053  0rngo  37199  imaexALTV  37503  dmqseqim  37830  ax12indalem  38119  ax12inda2ALT  38120  lcvexchlem4  38211  lcvexchlem5  38212  opcon3b  38370  2dim  38645  ps-1  38652  paddclN  39017  ltrnnid  39311  cdleme22b  39516  dihmeetlem13N  40494  dih1dimatlem  40504  dihlspsnat  40508  eqresfnbd  41361  remulcan2d  41480  nnaddcom  41485  sn-addcand  41595  sn-addcan2d  41597  onsupneqmaxlim0  42276  sqrtcval  42695  frege58c  42975  gneispa  43184  nzss  43379  expgrowth  43397  sbiota1  43496  f1cof1b  46084  f1ocof1ob2  46089  fafv2elrnb  46242  sbgoldbwt  46744  dignn0flhalflem1  47389  rrxlinesc  47509  aacllem  47936