Theorem imbitrrid 245

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 222	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	imbitrid 243	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  syl5ibrcom  246  biimprd  247  exdistrf  2438  pm2.61ne  3019  unineq  4269  elpreqprlem  4858  oteqex  5490  elopabrOLD  5553  otel3xp  5712  eqrelrdv2  5785  breldmg  5899  elrnmpt1  5947  cnveqb  6185  cnveq0  6186  predpoirr  6324  predfrirr  6325  limelon  6418  f1ssf1  6855  ndmfv  6916  eqfnun  7028  ffvresb  7116  isomin  7326  isofrlem  7329  oprabidw  7432  caovord3d  7610  eldifpw  7748  ssonuni  7760  onsucuni2  7815  ordzsl  7827  tfindsg  7843  findsg  7883  oteqimp  7987  frxp  8106  poxp  8108  fnwelem  8111  suppssOLD  8174  wfrlem14OLD  8317  tfrlem11  8383  ord1eln01  8491  ord2eln012  8492  oacl  8530  omcl  8531  oecl  8532  oa0r  8533  om0r  8534  om1r  8538  oe1m  8540  oaordi  8541  oawordri  8545  oaass  8556  oarec  8557  omwordri  8567  odi  8574  omass  8575  oewordri  8587  oeworde  8588  oeordsuc  8589  oelim2  8590  oeoa  8592  oeoelem  8593  oeoe  8594  nnm0r  8605  nnacl  8606  nnacom  8612  nnaordi  8613  nnaass  8617  nndi  8618  nnmass  8619  nnmsucr  8620  nnmcom  8621  omabs  8645  brecop  8799  eceqoveq  8811  elpm2r  8834  map0g  8873  undifixp  8923  fundmen  9026  mapxpen  9138  mapunen  9141  pssnn  9163  php  9205  phpOLD  9217  unxpdomlem2  9246  pssnnOLD  9260  f1vrnfibi  9332  elfir  9405  wemapso2lem  9542  wdompwdom  9568  inf3lem1  9618  inf3lem3  9620  cantnfval2  9659  cantnfp1lem3  9670  r1sdom  9764  r1tr  9766  carden2a  9956  fidomtri2  9984  prdom2  9996  infxpenlem  10003  acndom  10041  fodomacn  10046  wdomfil  10051  alephon  10059  alephordi  10064  alephle  10078  alephfplem3  10096  dfac2a  10119  kmlem9  10148  cflm  10240  cfslb  10256  cfslbn  10257  infpssrlem3  10295  infpssrlem4  10296  fin23lem21  10329  fin23lem30  10332  isf34lem7  10369  isf34lem6  10370  fin67  10385  isfin7-2  10386  fin1a2lem7  10396  fin1a2lem10  10399  iundom2g  10530  konigthlem  10558  alephreg  10572  gchdomtri  10619  wunr1om  10709  tskr1om  10757  inar1  10765  grur1a  10809  indpi  10897  genpprecl  10991  genpnmax  10997  addcmpblnr  11059  recexsrlem  11093  map2psrpr  11100  ax1rid  11151  axpre-mulgt0  11158  ltle  11298  nnmulcl  12232  nnsub  12252  nn0sub  12518  nneo  12642  uz11  12843  xrltle  13124  xltnegi  13191  xrsupsslem  13282  xrinfmsslem  13283  xrub  13287  supxrunb1  13294  supxrunb2  13295  om2uzuzi  13910  uzrdgxfr  13928  seqcl2  13982  seqfveq2  13986  seqshft2  13990  seqsplit  13997  seqcaopr3  13999  seqf1olem2a  14002  seqid2  14010  seqhomo  14011  ser1const  14020  m1expcl2  14047  expadd  14066  expmul  14069  faclbnd  14246  hashfzp1  14387  hashmap  14391  hashfacenOLD  14410  hashf1lem1OLD  14412  hashf1lem2  14413  hashf1  14414  seqcoll  14421  wrdsymb0  14495  len0nnbi  14497  eqs1  14558  swrdnd2  14601  wrd2ind  14669  pfxccatin12lem2c  14676  pfxccatin12lem2  14677  swrdccatin1d  14689  repswccat  14732  repswcshw  14758  cshwcshid  14774  rtrclreclem3  15003  rtrclreclem4  15004  dfrtrcl2  15005  relexpindlem  15006  relexpind  15007  rtrclind  15008  recan  15279  rexanre  15289  rlimcn3  15530  caurcvg2  15620  fsumiun  15763  efexp  16040  rpnnen2lem12  16164  dvdstr  16233  alzdvds  16259  zob  16298  sumeven  16326  sumodd  16327  bitsinv1  16379  smu01lem  16422  smupval  16425  smueqlem  16427  smumullem  16429  seq1st  16504  lcmfunsnlem2lem1  16571  lcmfunsnlem2lem2  16572  cncongr2  16601  prmdiveq  16717  odzdvds  16726  pythagtriplem2  16748  pcexp  16790  vdwlem13  16924  ramz  16956  prmolefac  16977  elrestr  17372  xpsff1o  17511  subsubc  17801  clatl  18462  frmdgsum  18776  sursubmefmnd  18810  injsubmefmnd  18811  smndex1mndlem  18823  dfgrp3e  18957  mulgneg2  19024  mulgnnass  19025  mhmmulg  19031  gsumwrev  19274  symgextf1lem  19329  symgfixelsi  19344  pmtrdifellem4  19388  sylow1lem1  19507  efgsfo  19648  efgred  19657  cyggexb  19808  gsumzres  19818  gsum2dlem2  19880  mulgass2  20197  rngimcnv  20347  funcrngcsetc  20525  funcrngcsetcALT  20526  rhmsscrnghm  20550  funcringcsetc  20559  lmodprop2d  20759  lspsnne2  20958  lspsneu  20963  cnfldmulg  21260  cnfldexp  21261  zrhpsgnelbas  21454  assapropd  21733  mplcoe1  21901  mplcoe3  21902  mplcoe5  21904  mhpvarcl  21998  ply1sclf1  22129  mat1scmat  22362  restopn2  23002  cnpf2  23075  cmpfi  23233  txcn  23451  txlm  23473  xkoptsub  23479  xkopjcn  23481  ufildr  23756  cnflf  23827  fclsnei  23844  fclscmp  23855  ufilcmp  23857  cnfcf  23867  symgtgp  23931  isxms2  24275  met2ndc  24353  metustbl  24396  tngngp2  24490  clmmulg  24949  iscau4  25128  ovolunlem1a  25346  ovolicc2lem4  25370  volfiniun  25397  voliunlem1  25400  volsup  25406  dvnadd  25780  dvnres  25782  dvcobr  25798  dvcobrOLD  25799  ply1nzb  25979  plypf1  26065  dgrle  26096  coeaddlem  26102  dgrlt  26120  dvntaylp  26223  cxpmul2  26538  rlimcnp  26812  facgam  26913  wilthlem2  26916  isnsqf  26982  musum  27038  chtub  27060  chpval2  27066  gausslemma2dlem0i  27212  dchrisumlem1  27337  qabvexp  27474  ostthlem2  27476  nodenselem8  27539  slerec  27667  bday1s  27679  ssltleft  27712  ssltright  27713  peano5n0s  28077  axsegconlem1  28610  ax5seglem4  28625  ax5seglem5  28626  axlowdimlem15  28649  axcontlem2  28658  axcontlem4  28660  incistruhgr  28774  upgredg2vtx  28836  upgredgpr  28837  numedglnl  28839  uhgr2edg  28900  nbupgruvtxres  29099  cusgrfilem1  29147  wlkres  29362  wlkp1lem2  29366  pthdivtx  29421  pthdlem2lem  29459  wlkiswwlks2lem4  29561  wwlksnredwwlkn0  29585  wwlksnextwrd  29586  wwlksnfi  29595  wwlksnextprop  29601  clwlkclwwlklem2a  29686  clwlkclwwlkf1lem2  29693  erclwwlksym  29709  clwwlkf1  29737  eleclclwwlknlem2  29749  erclwwlknsym  29758  clwwlknonex2  29797  eupth2lem3lem6  29921  frgr3vlem1  29961  3vfriswmgrlem  29965  wlkl0  30055  sspval  30411  nmosetre  30452  nmobndseqi  30467  nmobndseqiALT  30468  orthcom  30796  shsva  31008  shmodsi  31077  h1datomi  31269  nmopsetretALT  31551  nmfnsetre  31565  lnopcnbd  31724  pjclem4  31887  pj3si  31895  ssmd1  31999  atom1d  32041  chjatom  32045  atcvat4i  32085  cdj3lem2a  32124  cdj3lem3a  32127  disjunsn  32260  unitdivcld  33336  xrge0iifiso  33370  dya2iocuni  33737  bnj168  34196  bnj535  34356  bnj590  34376  bnj594  34378  bnj938  34403  bnj1118  34450  bnj1128  34456  fnrelpredd  34547  deranglem  34612  subfacp1lem6  34631  subfacval2  34633  cvmlift2lem12  34760  satffun  34855  mrsubvrs  34968  msrrcl  34989  mclsax  35015  dfon2lem6  35221  rdgprc  35227  ifscgr  35477  btwncolinear1  35502  hfelhf  35614  opnrebl2  35662  nn0prpw  35664  ordcmp  35788  findreccl  35794  nndivlub  35799  bj-rest0  36430  bj-isrvec2  36637  topdifinffinlem  36684  iooelexlt  36699  rdgeqoa  36707  exrecfnlem  36716  wl-mo3t  36897  matunitlindflem2  36941  poimirlem2  36946  poimirlem23  36967  poimirlem28  36972  poimirlem29  36973  poimirlem31  36975  poimirlem32  36976  sdclem2  37066  sdclem1  37067  prdsbnd2  37119  ismtyval  37124  rrnequiv  37159  isexid2  37179  ismndo1  37197  exidreslem  37201  rngo2  37231  rngoueqz  37264  risci  37311  prtlem11  38192  prtlem15  38201  cvrat4  38770  lcfl6  40827  dvdsexpnn0  41687  harval3  42744  clcnvlem  42829  cnvrcl0  42831  cnvtrcl0  42832  iunrelexpmin1  42914  iunrelexpmin2  42918  tworepnotupword  46051  fcoresf1b  46231  aovmpt4g  46360  elsetpreimafvbi  46510  iccpartiltu  46541  iccpartgt  46546  iccpartgel  46548  reuopreuprim  46645  fmtnofac1  46689  gbepos  46877  ellcoellss  47270  dignn0flhalflem2  47456  nn0sumshdiglemB  47460  1arympt1  47478  fullthinc  47820