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  2479  pm2.61ne  3043  spcimgft  3515  unineq  4242  elpreqprlem  4832  oteqex  5485  otel3xp  5709  eqrelrdv2  5783  breldmg  5901  elrnmpt1  5952  cnveqb  6197  cnveq0  6198  predpoirr  6336  predfrirr  6337  limelon  6428  f1ssf1  6855  ndmfv  6915  eqfnun  7034  ffvresb  7123  isomin  7337  isofrlem  7340  oprabidw  7443  caovord3d  7622  eldifpw  7768  ssonuni  7780  onsucuni2  7831  ordzsl  7842  tfindsg  7858  findsg  7895  oteqimp  8006  frxp  8123  poxp  8125  fnwelem  8128  tfrlem11  8376  ord1eln01  8482  ord2eln012  8483  oacl  8521  omcl  8522  oecl  8523  oa0r  8524  om0r  8525  om1r  8529  oe1m  8531  oaordi  8532  oawordri  8536  oaass  8547  oarec  8548  omwordri  8558  odi  8565  omass  8566  oewordri  8579  oeworde  8580  oeordsuc  8581  oelim2  8582  oeoa  8584  oeoelem  8585  oeoe  8586  nnm0r  8597  nnacl  8598  nnacom  8604  nnaordi  8605  nnaass  8609  nndi  8610  nnmass  8611  nnmsucr  8612  nnmcom  8613  omabs  8638  brecop  8809  eceqoveq  8821  elpm2r  8843  map0g  8883  undifixp  8933  fundmen  9029  mapxpen  9132  mapunen  9135  pssnn  9154  php  9192  unxpdomlem2  9218  f1vrnfibi  9300  elfir  9376  wemapso2lem  9515  wdompwdom  9541  inf3lem1  9598  inf3lem3  9600  cantnfval2  9639  cantnfp1lem3  9650  r1sdom  9747  r1tr  9749  carden2a  9953  fidomtri2  9981  prdom2  9991  infxpenlem  9998  acndom  10036  fodomacn  10041  wdomfil  10046  alephon  10054  alephordi  10059  alephle  10073  alephfplem3  10091  dfac2a  10114  kmlem9  10143  cflm  10234  cfslb  10251  cfslbn  10252  infpssrlem3  10290  infpssrlem4  10291  fin23lem21  10324  fin23lem30  10327  isf34lem7  10364  isf34lem6  10365  fin67  10380  isfin7-2  10381  fin1a2lem7  10391  fin1a2lem10  10394  iundom2g  10525  konigthlem  10554  alephreg  10568  gchdomtri  10615  wunr1om  10705  tskr1om  10753  inar1  10761  grur1a  10805  indpi  10893  genpprecl  10987  genpnmax  10993  addcmpblnr  11055  recexsrlem  11089  map2psrpr  11096  ax1rid  11147  axpre-mulgt0  11154  ltle  11299  nnmulcl  12258  nnsub  12281  nn0sub  12555  nneo  12681  uz11  12888  xrltle  13175  xltnegi  13243  xrsupsslem  13334  xrinfmsslem  13335  xrub  13339  supxrunb1  13346  supxrunb2  13347  om2uzuzi  13987  uzrdgxfr  14005  seqcl2  14058  seqfveq2  14062  seqshft2  14066  seqsplit  14073  seqcaopr3  14075  seqf1olem2a  14078  seqid2  14086  seqhomo  14087  ser1const  14096  m1expcl2  14123  expadd  14142  expmul  14145  faclbnd  14328  hashfzp1  14470  hashmap  14474  hashf1lem2  14495  hashf1  14496  seqcoll  14503  wrdsymb0  14588  len0nnbi  14590  eqs1  14652  swrdnd2  14695  wrd2ind  14762  pfxccatin12lem2c  14769  pfxccatin12lem2  14770  swrdccatin1d  14782  repswccat  14825  repswcshw  14851  cshwcshid  14866  rtrclreclem3  15099  rtrclreclem4  15100  dfrtrcl2  15101  relexpindlem  15102  relexpind  15103  rtrclind  15104  recan  15390  rexanre  15400  rlimcn3  15643  caurcvg2  15731  fsumiun  15875  efexp  16158  rpnnen2lem12  16282  dvdstr  16353  alzdvds  16379  zob  16418  sumeven  16446  sumodd  16447  bitsinv1  16501  smu01lem  16544  smupval  16547  smueqlem  16549  smumullem  16551  seq1st  16630  lcmfunsnlem2lem1  16697  lcmfunsnlem2lem2  16698  cncongr2  16727  prmdiveq  16846  odzdvds  16856  pythagtriplem2  16878  pcexp  16920  vdwlem13  17054  ramz  17086  prmolefac  17107  elrestr  17482  xpsff1o  17622  subsubc  17911  clatl  18565  frmdgsum  18922  sursubmefmnd  18956  injsubmefmnd  18957  smndex1mndlem  18972  dfgrp3e  19107  mulgneg2  19175  mulgnnass  19176  mhmmulg  19182  gsumwrev  19437  symgextf1lem  19491  symgfixelsi  19506  pmtrdifellem4  19550  sylow1lem1  19669  efgsfo  19810  efgred  19819  cyggexb  19970  gsumzres  19980  gsum2dlem2  20042  mulgass2  20393  rngimcnv  20539  funcrngcsetc  20726  funcrngcsetcALT  20727  rhmsscrnghm  20751  funcringcsetc  20760  lmodprop2d  21026  lspsnne2  21223  lspsneu  21228  cnfldmulg  21535  cnfldexp  21536  zrhpsgnelbas  21725  assapropd  22002  mplcoe1  22169  mplcoe3  22170  mplcoe5  22172  mhpvarcl  22292  ply1sclf1  22431  mat1scmat  22677  restopn2  23315  cnpf2  23388  cmpfi  23546  txcn  23764  txlm  23786  xkoptsub  23792  xkopjcn  23794  ufildr  24069  cnflf  24140  fclsnei  24157  fclscmp  24168  ufilcmp  24170  cnfcf  24180  symgtgp  24244  isxms2  24586  met2ndc  24661  metustbl  24704  tngngp2  24790  clmmulg  25241  iscau4  25419  ovolunlem1a  25636  ovolicc2lem4  25660  volfiniun  25687  voliunlem1  25690  volsup  25696  dvnadd  26069  dvnres  26071  dvcobr  26086  ply1nzb  26261  plypf1  26350  dgrle  26381  coeaddlem  26387  dgrlt  26404  dvntaylp  26515  cxpmul2  26835  rlimcnp  27111  facgam  27211  wilthlem2  27214  isnsqf  27280  musum  27336  chtub  27357  chpval2  27363  gausslemma2dlem0i  27509  dchrisumlem1  27634  qabvexp  27771  ostthlem2  27773  nodenselem8  27836  lesrec  27973  bday1  27988  sltsleft  28034  sltsright  28035  oncutlt  28438  noseqind  28466  dfnns2  28546  bdaypw2n0bnd  28638  axsegconlem1  29248  ax5seglem4  29263  ax5seglem5  29264  axlowdimlem15  29287  axcontlem2  29296  axcontlem4  29298  incistruhgr  29410  upgredg2vtx  29472  upgredgpr  29473  numedglnl  29475  uhgr2edg  29539  nbupgruvtxres  29738  cusgrfilem1  29786  wlkres  29999  wlkp1lem2  30003  pthdivtx  30057  pthdlem2lem  30097  wlkiswwlks2lem4  30202  wwlksnredwwlkn0  30226  wwlksnextwrd  30227  wwlksnfi  30236  wwlksnextprop  30242  clwlkclwwlklem2a  30330  clwlkclwwlkf1lem2  30337  erclwwlksym  30353  clwwlkf1  30381  eleclclwwlknlem2  30393  erclwwlknsym  30402  clwwlknonex2  30441  eupth2lem3lem6  30565  frgr3vlem1  30605  3vfriswmgrlem  30609  wlkl0  30699  sspval  31056  nmosetre  31097  nmobndseqi  31112  nmobndseqiALT  31113  orthcom  31441  shsva  31653  shmodsi  31722  h1datomi  31914  nmopsetretALT  32196  nmfnsetre  32210  lnopcnbd  32369  pjclem4  32532  pj3si  32540  ssmd1  32644  atom1d  32686  chjatom  32690  atcvat4i  32730  cdj3lem2a  32769  cdj3lem3a  32772  disjunsn  32920  unitdivcld  34272  xrge0iifiso  34306  dya2iocuni  34654  bnj168  35100  bnj535  35259  bnj590  35279  bnj594  35281  bnj938  35306  bnj1118  35353  bnj1128  35359  fnrelpredd  35463  acnum  35506  deranglem  35639  subfacp1lem6  35658  subfacval2  35660  cvmlift2lem12  35787  satffun  35882  mrsubvrs  35995  msrrcl  36016  mclsax  36042  dfon2lem6  36259  rdgprc  36265  ifscgr  36517  btwncolinear1  36542  hfelhf  36654  opnrebl2  36813  nn0prpw  36815  ordcmp  36939  findreccl  36945  nndivlub  36950  axtcond  36970  dfttc2g  36998  mh-inf3f1  37033  bj-rest0  37716  bj-isrvec2  37925  topdifinffinlem  37974  iooelexlt  37989  rdgeqoa  37997  exrecfnlem  38006  wl-mo3t  38212  matunitlindflem2  38249  poimirlem2  38254  poimirlem23  38275  poimirlem28  38280  poimirlem29  38281  poimirlem31  38283  poimirlem32  38284  sdclem2  38374  sdclem1  38375  prdsbnd2  38427  ismtyval  38432  rrnequiv  38467  isexid2  38487  ismndo1  38505  exidreslem  38509  rngo2  38539  rngoueqz  38572  risci  38619  eldisjdmqsim  39447  prtlem11  39621  prtlem15  39630  cvrat4  40198  lcfl6  42255  dvdsexpnn0  43076  harval3  44247  clcnvlem  44332  cnvrcl0  44334  cnvtrcl0  44335  iunrelexpmin1  44417  iunrelexpmin2  44421  ormkglobd  47574  fcoresf1b  47790  aovmpt4g  47921  elsetpreimafvbi  48123  iccpartiltu  48154  iccpartgt  48159  iccpartgel  48161  reuopreuprim  48258  fmtnofac1  48305  gbepos  48506  grtrif1o  48690  grtriclwlk3  48693  isubgr3stgrlem4  48717  gpgprismgr4cycllem3  48845  pgnbgreunbgrlem1  48861  pgnbgreunbgrlem3  48866  pgnbgreunbgrlem4  48867  pgnbgreunbgrlem5lem1  48868  pgnbgreunbgrlem5lem2  48869  pgnbgreunbgrlem5lem3  48870  pgnbgreunbgrlem6  48872  pgnbgreunbgr  48873  ellcoellss  49198  dignn0flhalflem2  49379  nn0sumshdiglemB  49383  1arympt1  49401  opth1neg  49587  opth2neg  49588  oppccatb  49777  fullthinc  50211