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  2476  pm2.61ne  3040  spcimgft  3510  unineq  4233  elpreqprlem  4820  oteqex  5471  otel3xp  5696  eqrelrdv2  5770  breldmg  5890  elrnmpt1  5941  predpoirr  6336  predfrirr  6337  limelon  6428  f1ssf1  6857  ndmfv  6917  eqfnun  7036  ffvresb  7126  isomin  7345  isofrlem  7348  oprabidw  7451  caovord3d  7631  eldifpw  7782  ssonuni  7794  onsucuni2  7845  ordzsl  7856  tfindsg  7872  findsg  7909  oteqimp  8020  frxp  8140  poxp  8142  fnwelem  8145  tfrlem11  8399  ord1eln01  8507  ord2eln012  8508  oacl  8546  omcl  8547  oecl  8548  oa0r  8549  om0r  8550  om1r  8554  oe1m  8556  oaordi  8557  oawordri  8561  oaass  8572  oarec  8573  omwordri  8583  odi  8590  omass  8591  oewordri  8604  oeworde  8605  oeordsuc  8606  oelim2  8607  oeoa  8609  oeoelem  8610  oeoe  8611  nnm0r  8622  nnacl  8623  nnacom  8629  nnaordi  8630  nnaass  8634  nndi  8635  nnmass  8636  nnmsucr  8637  nnmcom  8638  omabs  8663  brecop  8834  eceqoveq  8846  elpm2r  8868  map0g  8915  undifixp  8965  fundmen  9062  mapxpen  9165  mapunen  9168  pssnn  9187  php  9225  unxpdomlem2  9251  f1vrnfibi  9334  elfir  9410  wemapso2lem  9549  wdompwdom  9575  inf3lem1  9632  inf3lem3  9634  cantnfval2  9673  cantnfp1lem3  9684  r1sdom  9784  r1tr  9786  hfelhfOLD  9919  carden2a  10050  fidomtri2  10078  prdom2  10088  infxpenlem  10095  acndom  10133  fodomacn  10138  wdomfil  10143  alephon  10151  alephordi  10156  alephle  10170  alephfplem3  10188  dfac2a  10211  kmlem9  10240  cflm  10330  cfslb  10347  cfslbn  10348  infpssrlem3  10386  infpssrlem4  10387  fin23lem21  10420  fin23lem30  10423  isf34lem7  10460  isf34lem6  10461  fin67  10476  isfin7-2  10477  fin1a2lem7  10487  fin1a2lem10  10490  iundom2g  10627  konigthlem  10656  alephreg  10670  gchdomtri  10717  wunr1om  10807  tskr1om  10855  inar1  10863  grur1a  10907  indpi  10995  genpprecl  11089  genpnmax  11095  addcmpblnr  11157  recexsrlem  11191  map2psrpr  11198  ax1rid  11249  axpre-mulgt0  11256  ltle  11401  nnmulcl  12362  nnsub  12385  nn0sub  12659  nneo  12786  uz11  12993  xrltle  13281  xltnegi  13349  xrsupsslem  13440  xrinfmsslem  13441  xrub  13445  supxrunb1  13452  supxrunb2  13453  om2uzuzi  14095  uzrdgxfr  14113  seqcl2  14166  seqfveq2  14170  seqshft2  14174  seqsplit  14181  seqcaopr3  14183  seqf1olem2a  14186  seqid2  14194  seqhomo  14195  ser1const  14204  m1expcl2  14231  expadd  14250  expmul  14253  faclbnd  14437  hashfzp1  14579  hashmap  14583  hashf1lem2  14604  hashf1  14605  seqcoll  14612  wrdsymb0  14697  len0nnbi  14699  eqs1  14764  swrdnd2  14809  wrd2ind  14876  pfxccatin12lem2c  14883  pfxccatin12lem2  14884  swrdccatin1d  14896  repswccat  14941  repswcshw  14967  cshwcshid  14982  rtrclreclem3  15218  rtrclreclem4  15219  dfrtrcl2  15220  relexpindlem  15221  relexpind  15222  rtrclind  15223  recan  15509  rexanre  15519  rlimcn3  15762  caurcvg2  15850  fsumiun  15993  efexp  16274  rpnnen2lem12  16398  dvdstr  16469  alzdvds  16495  zob  16534  sumeven  16562  sumodd  16563  bitsinv1  16617  smu01lem  16660  smupval  16663  smueqlem  16665  smumullem  16667  seq1st  16751  lcmfunsnlem2lem1  16818  lcmfunsnlem2lem2  16819  cncongr2  16848  prmdiveq  16968  odzdvds  16978  pythagtriplem2  17000  pcexp  17042  vdwlem13  17176  ramz  17208  prmolefac  17229  elrestr  17604  xpsff1o  17744  subsubc  18033  clatl  18687  frmdgsum  19063  sursubmefmnd  19097  injsubmefmnd  19098  smndex1mndlem  19113  dfgrp3e  19255  mulgneg2  19323  mulgnnass  19324  mhmmulg  19330  gsumwrev  19585  symgextf1lem  19639  symgfixelsi  19654  pmtrdifellem4  19698  sylow1lem1  19817  efgsfo  19958  efgred  19967  cyggexb  20118  gsumzres  20128  gsum2dlem2  20190  mulgass2  20545  rngimcnv  20691  funcrngcsetc  20897  funcrngcsetcALT  20898  rhmsscrnghm  20922  funcringcsetc  20931  lmodprop2d  21204  lspsnne2  21401  lspsneu  21406  cnfldmulg  21715  cnfldexp  21716  zrhpsgnelbas  21905  assapropd  22184  mplcoe1  22351  mplcoe3  22352  mplcoe5  22354  mhpvarcl  22474  ply1sclf1  22613  mat1scmat  22859  matunitlindflem2  23000  restopn2  23500  cnpf2  23573  cmpfi  23731  txcn  23950  txlm  23972  xkoptsub  23978  xkopjcn  23980  ufildr  24255  cnflf  24326  fclsnei  24343  fclscmp  24354  ufilcmp  24356  cnfcf  24366  symgtgp  24430  isxms2  24772  met2ndc  24847  metustbl  24890  tngngp2  24976  clmmulg  25427  iscau4  25605  ovolunlem1a  25822  ovolicc2lem4  25846  volfiniun  25873  voliunlem1  25876  volsup  25882  dvnadd  26254  dvnres  26256  dvcobr  26271  ply1nzb  26446  plypf1  26536  dgrle  26567  coeaddlem  26573  dgrlt  26590  dvntaylp  26703  cxpmul2  27022  rlimcnp  27298  facgam  27398  wilthlem2  27401  isnsqf  27467  musum  27523  chtub  27544  chpval2  27550  gausslemma2dlem0i  27696  dchrisumlem1  27821  qabvexp  27958  ostthlem2  27960  fltoprmlem2  27999  nodenselem8  28053  lesrec  28190  bday1  28205  sltsleft  28251  sltsright  28252  oncutlt  28655  noseqind  28683  dfnns2  28763  bdaypw2n0bnd  28855  axsegconlem1  29500  ax5seglem4  29515  ax5seglem5  29516  axlowdimlem15  29539  axcontlem2  29548  axcontlem4  29550  incistruhgr  29662  upgredg2vtx  29724  upgredgpr  29725  numedglnl  29727  uhgr2edg  29794  nbupgruvtxres  29993  cusgrfilem1  30041  wlkres  30254  wlkp1lem2  30258  pthdivtx  30317  pthdlem2lem  30358  wlkiswwlks2lem4  30466  wwlksnredwwlkn0  30490  wwlksnextwrd  30491  wwlksnfi  30500  wwlksnextprop  30506  clwlkclwwlklem2a  30594  clwlkclwwlkf1lem2  30601  erclwwlksym  30617  clwwlkf1  30645  eleclclwwlknlem2  30657  erclwwlknsym  30666  clwwlknonex2  30705  eupth2lem3lem6  30839  frgr3vlem1  30879  3vfriswmgrlem  30883  wlkl0  30973  sspval  31330  nmosetre  31371  nmobndseqi  31386  nmobndseqiALT  31387  orthcom  31715  shsva  31927  shmodsi  31996  h1datomi  32188  nmopsetretALT  32470  nmfnsetre  32484  lnopcnbd  32643  pjclem4  32806  pj3si  32814  ssmd1  32918  atom1d  32960  chjatom  32964  atcvat4i  33004  cdj3lem2a  33043  cdj3lem3a  33046  disjunsn  33235  unitdivcld  34579  xrge0iifiso  34613  dya2iocuni  34961  bnj168  35407  bnj535  35566  bnj590  35586  bnj594  35588  bnj938  35613  bnj1118  35660  bnj1128  35666  fnrelpredd  35772  acnum  35811  j00smo  35944  deranglem  36017  subfacp1lem6  36036  subfacval2  36038  cvmlift2lem12  36165  satffun  36260  mrsubvrs  36373  msrrcl  36394  mclsax  36420  dfon2lem6  36642  rdgprc  36648  ifscgr  36901  btwncolinear1  36926  opnrebl2  37201  nn0prpw  37203  ordcmp  37327  findreccl  37333  nndivlub  37338  axtcond  37358  dfttc2g  37386  mh-inf3f1  37421  bj-rest0  38106  bj-isrvec2  38314  topdifinffinlem  38363  iooelexlt  38378  rdgeqoa  38386  exrecfnlem  38395  wl-mo3t  38601  poimirlem2  38633  poimirlem23  38654  poimirlem28  38659  poimirlem29  38660  poimirlem31  38662  poimirlem32  38663  sdclem2  38769  sdclem1  38770  prdsbnd2  38822  ismtyval  38827  rrnequiv  38862  isexid2  38882  ismndo1  38900  exidreslem  38904  rngo2  38934  rngoueqz  38967  risci  39014  eldisjdmqsim  39842  prtlem11  40016  prtlem15  40025  cvrat4  40593  lcfl6  42650  dvdsexpnn0  43479  harval3  44632  clcnvlem  44716  cnvrcl0  44718  cnvtrcl0  44719  iunrelexpmin1  44801  iunrelexpmin2  44805  ormkglobd  47980  fcoresf1b  48233  aovmpt4g  48364  elsetpreimafvbi  48566  iccpartiltu  48597  iccpartgt  48602  iccpartgel  48604  reuopreuprim  48701  fmtnofac1  48748  gbepos  48949  grtrif1o  49133  grtriclwlk3  49136  isubgr3stgrlem4  49160  gpgprismgr4cycllem3  49288  pgnbgreunbgrlem1  49304  pgnbgreunbgrlem3  49309  pgnbgreunbgrlem4  49310  pgnbgreunbgrlem5lem1  49311  pgnbgreunbgrlem5lem2  49312  pgnbgreunbgrlem5lem3  49313  pgnbgreunbgrlem6  49315  pgnbgreunbgr  49316  ellcoellss  49640  dignn0flhalflem2  49821  nn0sumshdiglemB  49825  1arympt1  49843  opth1neg  50030  opth2neg  50031  oppccatb  50223  fullthinc  50678