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  16715  odzdvds  16724  pythagtriplem2  16746  pcexp  16788  vdwlem13  16922  ramz  16954  prmolefac  16975  elrestr  17370  xpsff1o  17509  subsubc  17799  clatl  18460  frmdgsum  18774  sursubmefmnd  18808  injsubmefmnd  18809  smndex1mndlem  18821  dfgrp3e  18955  mulgneg2  19020  mulgnnass  19021  mhmmulg  19027  gsumwrev  19270  symgextf1lem  19325  symgfixelsi  19340  pmtrdifellem4  19384  sylow1lem1  19503  efgsfo  19644  efgred  19653  cyggexb  19804  gsumzres  19814  gsum2dlem2  19876  mulgass2  20193  rngimcnv  20343  funcrngcsetc  20521  funcrngcsetcALT  20522  rhmsscrnghm  20546  funcringcsetc  20555  lmodprop2d  20755  lspsnne2  20954  lspsneu  20959  cnfldmulg  21256  cnfldexp  21257  zrhpsgnelbas  21447  assapropd  21726  mplcoe1  21893  mplcoe3  21894  mplcoe5  21896  mhpvarcl  21990  ply1sclf1  22121  mat1scmat  22351  restopn2  22991  cnpf2  23064  cmpfi  23222  txcn  23440  txlm  23462  xkoptsub  23468  xkopjcn  23470  ufildr  23745  cnflf  23816  fclsnei  23833  fclscmp  23844  ufilcmp  23846  cnfcf  23856  symgtgp  23920  isxms2  24264  met2ndc  24342  metustbl  24385  tngngp2  24479  clmmulg  24938  iscau4  25117  ovolunlem1a  25335  ovolicc2lem4  25359  volfiniun  25386  voliunlem1  25389  volsup  25395  dvnadd  25769  dvnres  25771  dvcobr  25787  dvcobrOLD  25788  ply1nzb  25968  plypf1  26054  dgrle  26085  coeaddlem  26091  dgrlt  26109  dvntaylp  26212  cxpmul2  26527  rlimcnp  26801  facgam  26902  wilthlem2  26905  isnsqf  26971  musum  27027  chtub  27049  chpval2  27055  gausslemma2dlem0i  27201  dchrisumlem1  27326  qabvexp  27463  ostthlem2  27465  nodenselem8  27528  slerec  27656  bday1s  27668  ssltleft  27701  ssltright  27702  peano5n0s  28066  axsegconlem1  28599  ax5seglem4  28614  ax5seglem5  28615  axlowdimlem15  28638  axcontlem2  28647  axcontlem4  28649  incistruhgr  28763  upgredg2vtx  28825  upgredgpr  28826  numedglnl  28828  uhgr2edg  28889  nbupgruvtxres  29088  cusgrfilem1  29136  wlkres  29351  wlkp1lem2  29355  pthdivtx  29410  pthdlem2lem  29448  wlkiswwlks2lem4  29550  wwlksnredwwlkn0  29574  wwlksnextwrd  29575  wwlksnfi  29584  wwlksnextprop  29590  clwlkclwwlklem2a  29675  clwlkclwwlkf1lem2  29682  erclwwlksym  29698  clwwlkf1  29726  eleclclwwlknlem2  29738  erclwwlknsym  29747  clwwlknonex2  29786  eupth2lem3lem6  29910  frgr3vlem1  29950  3vfriswmgrlem  29954  wlkl0  30044  sspval  30400  nmosetre  30441  nmobndseqi  30456  nmobndseqiALT  30457  orthcom  30785  shsva  30997  shmodsi  31066  h1datomi  31258  nmopsetretALT  31540  nmfnsetre  31554  lnopcnbd  31713  pjclem4  31876  pj3si  31884  ssmd1  31988  atom1d  32030  chjatom  32034  atcvat4i  32074  cdj3lem2a  32113  cdj3lem3a  32116  disjunsn  32249  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