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  2270  dvelimdf  2447  ceqsal1t  3480  gencl  3489  spsbc  3766  ssnelpss  4077  sscon34b  4267  dfnfc2  4893  uniintsn  4949  prex  5392  copsexgw  5450  copsexg  5451  posn  5724  optocl  5733  funimass1  6598  f1ocnvb  6813  eqfnfv2  7004  elpreima  7030  fconst5  7180  dff13  7229  f1ocnvfv  7253  f1ocnvfvb  7254  fliftfun  7287  eusvobj2  7379  sorpsscmpl  7710  ssonprc  7763  dmfex  7881  xpexr  7894  xpexcnv  7896  relcnvexb  7902  frxp  8105  mpoxopn0yelv  8192  rntpos  8218  oawordeulem  8518  oalimcl  8524  odi  8543  omeulem2  8547  oeeulem  8565  nnasmo  8627  erexb  8696  findcard2  9128  unxpdomlem2  9198  dif1ennnALT  9222  enp1ilem  9223  isfinite2  9245  fodomfib  9280  fodomfibOLD  9282  inf0  9574  rankxplim2  9833  scott0  9839  djuexb  9862  ficardom  9914  cardaleph  10042  dfac5  10082  cflim2  10216  fin23lem23  10279  fin23lem28  10293  isf32lem5  10310  domtriomlem  10395  ac6num  10432  zorn2lem5  10453  zorn2lem6  10454  iunfo  10492  axrepndlem2  10546  axregnd  10557  hargch  10626  addcanpi  10852  mulcanpi  10853  indpi  10860  ltaddnq  10927  ltexnq  10928  prlem934  10986  ltaddpr2  10988  ltaprlem  10997  supsrlem  11064  ssxr  11243  ltxrlt  11244  addcan  11358  addcan2  11359  neg11  11473  negreb  11487  mulcand  11811  receu  11823  ldiv  12016  lemul1a  12036  cju  12182  nn1suc  12208  nnaddcl  12209  nndivtr  12233  znegclb  12570  zmulcl  12582  zeo  12620  uz11  12818  uzp1  12834  eqreznegel  12893  rpnnen1lem6  12941  xrltne  13123  xneg11  13175  xnegdi  13208  xrsupss  13269  xrinfmss  13270  elfznelfzob  13734  modadd1  13870  modmul1  13889  om2uzlti  13915  bccmpl  14274  hashen  14312  fz1eqb  14319  hashfn  14340  hashnn0n0nn  14356  hashtpg  14450  eqwrd  14522  ccatopth  14681  ccatopth2  14682  swrdccatin2  14694  cj11  15128  rennim  15205  cnpart  15206  sqrmo  15217  sqrtgt0  15224  sqreulem  15326  sqreu  15327  cnsqrt00  15359  lo1o1  15498  lo1eq  15534  rlimeq  15535  sumss  15690  cvgcmp  15782  fprodser  15915  efne0d  16063  efne0OLD  16065  dvdsabseq  16283  divalglem8  16370  bitsinv1lem  16411  pcfac  16870  prmreclem3  16889  sectmon  17744  yoniso  18246  oduposb  18288  lublecllem  18319  mgmb1mgm1  18582  sgrp2rid2  18853  grpinveu  18906  grpinv11  18939  mulgass  19043  galcan  19236  symg1bas  19321  cayleylem2  19343  odbezout  19488  odeq1  19490  dprddomcld  19933  dvreq1  20320  unitrrg  20612  frgpcyg  21483  obslbs  21639  coe1tm  22159  tgss3  22873  uptx  23512  txindislem  23520  qtopeu  23603  hmeocnvb  23661  qtophmeo  23704  trufil  23797  ufinffr  23816  ghmcnp  24002  tgioo  24684  lmmcvg  25161  bcth3  25231  ovolunlem1a  25397  vitali  25514  ismbf  25529  ismbfcn  25530  rolle  25894  itgsubstlem  25955  vieta1lem2  26219  elqaalem3  26229  aacjcl  26235  efif1olem4  26454  lognegb  26499  logcj  26515  argimgt0  26521  logdmnrp  26550  logcnlem3  26553  logrec  26673  dcubic  26756  isppw  27024  rplogsumlem2  27396  pntpbnd1  27497  sltres  27574  nosupno  27615  nosupres  27619  noinfno  27630  noinfres  27634  negs11  27955  divsmo  28087  n0subs  28253  n0sltp1le  28255  zs12negsclb  28341  axlowdimlem16  28884  usgr0vb  29164  nbgrssvwo2  29289  redwlk  29600  usgr2pthspth  29692  usgr2pth  29694  wlkswwlksf1o  29809  wlklnwwlkln2lem  29812  wpthswwlks2on  29891  clwlkclwwlkf  29937  wwlksubclwwlk  29987  frgr0v  30191  grpoinveu  30448  grpoinvf  30461  diporthcom  30645  norm1exi  31179  shmodsi  31318  shmodi  31319  dfch2  31336  orthin  31375  chssoc  31425  spansncvi  31581  kbpj  31885  lnopunilem1  31939  cnlnssadj  32009  bra11  32037  strlem4  32183  strlem5  32184  hstrlem4  32191  hstrlem5  32192  dmdmd  32229  mdslle1i  32246  mdslle2i  32247  mdslmd1lem1  32254  atcvatlem  32314  atcvat4i  32326  mdsymlem3  32334  bcm1n  32718  xmulcand  32841  xreceu  32842  tpr2rico  33902  bnj1125  34982  revwlkb  35113  umgr2cycllem  35127  mrsubff1  35501  mvhf1  35546  funpsstri  35753  btwnintr  36007  idinside  36072  btwnconn1lem13  36087  fneval  36340  bj-equsal1t  36810  bj-brrelex12ALT  37055  bj-elid6  37158  bj-isrvec2  37288  bj-bary1lem1  37299  bj-bary1  37300  fvineqsnf1  37398  wl-equsal1i  37532  uncf  37593  matunitlindflem2  37611  poimirlem4  37618  poimirlem9  37623  ismtybndlem  37800  grpoeqdivid  37875  0rngo  38021  dmqseqim  38648  ax12indalem  38938  ax12inda2ALT  38939  lcvexchlem4  39030  lcvexchlem5  39031  opcon3b  39189  2dim  39464  ps-1  39471  paddclN  39836  ltrnnid  40130  cdleme22b  40335  dihmeetlem13N  41313  dih1dimatlem  41323  dihlspsnat  41327  eqresfnbd  42220  remulcan2d  42245  nnaddcom  42256  log11d  42334  sn-addcand  42408  sn-addcan2d  42410  rediveud  42431  onsupneqmaxlim0  43213  sqrtcval  43630  frege58c  43910  gneispa  44119  nzss  44306  expgrowth  44324  sbiota1  44423  ormkglobd  46873  f1cof1b  47078  f1ocof1ob2  47083  fafv2elrnb  47236  sbgoldbwt  47778  dignn0flhalflem1  48604  rrxlinesc  48724  oppff1  49137  aacllem  49790