Theorem imbitrrid 246

Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)

Hypotheses

Ref	Expression
imbitrrid.1	⊢ (𝜑 → 𝜃)
imbitrrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
imbitrrid	⊢ (𝜒 → (𝜑 → 𝜓))

Proof of Theorem imbitrrid

Step	Hyp	Ref	Expression
1		imbitrrid.1	. 2 ⊢ (𝜑 → 𝜃)
2		imbitrrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	bicomd 223	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	imbitrid 244	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:  syl5ibrcom  247  biimprd  248  exdistrf  2452  pm2.61ne  3018  spcimgft  3492  unineq  4229  elpreqprlem  4810  oteqex  5448  otel3xp  5670  eqrelrdv2  5744  breldmg  5858  elrnmpt1  5909  cnveqb  6154  cnveq0  6155  predpoirr  6291  predfrirr  6292  limelon  6382  f1ssf1  6806  ndmfv  6866  eqfnun  6983  ffvresb  7072  isomin  7285  isofrlem  7288  oprabidw  7391  caovord3d  7570  eldifpw  7715  ssonuni  7727  onsucuni2  7778  ordzsl  7789  tfindsg  7805  findsg  7841  oteqimp  7954  frxp  8069  poxp  8071  fnwelem  8074  tfrlem11  8320  ord1eln01  8424  ord2eln012  8425  oacl  8463  omcl  8464  oecl  8465  oa0r  8466  om0r  8467  om1r  8471  oe1m  8473  oaordi  8474  oawordri  8478  oaass  8489  oarec  8490  omwordri  8500  odi  8507  omass  8508  oewordri  8521  oeworde  8522  oeordsuc  8523  oelim2  8524  oeoa  8526  oeoelem  8527  oeoe  8528  nnm0r  8539  nnacl  8540  nnacom  8546  nnaordi  8547  nnaass  8551  nndi  8552  nnmass  8553  nnmsucr  8554  nnmcom  8555  omabs  8580  brecop  8750  eceqoveq  8762  elpm2r  8785  map0g  8825  undifixp  8875  fundmen  8971  mapxpen  9074  mapunen  9077  pssnn  9096  php  9134  unxpdomlem2  9160  f1vrnfibi  9245  elfir  9321  wemapso2lem  9460  wdompwdom  9486  inf3lem1  9540  inf3lem3  9542  cantnfval2  9581  cantnfp1lem3  9592  r1sdom  9689  r1tr  9691  carden2a  9881  fidomtri2  9909  prdom2  9919  infxpenlem  9926  acndom  9964  fodomacn  9969  wdomfil  9974  alephon  9982  alephordi  9987  alephle  10001  alephfplem3  10019  dfac2a  10043  kmlem9  10072  cflm  10163  cfslb  10179  cfslbn  10180  infpssrlem3  10218  infpssrlem4  10219  fin23lem21  10252  fin23lem30  10255  isf34lem7  10292  isf34lem6  10293  fin67  10308  isfin7-2  10309  fin1a2lem7  10319  fin1a2lem10  10322  iundom2g  10453  konigthlem  10482  alephreg  10496  gchdomtri  10543  wunr1om  10633  tskr1om  10681  inar1  10689  grur1a  10733  indpi  10821  genpprecl  10915  genpnmax  10921  addcmpblnr  10983  recexsrlem  11017  map2psrpr  11024  ax1rid  11075  axpre-mulgt0  11082  ltle  11225  nnmulcl  12189  nnsub  12212  nn0sub  12478  nneo  12604  uz11  12804  xrltle  13091  xltnegi  13159  xrsupsslem  13250  xrinfmsslem  13251  xrub  13255  supxrunb1  13262  supxrunb2  13263  om2uzuzi  13902  uzrdgxfr  13920  seqcl2  13973  seqfveq2  13977  seqshft2  13981  seqsplit  13988  seqcaopr3  13990  seqf1olem2a  13993  seqid2  14001  seqhomo  14002  ser1const  14011  m1expcl2  14038  expadd  14057  expmul  14060  faclbnd  14243  hashfzp1  14384  hashmap  14388  hashf1lem2  14409  hashf1  14410  seqcoll  14417  wrdsymb0  14502  len0nnbi  14504  eqs1  14566  swrdnd2  14609  wrd2ind  14676  pfxccatin12lem2c  14683  pfxccatin12lem2  14684  swrdccatin1d  14696  repswccat  14739  repswcshw  14765  cshwcshid  14780  rtrclreclem3  15013  rtrclreclem4  15014  dfrtrcl2  15015  relexpindlem  15016  relexpind  15017  rtrclind  15018  recan  15290  rexanre  15300  rlimcn3  15543  caurcvg2  15631  fsumiun  15775  efexp  16059  rpnnen2lem12  16183  dvdstr  16254  alzdvds  16280  zob  16319  sumeven  16347  sumodd  16348  bitsinv1  16402  smu01lem  16445  smupval  16448  smueqlem  16450  smumullem  16452  seq1st  16531  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  cncongr2  16628  prmdiveq  16747  odzdvds  16757  pythagtriplem2  16779  pcexp  16821  vdwlem13  16955  ramz  16987  prmolefac  17008  elrestr  17382  xpsff1o  17522  subsubc  17811  clatl  18465  frmdgsum  18821  sursubmefmnd  18855  injsubmefmnd  18856  smndex1mndlem  18871  dfgrp3e  19007  mulgneg2  19075  mulgnnass  19076  mhmmulg  19082  gsumwrev  19332  symgextf1lem  19386  symgfixelsi  19401  pmtrdifellem4  19445  sylow1lem1  19564  efgsfo  19705  efgred  19714  cyggexb  19865  gsumzres  19875  gsum2dlem2  19937  mulgass2  20281  rngimcnv  20427  funcrngcsetc  20608  funcrngcsetcALT  20609  rhmsscrnghm  20633  funcringcsetc  20642  lmodprop2d  20910  lspsnne2  21108  lspsneu  21113  cnfldmulg  21393  cnfldexp  21394  zrhpsgnelbas  21584  assapropd  21861  mplcoe1  22025  mplcoe3  22026  mplcoe5  22028  mhpvarcl  22124  ply1sclf1  22264  mat1scmat  22514  restopn2  23152  cnpf2  23225  cmpfi  23383  txcn  23601  txlm  23623  xkoptsub  23629  xkopjcn  23631  ufildr  23906  cnflf  23977  fclsnei  23994  fclscmp  24005  ufilcmp  24007  cnfcf  24017  symgtgp  24081  isxms2  24423  met2ndc  24498  metustbl  24541  tngngp2  24627  clmmulg  25078  iscau4  25256  ovolunlem1a  25473  ovolicc2lem4  25497  volfiniun  25524  voliunlem1  25527  volsup  25533  dvnadd  25906  dvnres  25908  dvcobr  25923  ply1nzb  26098  plypf1  26187  dgrle  26218  coeaddlem  26224  dgrlt  26241  dvntaylp  26348  cxpmul2  26666  rlimcnp  26942  facgam  27043  wilthlem2  27046  isnsqf  27112  musum  27168  chtub  27189  chpval2  27195  gausslemma2dlem0i  27341  dchrisumlem1  27466  qabvexp  27603  ostthlem2  27605  nodenselem8  27669  lesrec  27805  bday1  27820  sltsleft  27866  sltsright  27867  oncutlt  28270  noseqind  28298  dfnns2  28378  bdaypw2n0bnd  28470  axsegconlem1  29000  ax5seglem4  29015  ax5seglem5  29016  axlowdimlem15  29039  axcontlem2  29048  axcontlem4  29050  incistruhgr  29162  upgredg2vtx  29224  upgredgpr  29225  numedglnl  29227  uhgr2edg  29291  nbupgruvtxres  29490  cusgrfilem1  29539  wlkres  29752  wlkp1lem2  29756  pthdivtx  29810  pthdlem2lem  29850  wlkiswwlks2lem4  29955  wwlksnredwwlkn0  29979  wwlksnextwrd  29980  wwlksnfi  29989  wwlksnextprop  29995  clwlkclwwlklem2a  30083  clwlkclwwlkf1lem2  30090  erclwwlksym  30106  clwwlkf1  30134  eleclclwwlknlem2  30146  erclwwlknsym  30155  clwwlknonex2  30194  eupth2lem3lem6  30318  frgr3vlem1  30358  3vfriswmgrlem  30362  wlkl0  30452  sspval  30809  nmosetre  30850  nmobndseqi  30865  nmobndseqiALT  30866  orthcom  31194  shsva  31406  shmodsi  31475  h1datomi  31667  nmopsetretALT  31949  nmfnsetre  31963  lnopcnbd  32122  pjclem4  32285  pj3si  32293  ssmd1  32397  atom1d  32439  chjatom  32443  atcvat4i  32483  cdj3lem2a  32522  cdj3lem3a  32525  disjunsn  32679  unitdivcld  34061  xrge0iifiso  34095  dya2iocuni  34443  bnj168  34889  bnj535  35048  bnj590  35068  bnj594  35070  bnj938  35095  bnj1118  35142  bnj1128  35148  fnrelpredd  35250  deranglem  35364  subfacp1lem6  35383  subfacval2  35385  cvmlift2lem12  35512  satffun  35607  mrsubvrs  35720  msrrcl  35741  mclsax  35767  dfon2lem6  35984  rdgprc  35990  ifscgr  36242  btwncolinear1  36267  hfelhf  36379  opnrebl2  36519  nn0prpw  36521  ordcmp  36645  findreccl  36651  nndivlub  36656  axtcond  36676  dfttc2g  36704  mh-inf3f1  36739  bj-rest0  37421  bj-isrvec2  37630  topdifinffinlem  37677  iooelexlt  37692  rdgeqoa  37700  exrecfnlem  37709  wl-mo3t  37915  matunitlindflem2  37952  poimirlem2  37957  poimirlem23  37978  poimirlem28  37983  poimirlem29  37984  poimirlem31  37986  poimirlem32  37987  sdclem2  38077  sdclem1  38078  prdsbnd2  38130  ismtyval  38135  rrnequiv  38170  isexid2  38190  ismndo1  38208  exidreslem  38212  rngo2  38242  rngoueqz  38275  risci  38322  eldisjdmqsim  39152  prtlem11  39326  prtlem15  39335  cvrat4  39903  lcfl6  41960  dvdsexpnn0  42780  harval3  43983  clcnvlem  44068  cnvrcl0  44070  cnvtrcl0  44071  iunrelexpmin1  44153  iunrelexpmin2  44157  ormkglobd  47321  fcoresf1b  47530  aovmpt4g  47661  elsetpreimafvbi  47863  iccpartiltu  47894  iccpartgt  47899  iccpartgel  47901  reuopreuprim  47998  fmtnofac1  48045  gbepos  48246  grtrif1o  48430  grtriclwlk3  48433  isubgr3stgrlem4  48457  gpgprismgr4cycllem3  48585  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem5lem1  48608  pgnbgreunbgrlem5lem2  48609  pgnbgreunbgrlem5lem3  48610  pgnbgreunbgrlem6  48612  pgnbgreunbgr  48613  ellcoellss  48923  dignn0flhalflem2  49104  nn0sumshdiglemB  49108  1arympt1  49126  opth1neg  49313  opth2neg  49314  oppccatb  49503  fullthinc  49937