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  2277  dvelimdf  2454  ceqsal1t  3463  gencl  3472  spsbc  3742  ssnelpss  4055  sscon34b  4245  dfnfc2  4873  uniintsn  4928  prexOLD  5378  copsexgw  5436  copsexg  5437  posn  5708  optocl  5716  optoclOLD  5717  funimass1  6572  f1ocnvb  6785  eqfnfv2  6976  elpreima  7002  fconst5  7152  dff13  7200  f1ocnvfv  7224  f1ocnvfvb  7225  fliftfun  7258  eusvobj2  7350  sorpsscmpl  7679  ssonprc  7732  dmfex  7847  xpexr  7860  xpexcnv  7862  relcnvexb  7868  frxp  8067  mpoxopn0yelv  8154  rntpos  8180  oawordeulem  8480  oalimcl  8486  odi  8505  omeulem2  8509  oeeulem  8528  nnasmo  8590  erexb  8660  findcard2  9090  unxpdomlem2  9158  dif1ennnALT  9178  enp1ilem  9179  isfinite2  9199  fodomfib  9230  fodomfibOLD  9232  inf0  9531  rankxplim2  9793  scott0  9799  djuexb  9822  ficardom  9874  cardaleph  10000  dfac5  10040  cflim2  10174  fin23lem23  10237  fin23lem28  10251  isf32lem5  10268  domtriomlem  10353  ac6num  10390  zorn2lem5  10411  zorn2lem6  10412  iunfo  10450  axrepndlem2  10505  axregnd  10516  hargch  10585  addcanpi  10811  mulcanpi  10812  indpi  10819  ltaddnq  10886  ltexnq  10887  prlem934  10945  ltaddpr2  10947  ltaprlem  10956  supsrlem  11023  ssxr  11204  ltxrlt  11205  addcan  11319  addcan2  11320  neg11  11434  negreb  11448  mulcand  11772  receu  11784  ldiv  11978  lemul1a  11998  cju  12144  nn1suc  12185  nnaddcl  12186  nnaddcom  12190  nndivtr  12213  znegclb  12553  zmulcl  12565  zeo  12604  uz11  12802  uzp1  12814  eqreznegel  12873  rpnnen1lem6  12921  xrltne  13103  xneg11  13156  xnegdi  13189  xrsupss  13250  xrinfmss  13251  elfznelfzob  13718  modadd1  13856  modmul1  13875  om2uzlti  13901  bccmpl  14260  hashen  14298  fz1eqb  14305  hashfn  14326  hashnn0n0nn  14342  hashtpg  14436  eqwrd  14508  ccatopth  14667  ccatopth2  14668  swrdccatin2  14680  cj11  15113  rennim  15190  cnpart  15191  sqrmo  15202  sqrtgt0  15209  sqreulem  15311  sqreu  15312  cnsqrt00  15344  lo1o1  15483  lo1eq  15519  rlimeq  15520  sumss  15675  cvgcmp  15768  fprodser  15903  efne0d  16051  efne0OLD  16053  dvdsabseq  16271  divalglem8  16358  bitsinv1lem  16399  pcfac  16859  prmreclem3  16878  sectmon  17738  yoniso  18240  oduposb  18282  lublecllem  18313  chnrev  18582  mgmb1mgm1  18612  sgrp2rid2  18886  grpinveu  18939  grpinv11  18972  mulgass  19076  galcan  19268  symg1bas  19355  cayleylem2  19377  odbezout  19522  odeq1  19524  dprddomcld  19967  dvreq1  20380  unitrrg  20669  frgpcyg  21561  obslbs  21718  coe1tm  22247  tgss3  22960  uptx  23599  txindislem  23607  qtopeu  23690  hmeocnvb  23748  qtophmeo  23791  trufil  23884  ufinffr  23903  ghmcnp  24089  tgioo  24770  lmmcvg  25237  bcth3  25307  ovolunlem1a  25472  vitali  25589  ismbf  25604  ismbfcn  25605  rolle  25966  itgsubstlem  26027  vieta1lem2  26290  elqaalem3  26300  aacjcl  26306  efif1olem4  26525  lognegb  26570  logcj  26586  argimgt0  26592  logdmnrp  26621  logcnlem3  26624  logrec  26744  dcubic  26827  isppw  27095  rplogsumlem2  27467  pntpbnd1  27568  ltsres  27645  nosupno  27686  nosupres  27690  noinfno  27701  noinfres  27705  negs11  28060  divsmo  28195  n0subs  28374  n0ltsp1le  28376  z12negsclb  28492  axlowdimlem16  29045  usgr0vb  29325  nbgrssvwo2  29450  redwlk  29759  usgr2pthspth  29850  usgr2pth  29852  wlkswwlksf1o  29967  wlklnwwlkln2lem  29970  wpthswwlks2on  30052  clwlkclwwlkf  30098  wwlksubclwwlk  30148  frgr0v  30352  grpoinveu  30610  grpoinvf  30623  diporthcom  30807  norm1exi  31341  shmodsi  31480  shmodi  31481  dfch2  31498  orthin  31537  chssoc  31587  spansncvi  31743  kbpj  32047  lnopunilem1  32101  cnlnssadj  32171  bra11  32199  strlem4  32345  strlem5  32346  hstrlem4  32353  hstrlem5  32354  dmdmd  32391  mdslle1i  32408  mdslle2i  32409  mdslmd1lem1  32416  atcvatlem  32476  atcvat4i  32488  mdsymlem3  32496  bcm1n  32888  xmulcand  33000  xreceu  33001  tpr2rico  34077  bnj1125  35155  revwlkb  35329  umgr2cycllem  35343  mrsubff1  35717  mvhf1  35762  funpsstri  35969  btwnintr  36222  idinside  36287  btwnconn1lem13  36302  fneval  36555  bj-equsal1t  37142  bj-brrelex12ALT  37387  bj-elid6  37497  bj-isrvec2  37627  bj-bary1lem1  37638  bj-bary1  37639  fvineqsnf1  37737  wl-equsal1i  37880  uncf  37931  matunitlindflem2  37949  poimirlem4  37956  poimirlem9  37961  ismtybndlem  38138  grpoeqdivid  38213  0rngo  38359  dmqseqim  39073  eldisjdmqsim2  39148  qmapeldisjsim  39192  rnqmapeleldisjsim  39194  ax12indalem  39402  ax12inda2ALT  39403  lcvexchlem4  39494  lcvexchlem5  39495  opcon3b  39653  2dim  39927  ps-1  39934  paddclN  40299  ltrnnid  40593  cdleme22b  40798  dihmeetlem13N  41776  dih1dimatlem  41786  dihlspsnat  41790  eqresfnbd  42684  remulcan2d  42706  log11d  42789  sn-addcand  42863  sn-addcan2d  42865  rediveud  42886  onsupneqmaxlim0  43667  sqrtcval  44083  frege58c  44363  gneispa  44572  nzss  44759  expgrowth  44777  sbiota1  44876  ormkglobd  47318  f1cof1b  47522  f1ocof1ob2  47527  fafv2elrnb  47680  sbgoldbwt  48250  dignn0flhalflem1  49088  rrxlinesc  49208  oppff1  49620  aacllem  50273