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  2479  pm2.61ne  3044  spcimgft  3514  unineq  4236  elpreqprlem  4824  oteqex  5477  otel3xp  5702  eqrelrdv2  5777  breldmg  5899  elrnmpt1  5950  predpoirr  6357  predfrirr  6358  limelon  6449  f1ssf1  6883  ndmfv  6943  eqfnun  7062  ffvresb  7153  isomin  7371  isofrlem  7374  oprabidw  7477  caovord3d  7658  eldifpw  7809  ssonuni  7821  onsucuni2  7872  ordzsl  7883  tfindsg  7899  findsg  7936  oteqimp  8047  frxp  8168  poxp  8170  fnwelem  8173  tfrlem11  8427  ord1eln01  8535  ord2eln012  8536  oacl  8574  omcl  8575  oecl  8576  oa0r  8577  om0r  8578  om1r  8582  oe1m  8584  oaordi  8585  oawordri  8589  oaass  8600  oarec  8601  omwordri  8611  odi  8618  omass  8619  oewordri  8632  oeworde  8633  oeordsuc  8634  oelim2  8635  oeoa  8637  oeoelem  8638  oeoe  8639  nnm0r  8650  nnacl  8651  nnacom  8657  nnaordi  8658  nnaass  8662  nndi  8663  nnmass  8664  nnmsucr  8665  nnmcom  8666  omabs  8691  brecop  8862  eceqoveq  8874  elpm2r  8896  map0g  8943  undifixp  8993  fundmen  9090  mapxpen  9193  mapunen  9196  pssnn  9215  php  9253  unxpdomlem2  9279  f1vrnfibi  9362  elfir  9437  wemapso2lem  9576  wdompwdom  9602  inf3lem1  9659  inf3lem3  9661  cantnfval2  9700  cantnfp1lem3  9711  r1sdom  9811  r1tr  9813  hfelhfOLD  9946  carden2a  10077  fidomtri2  10105  prdom2  10115  infxpenlem  10122  acndom  10160  fodomacn  10165  wdomfil  10170  alephon  10178  alephordi  10183  alephle  10197  alephfplem3  10215  dfac2a  10238  kmlem9  10267  cflm  10357  cfslb  10374  cfslbn  10375  infpssrlem3  10413  infpssrlem4  10414  fin23lem21  10447  fin23lem30  10450  isf34lem7  10487  isf34lem6  10488  fin67  10503  isfin7-2  10504  fin1a2lem7  10514  fin1a2lem10  10517  iundom2g  10654  konigthlem  10683  alephreg  10697  gchdomtri  10744  wunr1om  10834  tskr1om  10882  inar1  10890  grur1a  10934  indpi  11022  genpprecl  11116  genpnmax  11122  addcmpblnr  11184  recexsrlem  11218  map2psrpr  11225  ax1rid  11276  axpre-mulgt0  11283  ltle  11428  nnmulcl  12389  nnsub  12412  nn0sub  12686  nneo  12813  uz11  13020  xrltle  13308  xltnegi  13376  xrsupsslem  13467  xrinfmsslem  13468  xrub  13472  supxrunb1  13479  supxrunb2  13480  om2uzuzi  14122  uzrdgxfr  14140  seqcl2  14193  seqfveq2  14197  seqshft2  14201  seqsplit  14208  seqcaopr3  14210  seqf1olem2a  14213  seqid2  14221  seqhomo  14222  ser1const  14231  m1expcl2  14258  expadd  14277  expmul  14280  faclbnd  14464  hashfzp1  14606  hashmap  14610  hashf1lem2  14631  hashf1  14632  seqcoll  14639  wrdsymb0  14724  len0nnbi  14726  eqs1  14791  swrdnd2  14836  wrd2ind  14903  pfxccatin12lem2c  14910  pfxccatin12lem2  14911  swrdccatin1d  14923  repswccat  14968  repswcshw  14994  cshwcshid  15009  rtrclreclem3  15245  rtrclreclem4  15246  dfrtrcl2  15247  relexpindlem  15248  relexpind  15249  rtrclind  15250  recan  15536  rexanre  15546  rlimcn3  15789  caurcvg2  15877  fsumiun  16020  efexp  16301  rpnnen2lem12  16425  dvdstr  16496  alzdvds  16522  zob  16561  sumeven  16589  sumodd  16590  bitsinv1  16644  smu01lem  16687  smupval  16690  smueqlem  16692  smumullem  16694  seq1st  16778  lcmfunsnlem2lem1  16845  lcmfunsnlem2lem2  16846  cncongr2  16875  prmdiveq  16995  odzdvds  17005  pythagtriplem2  17027  pcexp  17069  vdwlem13  17203  ramz  17235  prmolefac  17256  elrestr  17631  xpsff1o  17771  subsubc  18060  clatl  18714  frmdgsum  19090  sursubmefmnd  19124  injsubmefmnd  19125  smndex1mndlem  19140  dfgrp3e  19282  mulgneg2  19350  mulgnnass  19351  mhmmulg  19357  gsumwrev  19613  symgextf1lem  19667  symgfixelsi  19682  pmtrdifellem4  19726  sylow1lem1  19845  efgsfo  19986  efgred  19995  cyggexb  20146  gsumzres  20156  gsum2dlem2  20218  mulgass2  20573  rngimcnv  20719  funcrngcsetc  20925  funcrngcsetcALT  20926  rhmsscrnghm  20950  funcringcsetc  20959  lmodprop2d  21232  lspsnne2  21429  lspsneu  21434  cnfldmulg  21743  cnfldexp  21744  zrhpsgnelbas  21933  assapropd  22212  mplcoe1  22379  mplcoe3  22380  mplcoe5  22382  mhpvarcl  22502  ply1sclf1  22641  mat1scmat  22887  matunitlindflem2  23028  restopn2  23528  cnpf2  23601  cmpfi  23759  txcn  23978  txlm  24000  xkoptsub  24006  xkopjcn  24008  ufildr  24283  cnflf  24354  fclsnei  24371  fclscmp  24382  ufilcmp  24384  cnfcf  24394  symgtgp  24458  isxms2  24800  met2ndc  24875  metustbl  24918  tngngp2  25004  clmmulg  25455  iscau4  25633  ovolunlem1a  25850  ovolicc2lem4  25874  volfiniun  25901  voliunlem1  25904  volsup  25910  dvnadd  26282  dvnres  26284  dvcobr  26299  ply1nzb  26474  plypf1  26564  dgrle  26595  coeaddlem  26601  dgrlt  26618  dvntaylp  26731  cxpmul2  27050  rlimcnp  27326  facgam  27426  wilthlem2  27429  isnsqf  27495  musum  27551  chtub  27572  chpval2  27578  gausslemma2dlem0i  27724  dchrisumlem1  27849  qabvexp  27986  ostthlem2  27988  fltoprmlem2  28027  nodenselem8  28081  lesrec  28218  bday1  28233  sltsleft  28279  sltsright  28280  oncutlt  28683  noseqind  28711  dfnns2  28791  bdaypw2n0bnd  28883  axsegconlem1  29528  ax5seglem4  29543  ax5seglem5  29544  axlowdimlem15  29567  axcontlem2  29576  axcontlem4  29578  incistruhgr  29690  upgredg2vtx  29752  upgredgpr  29753  numedglnl  29755  uhgr2edg  29822  nbupgruvtxres  30021  cusgrfilem1  30069  wlkres  30282  wlkp1lem2  30286  pthdivtx  30345  pthdlem2lem  30386  wlkiswwlks2lem4  30494  wwlksnredwwlkn0  30518  wwlksnextwrd  30519  wwlksnfi  30528  wwlksnextprop  30534  clwlkclwwlklem2a  30622  clwlkclwwlkf1lem2  30629  erclwwlksym  30645  clwwlkf1  30673  eleclclwwlknlem2  30685  erclwwlknsym  30694  clwwlknonex2  30733  eupth2lem3lem6  30867  frgr3vlem1  30907  3vfriswmgrlem  30911  wlkl0  31001  sspval  31358  nmosetre  31399  nmobndseqi  31414  nmobndseqiALT  31415  orthcom  31743  shsva  31955  shmodsi  32024  h1datomi  32216  nmopsetretALT  32498  nmfnsetre  32512  lnopcnbd  32671  pjclem4  32834  pj3si  32842  ssmd1  32946  atom1d  32988  chjatom  32992  atcvat4i  33032  cdj3lem2a  33071  cdj3lem3a  33074  disjunsn  33263  unitdivcld  34616  xrge0iifiso  34650  dya2iocuni  34998  bnj168  35444  bnj535  35603  bnj590  35623  bnj594  35625  bnj938  35650  bnj1118  35697  bnj1128  35703  fnrelpredd  35817  acnum  35860  j00smo  36018  deranglem  36111  subfacp1lem6  36130  subfacval2  36132  cvmlift2lem12  36259  satffun  36354  mrsubvrs  36467  msrrcl  36488  mclsax  36514  dfon2lem6  36741  rdgprc  36747  ifscgr  37000  btwncolinear1  37025  opnrebl2  37300  nn0prpw  37302  ordcmp  37426  findreccl  37432  nndivlub  37437  axtcond  37457  dfttc2g  37485  mh-inf3f1  37520  bj-rest0  38218  bj-isrvec2  38426  topdifinffinlem  38475  iooelexlt  38490  rdgeqoa  38498  exrecfnlem  38507  wl-mo3t  38713  poimirlem2  38745  poimirlem23  38766  poimirlem28  38771  poimirlem29  38772  poimirlem31  38774  poimirlem32  38775  sdclem2  38879  sdclem1  38880  prdsbnd2  38932  ismtyval  38937  rrnequiv  38972  isexid2  38992  ismndo1  39010  exidreslem  39014  rngo2  39044  rngoueqz  39077  risci  39124  eldisjdmqsim  39952  prtlem11  40126  prtlem15  40135  cvrat4  40703  lcfl6  42760  dvdsexpnn0  43590  harval3  44742  clcnvlem  44826  cnvrcl0  44828  cnvtrcl0  44829  iunrelexpmin1  44911  iunrelexpmin2  44915  ormkglobd  48102  fcoresf1b  48355  aovmpt4g  48486  elsetpreimafvbi  48688  iccpartiltu  48719  iccpartgt  48724  iccpartgel  48726  reuopreuprim  48823  fmtnofac1  48870  gbepos  49071  grtrif1o  49255  grtriclwlk3  49258  isubgr3stgrlem4  49282  gpgprismgr4cycllem3  49410  pgnbgreunbgrlem1  49426  pgnbgreunbgrlem3  49431  pgnbgreunbgrlem4  49432  pgnbgreunbgrlem5lem1  49433  pgnbgreunbgrlem5lem2  49434  pgnbgreunbgrlem5lem3  49435  pgnbgreunbgrlem6  49437  pgnbgreunbgr  49438  ellcoellss  49762  dignn0flhalflem2  49943  nn0sumshdiglemB  49947  1arympt1  49965  opth1neg  50152  opth2neg  50153  oppccatb  50345  fullthinc  50800