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  2445  pm2.61ne  3010  spcimgft  3503  unineq  4241  elpreqprlem  4820  oteqex  5447  otel3xp  5669  eqrelrdv2  5742  breldmg  5856  elrnmpt1  5906  cnveqb  6149  cnveq0  6150  predpoirr  6285  predfrirr  6286  limelon  6376  f1ssf1  6800  ndmfv  6859  eqfnun  6975  ffvresb  7063  isomin  7278  isofrlem  7281  oprabidw  7384  caovord3d  7563  eldifpw  7708  ssonuni  7720  onsucuni2  7773  ordzsl  7785  tfindsg  7801  findsg  7837  oteqimp  7950  frxp  8066  poxp  8068  fnwelem  8071  tfrlem11  8317  ord1eln01  8421  ord2eln012  8422  oacl  8460  omcl  8461  oecl  8462  oa0r  8463  om0r  8464  om1r  8468  oe1m  8470  oaordi  8471  oawordri  8475  oaass  8486  oarec  8487  omwordri  8497  odi  8504  omass  8505  oewordri  8517  oeworde  8518  oeordsuc  8519  oelim2  8520  oeoa  8522  oeoelem  8523  oeoe  8524  nnm0r  8535  nnacl  8536  nnacom  8542  nnaordi  8543  nnaass  8547  nndi  8548  nnmass  8549  nnmsucr  8550  nnmcom  8551  omabs  8576  brecop  8744  eceqoveq  8756  elpm2r  8779  map0g  8818  undifixp  8868  fundmen  8963  mapxpen  9067  mapunen  9070  pssnn  9092  php  9131  unxpdomlem2  9156  f1vrnfibi  9251  elfir  9324  wemapso2lem  9463  wdompwdom  9489  inf3lem1  9543  inf3lem3  9545  cantnfval2  9584  cantnfp1lem3  9595  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  10481  alephreg  10495  gchdomtri  10542  wunr1om  10632  tskr1om  10680  inar1  10688  grur1a  10732  indpi  10820  genpprecl  10914  genpnmax  10920  addcmpblnr  10982  recexsrlem  11016  map2psrpr  11023  ax1rid  11074  axpre-mulgt0  11081  ltle  11222  nnmulcl  12170  nnsub  12190  nn0sub  12452  nneo  12578  uz11  12778  xrltle  13069  xltnegi  13136  xrsupsslem  13227  xrinfmsslem  13228  xrub  13232  supxrunb1  13239  supxrunb2  13240  om2uzuzi  13874  uzrdgxfr  13892  seqcl2  13945  seqfveq2  13949  seqshft2  13953  seqsplit  13960  seqcaopr3  13962  seqf1olem2a  13965  seqid2  13973  seqhomo  13974  ser1const  13983  m1expcl2  14010  expadd  14029  expmul  14032  faclbnd  14215  hashfzp1  14356  hashmap  14360  hashf1lem2  14381  hashf1  14382  seqcoll  14389  wrdsymb0  14474  len0nnbi  14476  eqs1  14537  swrdnd2  14580  wrd2ind  14647  pfxccatin12lem2c  14654  pfxccatin12lem2  14655  swrdccatin1d  14667  repswccat  14710  repswcshw  14736  cshwcshid  14752  rtrclreclem3  14985  rtrclreclem4  14986  dfrtrcl2  14987  relexpindlem  14988  relexpind  14989  rtrclind  14990  recan  15262  rexanre  15272  rlimcn3  15515  caurcvg2  15603  fsumiun  15746  efexp  16028  rpnnen2lem12  16152  dvdstr  16223  alzdvds  16249  zob  16288  sumeven  16316  sumodd  16317  bitsinv1  16371  smu01lem  16414  smupval  16417  smueqlem  16419  smumullem  16421  seq1st  16500  lcmfunsnlem2lem1  16567  lcmfunsnlem2lem2  16568  cncongr2  16597  prmdiveq  16715  odzdvds  16725  pythagtriplem2  16747  pcexp  16789  vdwlem13  16923  ramz  16955  prmolefac  16976  elrestr  17350  xpsff1o  17489  subsubc  17778  clatl  18432  frmdgsum  18754  sursubmefmnd  18788  injsubmefmnd  18789  smndex1mndlem  18801  dfgrp3e  18937  mulgneg2  19005  mulgnnass  19006  mhmmulg  19012  gsumwrev  19263  symgextf1lem  19317  symgfixelsi  19332  pmtrdifellem4  19376  sylow1lem1  19495  efgsfo  19636  efgred  19645  cyggexb  19796  gsumzres  19806  gsum2dlem2  19868  mulgass2  20212  rngimcnv  20359  funcrngcsetc  20543  funcrngcsetcALT  20544  rhmsscrnghm  20568  funcringcsetc  20577  lmodprop2d  20845  lspsnne2  21043  lspsneu  21048  cnfldmulg  21328  cnfldexp  21329  zrhpsgnelbas  21519  assapropd  21797  mplcoe1  21960  mplcoe3  21961  mplcoe5  21963  mhpvarcl  22051  ply1sclf1  22191  mat1scmat  22442  restopn2  23080  cnpf2  23153  cmpfi  23311  txcn  23529  txlm  23551  xkoptsub  23557  xkopjcn  23559  ufildr  23834  cnflf  23905  fclsnei  23922  fclscmp  23933  ufilcmp  23935  cnfcf  23945  symgtgp  24009  isxms2  24352  met2ndc  24427  metustbl  24470  tngngp2  24556  clmmulg  25017  iscau4  25195  ovolunlem1a  25413  ovolicc2lem4  25437  volfiniun  25464  voliunlem1  25467  volsup  25473  dvnadd  25847  dvnres  25849  dvcobr  25865  dvcobrOLD  25866  ply1nzb  26044  plypf1  26133  dgrle  26164  coeaddlem  26170  dgrlt  26188  dvntaylp  26295  cxpmul2  26614  rlimcnp  26891  facgam  26992  wilthlem2  26995  isnsqf  27061  musum  27117  chtub  27139  chpval2  27145  gausslemma2dlem0i  27291  dchrisumlem1  27416  qabvexp  27553  ostthlem2  27555  nodenselem8  27619  slerec  27748  bday1s  27763  ssltleft  27802  ssltright  27803  onscutlt  28188  noseqind  28209  dfnns2  28284  axsegconlem1  28880  ax5seglem4  28895  ax5seglem5  28896  axlowdimlem15  28919  axcontlem2  28928  axcontlem4  28930  incistruhgr  29042  upgredg2vtx  29104  upgredgpr  29105  numedglnl  29107  uhgr2edg  29171  nbupgruvtxres  29370  cusgrfilem1  29419  wlkres  29632  wlkp1lem2  29636  pthdivtx  29690  pthdlem2lem  29730  wlkiswwlks2lem4  29835  wwlksnredwwlkn0  29859  wwlksnextwrd  29860  wwlksnfi  29869  wwlksnextprop  29875  clwlkclwwlklem2a  29960  clwlkclwwlkf1lem2  29967  erclwwlksym  29983  clwwlkf1  30011  eleclclwwlknlem2  30023  erclwwlknsym  30032  clwwlknonex2  30071  eupth2lem3lem6  30195  frgr3vlem1  30235  3vfriswmgrlem  30239  wlkl0  30329  sspval  30685  nmosetre  30726  nmobndseqi  30741  nmobndseqiALT  30742  orthcom  31070  shsva  31282  shmodsi  31351  h1datomi  31543  nmopsetretALT  31825  nmfnsetre  31839  lnopcnbd  31998  pjclem4  32161  pj3si  32169  ssmd1  32273  atom1d  32315  chjatom  32319  atcvat4i  32359  cdj3lem2a  32398  cdj3lem3a  32401  disjunsn  32556  unitdivcld  33867  xrge0iifiso  33901  dya2iocuni  34250  bnj168  34696  bnj535  34856  bnj590  34876  bnj594  34878  bnj938  34903  bnj1118  34950  bnj1128  34956  fnrelpredd  35055  deranglem  35138  subfacp1lem6  35157  subfacval2  35159  cvmlift2lem12  35286  satffun  35381  mrsubvrs  35494  msrrcl  35515  mclsax  35541  dfon2lem6  35761  rdgprc  35767  ifscgr  36017  btwncolinear1  36042  hfelhf  36154  opnrebl2  36294  nn0prpw  36296  ordcmp  36420  findreccl  36426  nndivlub  36431  bj-rest0  37066  bj-isrvec2  37273  topdifinffinlem  37320  iooelexlt  37335  rdgeqoa  37343  exrecfnlem  37352  wl-mo3t  37549  matunitlindflem2  37596  poimirlem2  37601  poimirlem23  37622  poimirlem28  37627  poimirlem29  37628  poimirlem31  37630  poimirlem32  37631  sdclem2  37721  sdclem1  37722  prdsbnd2  37774  ismtyval  37779  rrnequiv  37814  isexid2  37834  ismndo1  37852  exidreslem  37856  rngo2  37886  rngoueqz  37919  risci  37966  prtlem11  38844  prtlem15  38853  cvrat4  39422  lcfl6  41479  dvdsexpnn0  42307  harval3  43511  clcnvlem  43596  cnvrcl0  43598  cnvtrcl0  43599  iunrelexpmin1  43681  iunrelexpmin2  43685  ormkglobd  46857  tworepnotupword  46868  fcoresf1b  47055  aovmpt4g  47186  elsetpreimafvbi  47376  iccpartiltu  47407  iccpartgt  47412  iccpartgel  47414  reuopreuprim  47511  fmtnofac1  47555  gbepos  47743  grtrif1o  47927  grtriclwlk3  47930  isubgr3stgrlem4  47954  gpgprismgr4cycllem3  48082  pgnbgreunbgrlem1  48098  pgnbgreunbgrlem3  48103  pgnbgreunbgrlem4  48104  pgnbgreunbgrlem5lem1  48105  pgnbgreunbgrlem5lem2  48106  pgnbgreunbgrlem5lem3  48107  pgnbgreunbgrlem6  48109  pgnbgreunbgr  48110  ellcoellss  48421  dignn0flhalflem2  48602  nn0sumshdiglemB  48606  1arympt1  48624  opth1neg  48811  opth2neg  48812  oppccatb  49002  fullthinc  49436