Theorem imbitrrid 249

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 226	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	imbitrid 247	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  syl5ibrcom  250  biimprd  251  exdistrf  2481  pm2.61ne  3045  spcimgft  3517  unineq  4243  elpreqprlem  4826  oteqex  5473  otel3xp  5697  eqrelrdv2  5771  breldmg  5889  elrnmpt1  5940  cnveqb  6186  cnveq0  6187  predpoirr  6323  predfrirr  6324  limelon  6415  f1ssf1  6843  ndmfv  6903  eqfnun  7022  ffvresb  7111  isomin  7325  isofrlem  7328  oprabidw  7431  caovord3d  7610  eldifpw  7755  ssonuni  7767  onsucuni2  7818  ordzsl  7829  tfindsg  7845  findsg  7882  oteqimp  7993  frxp  8110  poxp  8112  fnwelem  8115  tfrlem11  8363  ord1eln01  8469  ord2eln012  8470  oacl  8508  omcl  8509  oecl  8510  oa0r  8511  om0r  8512  om1r  8516  oe1m  8518  oaordi  8519  oawordri  8523  oaass  8534  oarec  8535  omwordri  8545  odi  8552  omass  8553  oewordri  8566  oeworde  8567  oeordsuc  8568  oelim2  8569  oeoa  8571  oeoelem  8572  oeoe  8573  nnm0r  8584  nnacl  8585  nnacom  8591  nnaordi  8592  nnaass  8596  nndi  8597  nnmass  8598  nnmsucr  8599  nnmcom  8600  omabs  8625  brecop  8796  eceqoveq  8808  elpm2r  8830  map0g  8870  undifixp  8920  fundmen  9016  mapxpen  9119  mapunen  9122  pssnn  9141  php  9179  unxpdomlem2  9205  f1vrnfibi  9287  elfir  9363  wemapso2lem  9502  wdompwdom  9528  inf3lem1  9585  inf3lem3  9587  cantnfval2  9626  cantnfp1lem3  9637  r1sdom  9734  r1tr  9736  carden2a  9940  fidomtri2  9968  prdom2  9978  infxpenlem  9985  acndom  10023  fodomacn  10028  wdomfil  10033  alephon  10041  alephordi  10046  alephle  10060  alephfplem3  10078  dfac2a  10101  kmlem9  10130  cflm  10221  cfslb  10238  cfslbn  10239  infpssrlem3  10277  infpssrlem4  10278  fin23lem21  10311  fin23lem30  10314  isf34lem7  10351  isf34lem6  10352  fin67  10367  isfin7-2  10368  fin1a2lem7  10378  fin1a2lem10  10381  iundom2g  10512  konigthlem  10541  alephreg  10555  gchdomtri  10602  wunr1om  10692  tskr1om  10740  inar1  10748  grur1a  10792  indpi  10880  genpprecl  10974  genpnmax  10980  addcmpblnr  11042  recexsrlem  11076  map2psrpr  11083  ax1rid  11134  axpre-mulgt0  11141  ltle  11286  nnmulcl  12245  nnsub  12268  nn0sub  12542  nneo  12668  uz11  12875  xrltle  13162  xltnegi  13230  xrsupsslem  13321  xrinfmsslem  13322  xrub  13326  supxrunb1  13333  supxrunb2  13334  om2uzuzi  13973  uzrdgxfr  13991  seqcl2  14044  seqfveq2  14048  seqshft2  14052  seqsplit  14059  seqcaopr3  14061  seqf1olem2a  14064  seqid2  14072  seqhomo  14073  ser1const  14082  m1expcl2  14109  expadd  14128  expmul  14131  faclbnd  14314  hashfzp1  14456  hashmap  14460  hashf1lem2  14481  hashf1  14482  seqcoll  14489  wrdsymb0  14574  len0nnbi  14576  eqs1  14638  swrdnd2  14681  wrd2ind  14748  pfxccatin12lem2c  14755  pfxccatin12lem2  14756  swrdccatin1d  14768  repswccat  14811  repswcshw  14837  cshwcshid  14852  rtrclreclem3  15085  rtrclreclem4  15086  dfrtrcl2  15087  relexpindlem  15088  relexpind  15089  rtrclind  15090  recan  15376  rexanre  15386  rlimcn3  15629  caurcvg2  15717  fsumiun  15861  efexp  16145  rpnnen2lem12  16269  dvdstr  16340  alzdvds  16366  zob  16405  sumeven  16433  sumodd  16434  bitsinv1  16488  smu01lem  16531  smupval  16534  smueqlem  16536  smumullem  16538  seq1st  16617  lcmfunsnlem2lem1  16684  lcmfunsnlem2lem2  16685  cncongr2  16714  prmdiveq  16833  odzdvds  16843  pythagtriplem2  16865  pcexp  16907  vdwlem13  17041  ramz  17073  prmolefac  17094  elrestr  17469  xpsff1o  17609  subsubc  17898  clatl  18552  frmdgsum  18909  sursubmefmnd  18943  injsubmefmnd  18944  smndex1mndlem  18959  dfgrp3e  19094  mulgneg2  19162  mulgnnass  19163  mhmmulg  19169  gsumwrev  19424  symgextf1lem  19478  symgfixelsi  19493  pmtrdifellem4  19537  sylow1lem1  19656  efgsfo  19797  efgred  19806  cyggexb  19957  gsumzres  19967  gsum2dlem2  20029  mulgass2  20380  rngimcnv  20526  funcrngcsetc  20713  funcrngcsetcALT  20714  rhmsscrnghm  20738  funcringcsetc  20747  lmodprop2d  21011  lspsnne2  21208  lspsneu  21213  cnfldmulg  21511  cnfldexp  21512  zrhpsgnelbas  21701  assapropd  21978  mplcoe1  22145  mplcoe3  22146  mplcoe5  22148  mhpvarcl  22268  ply1sclf1  22407  mat1scmat  22653  restopn2  23291  cnpf2  23364  cmpfi  23522  txcn  23740  txlm  23762  xkoptsub  23768  xkopjcn  23770  ufildr  24045  cnflf  24116  fclsnei  24133  fclscmp  24144  ufilcmp  24146  cnfcf  24156  symgtgp  24220  isxms2  24562  met2ndc  24637  metustbl  24680  tngngp2  24766  clmmulg  25217  iscau4  25395  ovolunlem1a  25612  ovolicc2lem4  25636  volfiniun  25663  voliunlem1  25666  volsup  25672  dvnadd  26045  dvnres  26047  dvcobr  26062  ply1nzb  26237  plypf1  26326  dgrle  26357  coeaddlem  26363  dgrlt  26380  dvntaylp  26488  cxpmul2  26808  rlimcnp  27084  facgam  27184  wilthlem2  27187  isnsqf  27253  musum  27309  chtub  27330  chpval2  27336  gausslemma2dlem0i  27482  dchrisumlem1  27607  qabvexp  27744  ostthlem2  27746  nodenselem8  27809  lesrec  27946  bday1  27961  sltsleft  28007  sltsright  28008  oncutlt  28411  noseqind  28439  dfnns2  28519  bdaypw2n0bnd  28611  axsegconlem1  29172  ax5seglem4  29187  ax5seglem5  29188  axlowdimlem15  29211  axcontlem2  29220  axcontlem4  29222  incistruhgr  29334  upgredg2vtx  29396  upgredgpr  29397  numedglnl  29399  uhgr2edg  29463  nbupgruvtxres  29662  cusgrfilem1  29710  wlkres  29923  wlkp1lem2  29927  pthdivtx  29981  pthdlem2lem  30021  wlkiswwlks2lem4  30126  wwlksnredwwlkn0  30150  wwlksnextwrd  30151  wwlksnfi  30160  wwlksnextprop  30166  clwlkclwwlklem2a  30254  clwlkclwwlkf1lem2  30261  erclwwlksym  30277  clwwlkf1  30305  eleclclwwlknlem2  30317  erclwwlknsym  30326  clwwlknonex2  30365  eupth2lem3lem6  30489  frgr3vlem1  30529  3vfriswmgrlem  30533  wlkl0  30623  sspval  30980  nmosetre  31021  nmobndseqi  31036  nmobndseqiALT  31037  orthcom  31365  shsva  31577  shmodsi  31646  h1datomi  31838  nmopsetretALT  32120  nmfnsetre  32134  lnopcnbd  32293  pjclem4  32456  pj3si  32464  ssmd1  32568  atom1d  32610  chjatom  32614  atcvat4i  32654  cdj3lem2a  32693  cdj3lem3a  32696  disjunsn  32845  unitdivcld  34203  xrge0iifiso  34237  dya2iocuni  34585  bnj168  35031  bnj535  35190  bnj590  35210  bnj594  35212  bnj938  35237  bnj1118  35284  bnj1128  35290  fnrelpredd  35392  deranglem  35524  subfacp1lem6  35543  subfacval2  35545  cvmlift2lem12  35672  satffun  35767  mrsubvrs  35880  msrrcl  35901  mclsax  35927  dfon2lem6  36144  rdgprc  36150  ifscgr  36402  btwncolinear1  36427  hfelhf  36539  opnrebl2  36689  nn0prpw  36691  ordcmp  36815  findreccl  36821  nndivlub  36826  axtcond  36846  dfttc2g  36874  mh-inf3f1  36909  bj-rest0  37590  bj-isrvec2  37799  topdifinffinlem  37848  iooelexlt  37863  rdgeqoa  37871  exrecfnlem  37880  wl-mo3t  38086  matunitlindflem2  38123  poimirlem2  38128  poimirlem23  38149  poimirlem28  38154  poimirlem29  38155  poimirlem31  38157  poimirlem32  38158  sdclem2  38248  sdclem1  38249  prdsbnd2  38301  ismtyval  38306  rrnequiv  38341  isexid2  38361  ismndo1  38379  exidreslem  38383  rngo2  38413  rngoueqz  38446  risci  38493  eldisjdmqsim  39323  prtlem11  39497  prtlem15  39506  cvrat4  40074  lcfl6  42131  dvdsexpnn0  42950  harval3  44121  clcnvlem  44206  cnvrcl0  44208  cnvtrcl0  44209  iunrelexpmin1  44291  iunrelexpmin2  44295  ormkglobd  47450  fcoresf1b  47663  aovmpt4g  47794  elsetpreimafvbi  47996  iccpartiltu  48027  iccpartgt  48032  iccpartgel  48034  reuopreuprim  48131  fmtnofac1  48178  gbepos  48379  grtrif1o  48563  grtriclwlk3  48566  isubgr3stgrlem4  48590  gpgprismgr4cycllem3  48718  pgnbgreunbgrlem1  48734  pgnbgreunbgrlem3  48739  pgnbgreunbgrlem4  48740  pgnbgreunbgrlem5lem1  48741  pgnbgreunbgrlem5lem2  48742  pgnbgreunbgrlem5lem3  48743  pgnbgreunbgrlem6  48745  pgnbgreunbgr  48746  ellcoellss  49067  dignn0flhalflem2  49248  nn0sumshdiglemB  49252  1arympt1  49270  opth1neg  49456  opth2neg  49457  oppccatb  49646  fullthinc  50080