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  2478  pm2.61ne  3042  spcimgft  3513  unineq  4237  elpreqprlem  4829  oteqex  5481  otel3xp  5705  eqrelrdv2  5779  breldmg  5897  elrnmpt1  5948  cnveqb  6194  cnveq0  6195  predpoirr  6335  predfrirr  6336  limelon  6427  f1ssf1  6854  ndmfv  6914  eqfnun  7033  ffvresb  7123  isomin  7342  isofrlem  7345  oprabidw  7448  caovord3d  7628  eldifpw  7771  ssonuni  7783  onsucuni2  7834  ordzsl  7845  tfindsg  7861  findsg  7898  oteqimp  8009  frxp  8128  poxp  8130  fnwelem  8133  tfrlem11  8381  ord1eln01  8487  ord2eln012  8488  oacl  8526  omcl  8527  oecl  8528  oa0r  8529  om0r  8530  om1r  8534  oe1m  8536  oaordi  8537  oawordri  8541  oaass  8552  oarec  8553  omwordri  8563  odi  8570  omass  8571  oewordri  8584  oeworde  8585  oeordsuc  8586  oelim2  8587  oeoa  8589  oeoelem  8590  oeoe  8591  nnm0r  8602  nnacl  8603  nnacom  8609  nnaordi  8610  nnaass  8614  nndi  8615  nnmass  8616  nnmsucr  8617  nnmcom  8618  omabs  8643  brecop  8814  eceqoveq  8826  elpm2r  8848  map0g  8895  undifixp  8945  fundmen  9042  mapxpen  9145  mapunen  9148  pssnn  9167  php  9205  unxpdomlem2  9231  f1vrnfibi  9313  elfir  9389  wemapso2lem  9528  wdompwdom  9554  inf3lem1  9611  inf3lem3  9613  cantnfval2  9652  cantnfp1lem3  9663  r1sdom  9760  r1tr  9762  carden2a  9975  fidomtri2  10003  prdom2  10013  infxpenlem  10020  acndom  10058  fodomacn  10063  wdomfil  10068  alephon  10076  alephordi  10081  alephle  10095  alephfplem3  10113  dfac2a  10136  kmlem9  10165  cflm  10255  cfslb  10272  cfslbn  10273  infpssrlem3  10311  infpssrlem4  10312  fin23lem21  10345  fin23lem30  10348  isf34lem7  10385  isf34lem6  10386  fin67  10401  isfin7-2  10402  fin1a2lem7  10412  fin1a2lem10  10415  iundom2g  10552  konigthlem  10581  alephreg  10595  gchdomtri  10642  wunr1om  10732  tskr1om  10780  inar1  10788  grur1a  10832  indpi  10920  genpprecl  11014  genpnmax  11020  addcmpblnr  11082  recexsrlem  11116  map2psrpr  11123  ax1rid  11174  axpre-mulgt0  11181  ltle  11326  nnmulcl  12285  nnsub  12308  nn0sub  12582  nneo  12709  uz11  12916  xrltle  13204  xltnegi  13272  xrsupsslem  13363  xrinfmsslem  13364  xrub  13368  supxrunb1  13375  supxrunb2  13376  om2uzuzi  14017  uzrdgxfr  14035  seqcl2  14088  seqfveq2  14092  seqshft2  14096  seqsplit  14103  seqcaopr3  14105  seqf1olem2a  14108  seqid2  14116  seqhomo  14117  ser1const  14126  m1expcl2  14153  expadd  14172  expmul  14175  faclbnd  14358  hashfzp1  14500  hashmap  14504  hashf1lem2  14525  hashf1  14526  seqcoll  14533  wrdsymb0  14618  len0nnbi  14620  eqs1  14684  swrdnd2  14729  wrd2ind  14796  pfxccatin12lem2c  14803  pfxccatin12lem2  14804  swrdccatin1d  14816  repswccat  14861  repswcshw  14887  cshwcshid  14902  rtrclreclem3  15137  rtrclreclem4  15138  dfrtrcl2  15139  relexpindlem  15140  relexpind  15141  rtrclind  15142  recan  15428  rexanre  15438  rlimcn3  15681  caurcvg2  15769  fsumiun  15912  efexp  16195  rpnnen2lem12  16319  dvdstr  16390  alzdvds  16416  zob  16455  sumeven  16483  sumodd  16484  bitsinv1  16538  smu01lem  16581  smupval  16584  smueqlem  16586  smumullem  16588  seq1st  16667  lcmfunsnlem2lem1  16734  lcmfunsnlem2lem2  16735  cncongr2  16764  prmdiveq  16883  odzdvds  16893  pythagtriplem2  16915  pcexp  16957  vdwlem13  17091  ramz  17123  prmolefac  17144  elrestr  17519  xpsff1o  17659  subsubc  17948  clatl  18602  frmdgsum  18977  sursubmefmnd  19011  injsubmefmnd  19012  smndex1mndlem  19027  dfgrp3e  19169  mulgneg2  19237  mulgnnass  19238  mhmmulg  19244  gsumwrev  19499  symgextf1lem  19553  symgfixelsi  19568  pmtrdifellem4  19612  sylow1lem1  19731  efgsfo  19872  efgred  19881  cyggexb  20032  gsumzres  20042  gsum2dlem2  20104  mulgass2  20457  rngimcnv  20603  funcrngcsetc  20808  funcrngcsetcALT  20809  rhmsscrnghm  20833  funcringcsetc  20842  lmodprop2d  21114  lspsnne2  21311  lspsneu  21316  cnfldmulg  21623  cnfldexp  21624  zrhpsgnelbas  21813  assapropd  22092  mplcoe1  22259  mplcoe3  22260  mplcoe5  22262  mhpvarcl  22382  ply1sclf1  22521  mat1scmat  22767  matunitlindflem2  22908  restopn2  23408  cnpf2  23481  cmpfi  23639  txcn  23858  txlm  23880  xkoptsub  23886  xkopjcn  23888  ufildr  24163  cnflf  24234  fclsnei  24251  fclscmp  24262  ufilcmp  24264  cnfcf  24274  symgtgp  24338  isxms2  24680  met2ndc  24755  metustbl  24798  tngngp2  24884  clmmulg  25335  iscau4  25513  ovolunlem1a  25730  ovolicc2lem4  25754  volfiniun  25781  voliunlem1  25784  volsup  25790  dvnadd  26163  dvnres  26165  dvcobr  26180  ply1nzb  26355  plypf1  26445  dgrle  26476  coeaddlem  26482  dgrlt  26499  dvntaylp  26614  cxpmul2  26934  rlimcnp  27210  facgam  27310  wilthlem2  27313  isnsqf  27379  musum  27435  chtub  27456  chpval2  27462  gausslemma2dlem0i  27608  dchrisumlem1  27733  qabvexp  27870  ostthlem2  27872  nodenselem8  27935  lesrec  28072  bday1  28087  sltsleft  28133  sltsright  28134  oncutlt  28537  noseqind  28565  dfnns2  28645  bdaypw2n0bnd  28737  axsegconlem1  29382  ax5seglem4  29397  ax5seglem5  29398  axlowdimlem15  29421  axcontlem2  29430  axcontlem4  29432  incistruhgr  29544  upgredg2vtx  29606  upgredgpr  29607  numedglnl  29609  uhgr2edg  29676  nbupgruvtxres  29875  cusgrfilem1  29923  wlkres  30136  wlkp1lem2  30140  pthdivtx  30199  pthdlem2lem  30240  wlkiswwlks2lem4  30348  wwlksnredwwlkn0  30372  wwlksnextwrd  30373  wwlksnfi  30382  wwlksnextprop  30388  clwlkclwwlklem2a  30476  clwlkclwwlkf1lem2  30483  erclwwlksym  30499  clwwlkf1  30527  eleclclwwlknlem2  30539  erclwwlknsym  30548  clwwlknonex2  30587  eupth2lem3lem6  30721  frgr3vlem1  30761  3vfriswmgrlem  30765  wlkl0  30855  sspval  31212  nmosetre  31253  nmobndseqi  31268  nmobndseqiALT  31269  orthcom  31597  shsva  31809  shmodsi  31878  h1datomi  32070  nmopsetretALT  32352  nmfnsetre  32366  lnopcnbd  32525  pjclem4  32688  pj3si  32696  ssmd1  32800  atom1d  32842  chjatom  32846  atcvat4i  32886  cdj3lem2a  32925  cdj3lem3a  32928  disjunsn  33075  unitdivcld  34419  xrge0iifiso  34453  dya2iocuni  34802  bnj168  35248  bnj535  35407  bnj590  35427  bnj594  35429  bnj938  35454  bnj1118  35501  bnj1128  35507  fnrelpredd  35604  acnum  35646  deranglem  35753  subfacp1lem6  35772  subfacval2  35774  cvmlift2lem12  35901  satffun  35996  mrsubvrs  36109  msrrcl  36130  mclsax  36156  dfon2lem6  36373  rdgprc  36379  ifscgr  36632  btwncolinear1  36657  hfelhf  36769  opnrebl2  36948  nn0prpw  36950  ordcmp  37074  findreccl  37080  nndivlub  37085  axtcond  37105  dfttc2g  37133  mh-inf3f1  37168  bj-rest0  37851  bj-isrvec2  38060  topdifinffinlem  38109  iooelexlt  38124  rdgeqoa  38132  exrecfnlem  38141  wl-mo3t  38347  poimirlem2  38379  poimirlem23  38400  poimirlem28  38405  poimirlem29  38406  poimirlem31  38408  poimirlem32  38409  sdclem2  38500  sdclem1  38501  prdsbnd2  38553  ismtyval  38558  rrnequiv  38593  isexid2  38613  ismndo1  38631  exidreslem  38635  rngo2  38665  rngoueqz  38698  risci  38745  eldisjdmqsim  39573  prtlem11  39747  prtlem15  39756  cvrat4  40324  lcfl6  42381  dvdsexpnn0  43217  harval3  44386  clcnvlem  44471  cnvrcl0  44473  cnvtrcl0  44474  iunrelexpmin1  44556  iunrelexpmin2  44560  ormkglobd  47713  fcoresf1b  47966  aovmpt4g  48097  elsetpreimafvbi  48299  iccpartiltu  48330  iccpartgt  48335  iccpartgel  48337  reuopreuprim  48434  fmtnofac1  48481  gbepos  48682  grtrif1o  48866  grtriclwlk3  48869  isubgr3stgrlem4  48893  gpgprismgr4cycllem3  49021  pgnbgreunbgrlem1  49037  pgnbgreunbgrlem3  49042  pgnbgreunbgrlem4  49043  pgnbgreunbgrlem5lem1  49044  pgnbgreunbgrlem5lem2  49045  pgnbgreunbgrlem5lem3  49046  pgnbgreunbgrlem6  49048  pgnbgreunbgr  49049  ellcoellss  49373  dignn0flhalflem2  49554  nn0sumshdiglemB  49558  1arympt1  49576  opth1neg  49762  opth2neg  49763  oppccatb  49950  fullthinc  50384