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  2477  pm2.61ne  3041  spcimgft  3511  unineq  4234  elpreqprlem  4826  oteqex  5472  otel3xp  5697  eqrelrdv2  5771  breldmg  5891  elrnmpt1  5942  cnveqb  6188  cnveq0  6189  predpoirr  6329  predfrirr  6330  limelon  6421  f1ssf1  6849  ndmfv  6909  eqfnun  7028  ffvresb  7118  isomin  7337  isofrlem  7340  oprabidw  7443  caovord3d  7623  eldifpw  7771  ssonuni  7783  onsucuni2  7834  ordzsl  7845  tfindsg  7861  findsg  7898  oteqimp  8009  frxp  8127  poxp  8129  fnwelem  8132  tfrlem11  8380  ord1eln01  8488  ord2eln012  8489  oacl  8527  omcl  8528  oecl  8529  oa0r  8530  om0r  8531  om1r  8535  oe1m  8537  oaordi  8538  oawordri  8542  oaass  8553  oarec  8554  omwordri  8564  odi  8571  omass  8572  oewordri  8585  oeworde  8586  oeordsuc  8587  oelim2  8588  oeoa  8590  oeoelem  8591  oeoe  8592  nnm0r  8603  nnacl  8604  nnacom  8610  nnaordi  8611  nnaass  8615  nndi  8616  nnmass  8617  nnmsucr  8618  nnmcom  8619  omabs  8644  brecop  8815  eceqoveq  8827  elpm2r  8849  map0g  8896  undifixp  8946  fundmen  9043  mapxpen  9146  mapunen  9149  pssnn  9168  php  9206  unxpdomlem2  9232  f1vrnfibi  9315  elfir  9391  wemapso2lem  9530  wdompwdom  9556  inf3lem1  9613  inf3lem3  9615  cantnfval2  9654  cantnfp1lem3  9665  r1sdom  9764  r1tr  9766  hfelhfOLD  9897  carden2a  10028  fidomtri2  10056  prdom2  10066  infxpenlem  10073  acndom  10111  fodomacn  10116  wdomfil  10121  alephon  10129  alephordi  10134  alephle  10148  alephfplem3  10166  dfac2a  10189  kmlem9  10218  cflm  10308  cfslb  10325  cfslbn  10326  infpssrlem3  10364  infpssrlem4  10365  fin23lem21  10398  fin23lem30  10401  isf34lem7  10438  isf34lem6  10439  fin67  10454  isfin7-2  10455  fin1a2lem7  10465  fin1a2lem10  10468  iundom2g  10605  konigthlem  10634  alephreg  10648  gchdomtri  10695  wunr1om  10785  tskr1om  10833  inar1  10841  grur1a  10885  indpi  10973  genpprecl  11067  genpnmax  11073  addcmpblnr  11135  recexsrlem  11169  map2psrpr  11176  ax1rid  11227  axpre-mulgt0  11234  ltle  11379  nnmulcl  12340  nnsub  12363  nn0sub  12637  nneo  12764  uz11  12971  xrltle  13259  xltnegi  13327  xrsupsslem  13418  xrinfmsslem  13419  xrub  13423  supxrunb1  13430  supxrunb2  13431  om2uzuzi  14072  uzrdgxfr  14090  seqcl2  14143  seqfveq2  14147  seqshft2  14151  seqsplit  14158  seqcaopr3  14160  seqf1olem2a  14163  seqid2  14171  seqhomo  14172  ser1const  14181  m1expcl2  14208  expadd  14227  expmul  14230  faclbnd  14414  hashfzp1  14556  hashmap  14560  hashf1lem2  14581  hashf1  14582  seqcoll  14589  wrdsymb0  14674  len0nnbi  14676  eqs1  14740  swrdnd2  14785  wrd2ind  14852  pfxccatin12lem2c  14859  pfxccatin12lem2  14860  swrdccatin1d  14872  repswccat  14917  repswcshw  14943  cshwcshid  14958  rtrclreclem3  15193  rtrclreclem4  15194  dfrtrcl2  15195  relexpindlem  15196  relexpind  15197  rtrclind  15198  recan  15484  rexanre  15494  rlimcn3  15737  caurcvg2  15825  fsumiun  15968  efexp  16249  rpnnen2lem12  16373  dvdstr  16444  alzdvds  16470  zob  16509  sumeven  16537  sumodd  16538  bitsinv1  16592  smu01lem  16635  smupval  16638  smueqlem  16640  smumullem  16642  seq1st  16726  lcmfunsnlem2lem1  16793  lcmfunsnlem2lem2  16794  cncongr2  16823  prmdiveq  16943  odzdvds  16953  pythagtriplem2  16975  pcexp  17017  vdwlem13  17151  ramz  17183  prmolefac  17204  elrestr  17579  xpsff1o  17719  subsubc  18008  clatl  18662  frmdgsum  19038  sursubmefmnd  19072  injsubmefmnd  19073  smndex1mndlem  19088  dfgrp3e  19230  mulgneg2  19298  mulgnnass  19299  mhmmulg  19305  gsumwrev  19560  symgextf1lem  19614  symgfixelsi  19629  pmtrdifellem4  19673  sylow1lem1  19792  efgsfo  19933  efgred  19942  cyggexb  20093  gsumzres  20103  gsum2dlem2  20165  mulgass2  20520  rngimcnv  20666  funcrngcsetc  20872  funcrngcsetcALT  20873  rhmsscrnghm  20897  funcringcsetc  20906  lmodprop2d  21179  lspsnne2  21376  lspsneu  21381  cnfldmulg  21690  cnfldexp  21691  zrhpsgnelbas  21880  assapropd  22159  mplcoe1  22326  mplcoe3  22327  mplcoe5  22329  mhpvarcl  22449  ply1sclf1  22588  mat1scmat  22834  matunitlindflem2  22975  restopn2  23475  cnpf2  23548  cmpfi  23706  txcn  23925  txlm  23947  xkoptsub  23953  xkopjcn  23955  ufildr  24230  cnflf  24301  fclsnei  24318  fclscmp  24329  ufilcmp  24331  cnfcf  24341  symgtgp  24405  isxms2  24747  met2ndc  24822  metustbl  24865  tngngp2  24951  clmmulg  25402  iscau4  25580  ovolunlem1a  25797  ovolicc2lem4  25821  volfiniun  25848  voliunlem1  25851  volsup  25857  dvnadd  26229  dvnres  26231  dvcobr  26246  ply1nzb  26421  plypf1  26511  dgrle  26542  coeaddlem  26548  dgrlt  26565  dvntaylp  26680  cxpmul2  26999  rlimcnp  27275  facgam  27375  wilthlem2  27378  isnsqf  27444  musum  27500  chtub  27521  chpval2  27527  gausslemma2dlem0i  27673  dchrisumlem1  27798  qabvexp  27935  ostthlem2  27937  fltoprmlem2  27976  nodenselem8  28030  lesrec  28167  bday1  28182  sltsleft  28228  sltsright  28229  oncutlt  28632  noseqind  28660  dfnns2  28740  bdaypw2n0bnd  28832  axsegconlem1  29477  ax5seglem4  29492  ax5seglem5  29493  axlowdimlem15  29516  axcontlem2  29525  axcontlem4  29527  incistruhgr  29639  upgredg2vtx  29701  upgredgpr  29702  numedglnl  29704  uhgr2edg  29771  nbupgruvtxres  29970  cusgrfilem1  30018  wlkres  30231  wlkp1lem2  30235  pthdivtx  30294  pthdlem2lem  30335  wlkiswwlks2lem4  30443  wwlksnredwwlkn0  30467  wwlksnextwrd  30468  wwlksnfi  30477  wwlksnextprop  30483  clwlkclwwlklem2a  30571  clwlkclwwlkf1lem2  30578  erclwwlksym  30594  clwwlkf1  30622  eleclclwwlknlem2  30634  erclwwlknsym  30643  clwwlknonex2  30682  eupth2lem3lem6  30816  frgr3vlem1  30856  3vfriswmgrlem  30860  wlkl0  30950  sspval  31307  nmosetre  31348  nmobndseqi  31363  nmobndseqiALT  31364  orthcom  31692  shsva  31904  shmodsi  31973  h1datomi  32165  nmopsetretALT  32447  nmfnsetre  32461  lnopcnbd  32620  pjclem4  32783  pj3si  32791  ssmd1  32895  atom1d  32937  chjatom  32941  atcvat4i  32981  cdj3lem2a  33020  cdj3lem3a  33023  disjunsn  33170  unitdivcld  34515  xrge0iifiso  34549  dya2iocuni  34898  bnj168  35344  bnj535  35503  bnj590  35523  bnj594  35525  bnj938  35550  bnj1118  35597  bnj1128  35603  fnrelpredd  35699  acnum  35733  deranglem  35900  subfacp1lem6  35919  subfacval2  35921  cvmlift2lem12  36048  satffun  36143  mrsubvrs  36256  msrrcl  36277  mclsax  36303  dfon2lem6  36520  rdgprc  36526  ifscgr  36779  btwncolinear1  36804  opnrebl2  37079  nn0prpw  37081  ordcmp  37205  findreccl  37211  nndivlub  37216  axtcond  37236  dfttc2g  37264  mh-inf3f1  37299  bj-rest0  37982  bj-isrvec2  38189  topdifinffinlem  38238  iooelexlt  38253  rdgeqoa  38261  exrecfnlem  38270  wl-mo3t  38476  poimirlem2  38508  poimirlem23  38529  poimirlem28  38534  poimirlem29  38535  poimirlem31  38537  poimirlem32  38538  sdclem2  38644  sdclem1  38645  prdsbnd2  38697  ismtyval  38702  rrnequiv  38737  isexid2  38757  ismndo1  38775  exidreslem  38779  rngo2  38809  rngoueqz  38842  risci  38889  eldisjdmqsim  39717  prtlem11  39891  prtlem15  39900  cvrat4  40468  lcfl6  42525  dvdsexpnn0  43354  harval3  44497  clcnvlem  44582  cnvrcl0  44584  cnvtrcl0  44585  iunrelexpmin1  44667  iunrelexpmin2  44671  ormkglobd  47831  fcoresf1b  48084  aovmpt4g  48215  elsetpreimafvbi  48417  iccpartiltu  48448  iccpartgt  48453  iccpartgel  48455  reuopreuprim  48552  fmtnofac1  48599  gbepos  48800  grtrif1o  48984  grtriclwlk3  48987  isubgr3stgrlem4  49011  gpgprismgr4cycllem3  49139  pgnbgreunbgrlem1  49155  pgnbgreunbgrlem3  49160  pgnbgreunbgrlem4  49161  pgnbgreunbgrlem5lem1  49162  pgnbgreunbgrlem5lem2  49163  pgnbgreunbgrlem5lem3  49164  pgnbgreunbgrlem6  49166  pgnbgreunbgr  49167  ellcoellss  49491  dignn0flhalflem2  49672  nn0sumshdiglemB  49676  1arympt1  49694  opth1neg  49880  opth2neg  49881  oppccatb  50068  fullthinc  50502