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 ⊢ (𝜒 → (𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  syl5ibrcom  250  biimprd  251  exdistrf  2482  pm2.61ne  3046  spcimgft  3518  unineq  4244  elpreqprlem  4836  oteqex  5488  otel3xp  5712  eqrelrdv2  5786  breldmg  5904  elrnmpt1  5955  cnveqb  6200  cnveq0  6201  predpoirr  6341  predfrirr  6342  limelon  6433  f1ssf1  6860  ndmfv  6920  eqfnun  7039  ffvresb  7128  isomin  7346  isofrlem  7349  oprabidw  7454  caovord3d  7633  eldifpw  7776  ssonuni  7788  onsucuni2  7839  ordzsl  7850  tfindsg  7866  findsg  7903  oteqimp  8014  frxp  8131  poxp  8133  fnwelem  8136  tfrlem11  8384  ord1eln01  8490  ord2eln012  8491  oacl  8529  omcl  8530  oecl  8531  oa0r  8532  om0r  8533  om1r  8537  oe1m  8539  oaordi  8540  oawordri  8544  oaass  8555  oarec  8556  omwordri  8566  odi  8573  omass  8574  oewordri  8587  oeworde  8588  oeordsuc  8589  oelim2  8590  oeoa  8592  oeoelem  8593  oeoe  8594  nnm0r  8605  nnacl  8606  nnacom  8612  nnaordi  8613  nnaass  8617  nndi  8618  nnmass  8619  nnmsucr  8620  nnmcom  8621  omabs  8646  brecop  8817  eceqoveq  8829  elpm2r  8851  map0g  8891  undifixp  8941  fundmen  9038  mapxpen  9141  mapunen  9144  pssnn  9163  php  9201  unxpdomlem2  9227  f1vrnfibi  9309  elfir  9385  wemapso2lem  9524  wdompwdom  9550  inf3lem1  9607  inf3lem3  9609  cantnfval2  9648  cantnfp1lem3  9659  r1sdom  9756  r1tr  9758  carden2a  9971  fidomtri2  9999  prdom2  10009  infxpenlem  10016  acndom  10054  fodomacn  10059  wdomfil  10064  alephon  10072  alephordi  10077  alephle  10091  alephfplem3  10109  dfac2a  10132  kmlem9  10161  cflm  10251  cfslb  10268  cfslbn  10269  infpssrlem3  10307  infpssrlem4  10308  fin23lem21  10341  fin23lem30  10344  isf34lem7  10381  isf34lem6  10382  fin67  10397  isfin7-2  10398  fin1a2lem7  10408  fin1a2lem10  10411  iundom2g  10542  konigthlem  10571  alephreg  10585  gchdomtri  10632  wunr1om  10722  tskr1om  10770  inar1  10778  grur1a  10822  indpi  10910  genpprecl  11004  genpnmax  11010  addcmpblnr  11072  recexsrlem  11106  map2psrpr  11113  ax1rid  11164  axpre-mulgt0  11171  ltle  11316  nnmulcl  12275  nnsub  12298  nn0sub  12572  nneo  12698  uz11  12905  xrltle  13192  xltnegi  13260  xrsupsslem  13351  xrinfmsslem  13352  xrub  13356  supxrunb1  13363  supxrunb2  13364  om2uzuzi  14005  uzrdgxfr  14023  seqcl2  14076  seqfveq2  14080  seqshft2  14084  seqsplit  14091  seqcaopr3  14093  seqf1olem2a  14096  seqid2  14104  seqhomo  14105  ser1const  14114  m1expcl2  14141  expadd  14160  expmul  14163  faclbnd  14346  hashfzp1  14488  hashmap  14492  hashf1lem2  14513  hashf1  14514  seqcoll  14521  wrdsymb0  14606  len0nnbi  14608  eqs1  14672  swrdnd2  14717  wrd2ind  14784  pfxccatin12lem2c  14791  pfxccatin12lem2  14792  swrdccatin1d  14804  repswccat  14849  repswcshw  14875  cshwcshid  14890  rtrclreclem3  15123  rtrclreclem4  15124  dfrtrcl2  15125  relexpindlem  15126  relexpind  15127  rtrclind  15128  recan  15414  rexanre  15424  rlimcn3  15667  caurcvg2  15755  fsumiun  15899  efexp  16182  rpnnen2lem12  16306  dvdstr  16377  alzdvds  16403  zob  16442  sumeven  16470  sumodd  16471  bitsinv1  16525  smu01lem  16568  smupval  16571  smueqlem  16573  smumullem  16575  seq1st  16654  lcmfunsnlem2lem1  16721  lcmfunsnlem2lem2  16722  cncongr2  16751  prmdiveq  16870  odzdvds  16880  pythagtriplem2  16902  pcexp  16944  vdwlem13  17078  ramz  17110  prmolefac  17131  elrestr  17506  xpsff1o  17646  subsubc  17935  clatl  18589  frmdgsum  18952  sursubmefmnd  18986  injsubmefmnd  18987  smndex1mndlem  19002  dfgrp3e  19137  mulgneg2  19205  mulgnnass  19206  mhmmulg  19212  gsumwrev  19467  symgextf1lem  19521  symgfixelsi  19536  pmtrdifellem4  19580  sylow1lem1  19699  efgsfo  19840  efgred  19849  cyggexb  20000  gsumzres  20010  gsum2dlem2  20072  mulgass2  20425  rngimcnv  20571  funcrngcsetc  20776  funcrngcsetcALT  20777  rhmsscrnghm  20801  funcringcsetc  20810  lmodprop2d  21082  lspsnne2  21279  lspsneu  21284  cnfldmulg  21591  cnfldexp  21592  zrhpsgnelbas  21781  assapropd  22058  mplcoe1  22225  mplcoe3  22226  mplcoe5  22228  mhpvarcl  22348  ply1sclf1  22487  mat1scmat  22733  restopn2  23371  cnpf2  23444  cmpfi  23602  txcn  23820  txlm  23842  xkoptsub  23848  xkopjcn  23850  ufildr  24125  cnflf  24196  fclsnei  24213  fclscmp  24224  ufilcmp  24226  cnfcf  24236  symgtgp  24300  isxms2  24642  met2ndc  24717  metustbl  24760  tngngp2  24846  clmmulg  25297  iscau4  25475  ovolunlem1a  25692  ovolicc2lem4  25716  volfiniun  25743  voliunlem1  25746  volsup  25752  dvnadd  26125  dvnres  26127  dvcobr  26142  ply1nzb  26317  plypf1  26406  dgrle  26437  coeaddlem  26443  dgrlt  26460  dvntaylp  26571  cxpmul2  26891  rlimcnp  27167  facgam  27267  wilthlem2  27270  isnsqf  27336  musum  27392  chtub  27413  chpval2  27419  gausslemma2dlem0i  27565  dchrisumlem1  27690  qabvexp  27827  ostthlem2  27829  nodenselem8  27892  lesrec  28029  bday1  28044  sltsleft  28090  sltsright  28091  oncutlt  28494  noseqind  28522  dfnns2  28602  bdaypw2n0bnd  28694  axsegconlem1  29304  ax5seglem4  29319  ax5seglem5  29320  axlowdimlem15  29343  axcontlem2  29352  axcontlem4  29354  incistruhgr  29466  upgredg2vtx  29528  upgredgpr  29529  numedglnl  29531  uhgr2edg  29595  nbupgruvtxres  29794  cusgrfilem1  29842  wlkres  30055  wlkp1lem2  30059  pthdivtx  30113  pthdlem2lem  30153  wlkiswwlks2lem4  30258  wwlksnredwwlkn0  30282  wwlksnextwrd  30283  wwlksnfi  30292  wwlksnextprop  30298  clwlkclwwlklem2a  30386  clwlkclwwlkf1lem2  30393  erclwwlksym  30409  clwwlkf1  30437  eleclclwwlknlem2  30449  erclwwlknsym  30458  clwwlknonex2  30497  eupth2lem3lem6  30621  frgr3vlem1  30661  3vfriswmgrlem  30665  wlkl0  30755  sspval  31112  nmosetre  31153  nmobndseqi  31168  nmobndseqiALT  31169  orthcom  31497  shsva  31709  shmodsi  31778  h1datomi  31970  nmopsetretALT  32252  nmfnsetre  32266  lnopcnbd  32425  pjclem4  32588  pj3si  32596  ssmd1  32700  atom1d  32742  chjatom  32746  atcvat4i  32786  cdj3lem2a  32825  cdj3lem3a  32828  disjunsn  32976  unitdivcld  34322  xrge0iifiso  34356  dya2iocuni  34705  bnj168  35151  bnj535  35310  bnj590  35330  bnj594  35332  bnj938  35357  bnj1118  35404  bnj1128  35410  fnrelpredd  35507  acnum  35549  deranglem  35679  subfacp1lem6  35698  subfacval2  35700  cvmlift2lem12  35827  satffun  35922  mrsubvrs  36035  msrrcl  36056  mclsax  36082  dfon2lem6  36299  rdgprc  36305  ifscgr  36557  btwncolinear1  36582  hfelhf  36694  opnrebl2  36873  nn0prpw  36875  ordcmp  36999  findreccl  37005  nndivlub  37010  axtcond  37030  dfttc2g  37058  mh-inf3f1  37093  bj-rest0  37776  bj-isrvec2  37985  topdifinffinlem  38034  iooelexlt  38049  rdgeqoa  38057  exrecfnlem  38066  wl-mo3t  38272  matunitlindflem2  38309  poimirlem2  38314  poimirlem23  38335  poimirlem28  38340  poimirlem29  38341  poimirlem31  38343  poimirlem32  38344  sdclem2  38434  sdclem1  38435  prdsbnd2  38487  ismtyval  38492  rrnequiv  38527  isexid2  38547  ismndo1  38565  exidreslem  38569  rngo2  38599  rngoueqz  38632  risci  38679  eldisjdmqsim  39507  prtlem11  39681  prtlem15  39690  cvrat4  40258  lcfl6  42315  dvdsexpnn0  43136  harval3  44305  clcnvlem  44390  cnvrcl0  44392  cnvtrcl0  44393  iunrelexpmin1  44475  iunrelexpmin2  44479  ormkglobd  47632  fcoresf1b  47848  aovmpt4g  47979  elsetpreimafvbi  48181  iccpartiltu  48212  iccpartgt  48217  iccpartgel  48219  reuopreuprim  48316  fmtnofac1  48363  gbepos  48564  grtrif1o  48748  grtriclwlk3  48751  isubgr3stgrlem4  48775  gpgprismgr4cycllem3  48903  pgnbgreunbgrlem1  48919  pgnbgreunbgrlem3  48924  pgnbgreunbgrlem4  48925  pgnbgreunbgrlem5lem1  48926  pgnbgreunbgrlem5lem2  48927  pgnbgreunbgrlem5lem3  48928  pgnbgreunbgrlem6  48930  pgnbgreunbgr  48931  ellcoellss  49256  dignn0flhalflem2  49437  nn0sumshdiglemB  49441  1arympt1  49459  opth1neg  49645  opth2neg  49646  oppccatb  49835  fullthinc  50269