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  3505  unineq  4242  elpreqprlem  4824  oteqex  5456  otel3xp  5678  eqrelrdv2  5752  breldmg  5866  elrnmpt1  5917  cnveqb  6162  cnveq0  6163  predpoirr  6299  predfrirr  6300  limelon  6390  f1ssf1  6814  ndmfv  6874  eqfnun  6991  ffvresb  7080  isomin  7293  isofrlem  7296  oprabidw  7399  caovord3d  7578  eldifpw  7723  ssonuni  7735  onsucuni2  7786  ordzsl  7797  tfindsg  7813  findsg  7849  oteqimp  7962  frxp  8078  poxp  8080  fnwelem  8083  tfrlem11  8329  ord1eln01  8433  ord2eln012  8434  oacl  8472  omcl  8473  oecl  8474  oa0r  8475  om0r  8476  om1r  8480  oe1m  8482  oaordi  8483  oawordri  8487  oaass  8498  oarec  8499  omwordri  8509  odi  8516  omass  8517  oewordri  8530  oeworde  8531  oeordsuc  8532  oelim2  8533  oeoa  8535  oeoelem  8536  oeoe  8537  nnm0r  8548  nnacl  8549  nnacom  8555  nnaordi  8556  nnaass  8560  nndi  8561  nnmass  8562  nnmsucr  8563  nnmcom  8564  omabs  8589  brecop  8759  eceqoveq  8771  elpm2r  8794  map0g  8834  undifixp  8884  fundmen  8980  mapxpen  9083  mapunen  9086  pssnn  9105  php  9143  unxpdomlem2  9169  f1vrnfibi  9254  elfir  9330  wemapso2lem  9469  wdompwdom  9495  inf3lem1  9549  inf3lem3  9551  cantnfval2  9590  cantnfp1lem3  9601  r1sdom  9698  r1tr  9700  carden2a  9890  fidomtri2  9918  prdom2  9928  infxpenlem  9935  acndom  9973  fodomacn  9978  wdomfil  9983  alephon  9991  alephordi  9996  alephle  10010  alephfplem3  10028  dfac2a  10052  kmlem9  10081  cflm  10172  cfslb  10188  cfslbn  10189  infpssrlem3  10227  infpssrlem4  10228  fin23lem21  10261  fin23lem30  10264  isf34lem7  10301  isf34lem6  10302  fin67  10317  isfin7-2  10318  fin1a2lem7  10328  fin1a2lem10  10331  iundom2g  10462  konigthlem  10491  alephreg  10505  gchdomtri  10552  wunr1om  10642  tskr1om  10690  inar1  10698  grur1a  10742  indpi  10830  genpprecl  10924  genpnmax  10930  addcmpblnr  10992  recexsrlem  11026  map2psrpr  11033  ax1rid  11084  axpre-mulgt0  11091  ltle  11233  nnmulcl  12181  nnsub  12201  nn0sub  12463  nneo  12588  uz11  12788  xrltle  13075  xltnegi  13143  xrsupsslem  13234  xrinfmsslem  13235  xrub  13239  supxrunb1  13246  supxrunb2  13247  om2uzuzi  13884  uzrdgxfr  13902  seqcl2  13955  seqfveq2  13959  seqshft2  13963  seqsplit  13970  seqcaopr3  13972  seqf1olem2a  13975  seqid2  13983  seqhomo  13984  ser1const  13993  m1expcl2  14020  expadd  14039  expmul  14042  faclbnd  14225  hashfzp1  14366  hashmap  14370  hashf1lem2  14391  hashf1  14392  seqcoll  14399  wrdsymb0  14484  len0nnbi  14486  eqs1  14548  swrdnd2  14591  wrd2ind  14658  pfxccatin12lem2c  14665  pfxccatin12lem2  14666  swrdccatin1d  14678  repswccat  14721  repswcshw  14747  cshwcshid  14762  rtrclreclem3  14995  rtrclreclem4  14996  dfrtrcl2  14997  relexpindlem  14998  relexpind  14999  rtrclind  15000  recan  15272  rexanre  15282  rlimcn3  15525  caurcvg2  15613  fsumiun  15756  efexp  16038  rpnnen2lem12  16162  dvdstr  16233  alzdvds  16259  zob  16298  sumeven  16326  sumodd  16327  bitsinv1  16381  smu01lem  16424  smupval  16427  smueqlem  16429  smumullem  16431  seq1st  16510  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  cncongr2  16607  prmdiveq  16725  odzdvds  16735  pythagtriplem2  16757  pcexp  16799  vdwlem13  16933  ramz  16965  prmolefac  16986  elrestr  17360  xpsff1o  17500  subsubc  17789  clatl  18443  frmdgsum  18799  sursubmefmnd  18833  injsubmefmnd  18834  smndex1mndlem  18846  dfgrp3e  18982  mulgneg2  19050  mulgnnass  19051  mhmmulg  19057  gsumwrev  19307  symgextf1lem  19361  symgfixelsi  19376  pmtrdifellem4  19420  sylow1lem1  19539  efgsfo  19680  efgred  19689  cyggexb  19840  gsumzres  19850  gsum2dlem2  19912  mulgass2  20256  rngimcnv  20404  funcrngcsetc  20585  funcrngcsetcALT  20586  rhmsscrnghm  20610  funcringcsetc  20619  lmodprop2d  20887  lspsnne2  21085  lspsneu  21090  cnfldmulg  21370  cnfldexp  21371  zrhpsgnelbas  21561  assapropd  21839  mplcoe1  22004  mplcoe3  22005  mplcoe5  22007  mhpvarcl  22103  ply1sclf1  22243  mat1scmat  22495  restopn2  23133  cnpf2  23206  cmpfi  23364  txcn  23582  txlm  23604  xkoptsub  23610  xkopjcn  23612  ufildr  23887  cnflf  23958  fclsnei  23975  fclscmp  23986  ufilcmp  23988  cnfcf  23998  symgtgp  24062  isxms2  24404  met2ndc  24479  metustbl  24522  tngngp2  24608  clmmulg  25069  iscau4  25247  ovolunlem1a  25465  ovolicc2lem4  25489  volfiniun  25516  voliunlem1  25519  volsup  25525  dvnadd  25899  dvnres  25901  dvcobr  25917  dvcobrOLD  25918  ply1nzb  26096  plypf1  26185  dgrle  26216  coeaddlem  26222  dgrlt  26240  dvntaylp  26347  cxpmul2  26666  rlimcnp  26943  facgam  27044  wilthlem2  27047  isnsqf  27113  musum  27169  chtub  27191  chpval2  27197  gausslemma2dlem0i  27343  dchrisumlem1  27468  qabvexp  27605  ostthlem2  27607  nodenselem8  27671  lesrec  27807  bday1  27822  sltsleft  27868  sltsright  27869  oncutlt  28272  noseqind  28300  dfnns2  28380  bdaypw2n0bnd  28472  axsegconlem1  29002  ax5seglem4  29017  ax5seglem5  29018  axlowdimlem15  29041  axcontlem2  29050  axcontlem4  29052  incistruhgr  29164  upgredg2vtx  29226  upgredgpr  29227  numedglnl  29229  uhgr2edg  29293  nbupgruvtxres  29492  cusgrfilem1  29541  wlkres  29754  wlkp1lem2  29758  pthdivtx  29812  pthdlem2lem  29852  wlkiswwlks2lem4  29957  wwlksnredwwlkn0  29981  wwlksnextwrd  29982  wwlksnfi  29991  wwlksnextprop  29997  clwlkclwwlklem2a  30085  clwlkclwwlkf1lem2  30092  erclwwlksym  30108  clwwlkf1  30136  eleclclwwlknlem2  30148  erclwwlknsym  30157  clwwlknonex2  30196  eupth2lem3lem6  30320  frgr3vlem1  30360  3vfriswmgrlem  30364  wlkl0  30454  sspval  30810  nmosetre  30851  nmobndseqi  30866  nmobndseqiALT  30867  orthcom  31195  shsva  31407  shmodsi  31476  h1datomi  31668  nmopsetretALT  31950  nmfnsetre  31964  lnopcnbd  32123  pjclem4  32286  pj3si  32294  ssmd1  32398  atom1d  32440  chjatom  32444  atcvat4i  32484  cdj3lem2a  32523  cdj3lem3a  32526  disjunsn  32680  unitdivcld  34078  xrge0iifiso  34112  dya2iocuni  34460  bnj168  34906  bnj535  35065  bnj590  35085  bnj594  35087  bnj938  35112  bnj1118  35159  bnj1128  35165  fnrelpredd  35266  deranglem  35379  subfacp1lem6  35398  subfacval2  35400  cvmlift2lem12  35527  satffun  35622  mrsubvrs  35735  msrrcl  35756  mclsax  35782  dfon2lem6  35999  rdgprc  36005  ifscgr  36257  btwncolinear1  36282  hfelhf  36394  opnrebl2  36534  nn0prpw  36536  ordcmp  36660  findreccl  36666  nndivlub  36671  bj-rest0  37340  bj-isrvec2  37549  topdifinffinlem  37596  iooelexlt  37611  rdgeqoa  37619  exrecfnlem  37628  wl-mo3t  37825  matunitlindflem2  37862  poimirlem2  37867  poimirlem23  37888  poimirlem28  37893  poimirlem29  37894  poimirlem31  37896  poimirlem32  37897  sdclem2  37987  sdclem1  37988  prdsbnd2  38040  ismtyval  38045  rrnequiv  38080  isexid2  38100  ismndo1  38118  exidreslem  38122  rngo2  38152  rngoueqz  38185  risci  38232  eldisjdmqsim  39062  prtlem11  39236  prtlem15  39245  cvrat4  39813  lcfl6  41870  dvdsexpnn0  42698  harval3  43888  clcnvlem  43973  cnvrcl0  43975  cnvtrcl0  43976  iunrelexpmin1  44058  iunrelexpmin2  44062  ormkglobd  47227  fcoresf1b  47424  aovmpt4g  47555  elsetpreimafvbi  47745  iccpartiltu  47776  iccpartgt  47781  iccpartgel  47783  reuopreuprim  47880  fmtnofac1  47924  gbepos  48112  grtrif1o  48296  grtriclwlk3  48299  isubgr3stgrlem4  48323  gpgprismgr4cycllem3  48451  pgnbgreunbgrlem1  48467  pgnbgreunbgrlem3  48472  pgnbgreunbgrlem4  48473  pgnbgreunbgrlem5lem1  48474  pgnbgreunbgrlem5lem2  48475  pgnbgreunbgrlem5lem3  48476  pgnbgreunbgrlem6  48478  pgnbgreunbgr  48479  ellcoellss  48789  dignn0flhalflem2  48970  nn0sumshdiglemB  48974  1arympt1  48992  opth1neg  49179  opth2neg  49180  oppccatb  49369  fullthinc  49803