Theorem syl5ibr 246

Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)

Hypotheses

Ref	Expression
syl5ibr.1	⊢ (𝜑 → 𝜃)
syl5ibr.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5ibr	⊢ (𝜒 → (𝜑 → 𝜓))

Proof of Theorem syl5ibr

Step	Hyp	Ref	Expression
1		syl5ibr.1	. 2 ⊢ (𝜑 → 𝜃)
2		syl5ibr.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	bicomd 222	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	syl5ib 244	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  247  biimprd  248  exdistrf  2445  pm2.61ne  3028  unineq  4217  elpreqprlem  4802  oteqex  5427  elopabrOLD  5489  otel3xp  5644  eqrelrdv2  5717  breldmg  5831  elrnmpt1  5879  cnveqb  6114  cnveq0  6115  predpoirr  6251  predfrirr  6252  limelon  6344  f1ssf1  6778  ndmfv  6836  ffvresb  7030  isomin  7240  isofrlem  7243  oprabidw  7338  caovord3d  7514  eldifpw  7650  ssonuni  7662  onsucuni2  7713  ordzsl  7724  tfindsg  7739  findsg  7778  oteqimp  7882  frxp  7998  poxp  8000  fnwelem  8003  suppssOLD  8042  wfrlem14OLD  8184  tfrlem11  8250  ord1eln01  8357  ord2eln012  8358  oacl  8396  omcl  8397  oecl  8398  oa0r  8399  om0r  8400  om1r  8405  oe1m  8407  oaordi  8408  oawordri  8412  oaass  8423  oarec  8424  omwordri  8434  odi  8441  omass  8442  oewordri  8454  oeworde  8455  oeordsuc  8456  oelim2  8457  oeoa  8459  oeoelem  8460  oeoe  8461  nnm0r  8472  nnacl  8473  nnacom  8479  nnaordi  8480  nnaass  8484  nndi  8485  nnmass  8486  nnmsucr  8487  nnmcom  8488  omabs  8512  brecop  8630  eceqoveq  8642  elpm2r  8664  map0g  8703  undifixp  8753  fundmen  8856  mapxpen  8968  mapunen  8971  pssnn  8989  php  9031  phpOLD  9043  unxpdomlem2  9072  pssnnOLD  9084  f1vrnfibi  9148  elfir  9218  wemapso2lem  9355  wdompwdom  9381  inf3lem1  9430  inf3lem3  9432  cantnfval2  9471  cantnfp1lem3  9482  r1sdom  9576  r1tr  9578  carden2a  9768  fidomtri2  9796  prdom2  9808  infxpenlem  9815  acndom  9853  fodomacn  9858  wdomfil  9863  alephon  9871  alephordi  9876  alephle  9890  alephfplem3  9908  dfac2a  9931  kmlem9  9960  cflm  10052  cfslb  10068  cfslbn  10069  infpssrlem3  10107  infpssrlem4  10108  fin23lem21  10141  fin23lem30  10144  isf34lem7  10181  isf34lem6  10182  fin67  10197  isfin7-2  10198  fin1a2lem7  10208  fin1a2lem10  10211  iundom2g  10342  konigthlem  10370  alephreg  10384  gchdomtri  10431  wunr1om  10521  tskr1om  10569  inar1  10577  grur1a  10621  indpi  10709  genpprecl  10803  genpnmax  10809  addcmpblnr  10871  recexsrlem  10905  map2psrpr  10912  ax1rid  10963  axpre-mulgt0  10970  ltle  11109  nnmulcl  12043  nnsub  12063  nn0sub  12329  nneo  12450  uz11  12653  xrltle  12929  xltnegi  12996  xrsupsslem  13087  xrinfmsslem  13088  xrub  13092  supxrunb1  13099  supxrunb2  13100  om2uzuzi  13715  uzrdgxfr  13733  seqcl2  13787  seqfveq2  13791  seqshft2  13795  seqsplit  13802  seqcaopr3  13804  seqf1olem2a  13807  seqid2  13815  seqhomo  13816  ser1const  13825  m1expcl2  13850  expadd  13871  expmul  13874  faclbnd  14050  hashfzp1  14191  hashmap  14195  hashfacenOLD  14212  hashf1lem1OLD  14214  hashf1lem2  14215  hashf1  14216  seqcoll  14223  wrdsymb0  14297  len0nnbi  14299  eqs1  14362  swrdnd2  14413  wrd2ind  14481  pfxccatin12lem2c  14488  pfxccatin12lem2  14489  swrdccatin1d  14501  repswccat  14544  repswcshw  14570  cshwcshid  14585  rtrclreclem3  14816  rtrclreclem4  14817  dfrtrcl2  14818  relexpindlem  14819  relexpind  14820  rtrclind  14821  recan  15093  rexanre  15103  rlimcn3  15344  caurcvg2  15434  fsumiun  15578  efexp  15855  rpnnen2lem12  15979  dvdstr  16048  alzdvds  16074  zob  16113  sumeven  16141  sumodd  16142  bitsinv1  16194  smu01lem  16237  smupval  16240  smueqlem  16242  smumullem  16244  seq1st  16321  lcmfunsnlem2lem1  16388  lcmfunsnlem2lem2  16389  cncongr2  16418  prmdiveq  16532  odzdvds  16541  pythagtriplem2  16563  pcexp  16605  vdwlem13  16739  ramz  16771  prmolefac  16792  elrestr  17184  xpsff1o  17323  subsubc  17613  clatl  18271  frmdgsum  18546  sursubmefmnd  18580  injsubmefmnd  18581  smndex1mndlem  18593  dfgrp3e  18720  mulgneg2  18782  mulgnnass  18783  mhmmulg  18789  gsumwrev  19018  symgextf1lem  19073  symgfixelsi  19088  pmtrdifellem4  19132  sylow1lem1  19248  efgsfo  19390  efgred  19399  cyggexb  19545  gsumzres  19555  gsum2dlem2  19617  ringadd2  19859  mulgass2  19885  lmodprop2d  20230  lspsnne2  20425  lspsneu  20430  cnfldmulg  20675  cnfldexp  20676  zrhpsgnelbas  20844  assapropd  21121  mplcoe1  21283  mplcoe3  21284  mplcoe5  21286  mhpvarcl  21383  ply1sclf1  21505  mat1scmat  21733  restopn2  22373  cnpf2  22446  cmpfi  22604  txcn  22822  txlm  22844  xkoptsub  22850  xkopjcn  22852  ufildr  23127  cnflf  23198  fclsnei  23215  fclscmp  23226  ufilcmp  23228  cnfcf  23238  symgtgp  23302  isxms2  23646  met2ndc  23724  metustbl  23767  tngngp2  23861  clmmulg  24309  iscau4  24488  ovolunlem1a  24705  ovolicc2lem4  24729  volfiniun  24756  voliunlem1  24759  volsup  24765  dvnadd  25138  dvnres  25140  dvcobr  25155  ply1nzb  25332  plypf1  25418  dgrle  25449  coeaddlem  25455  dgrlt  25472  dvntaylp  25575  cxpmul2  25889  rlimcnp  26160  facgam  26260  wilthlem2  26263  isnsqf  26329  musum  26385  chtub  26405  chpval2  26411  gausslemma2dlem0i  26557  dchrisumlem1  26682  qabvexp  26819  ostthlem2  26821  axsegconlem1  27330  ax5seglem4  27345  ax5seglem5  27346  axlowdimlem15  27369  axcontlem2  27378  axcontlem4  27380  incistruhgr  27494  upgredg2vtx  27556  upgredgpr  27557  numedglnl  27559  uhgr2edg  27620  nbupgruvtxres  27819  cusgrfilem1  27867  wlkres  28083  wlkp1lem2  28087  pthdivtx  28142  pthdlem2lem  28180  wlkiswwlks2lem4  28282  wwlksnredwwlkn0  28306  wwlksnextwrd  28307  wwlksnfi  28316  wwlksnextprop  28322  clwlkclwwlklem2a  28407  clwlkclwwlkf1lem2  28414  erclwwlksym  28430  clwwlkf1  28458  eleclclwwlknlem2  28470  erclwwlknsym  28479  clwwlknonex2  28518  eupth2lem3lem6  28642  frgr3vlem1  28682  3vfriswmgrlem  28686  wlkl0  28776  sspval  29130  nmosetre  29171  nmobndseqi  29186  nmobndseqiALT  29187  orthcom  29515  shsva  29727  shmodsi  29796  h1datomi  29988  nmopsetretALT  30270  nmfnsetre  30284  lnopcnbd  30443  pjclem4  30606  pj3si  30614  ssmd1  30718  atom1d  30760  chjatom  30764  atcvat4i  30804  cdj3lem2a  30843  cdj3lem3a  30846  disjunsn  30978  unitdivcld  31896  xrge0iifiso  31930  dya2iocuni  32295  bnj168  32754  bnj535  32915  bnj590  32935  bnj594  32937  bnj938  32962  bnj1118  33009  bnj1128  33015  fnrelpredd  33106  deranglem  33173  subfacp1lem6  33192  subfacval2  33194  cvmlift2lem12  33321  satffun  33416  mrsubvrs  33529  msrrcl  33550  mclsax  33576  dfon2lem6  33809  rdgprc  33815  nodenselem8  33939  slerec  34058  bday1s  34070  ssltleft  34099  ssltright  34100  ifscgr  34391  btwncolinear1  34416  hfelhf  34528  opnrebl2  34555  nn0prpw  34557  ordcmp  34681  findreccl  34687  nndivlub  34692  bj-rest0  35308  bj-isrvec2  35515  topdifinffinlem  35562  iooelexlt  35577  rdgeqoa  35585  exrecfnlem  35594  wl-mo3t  35775  matunitlindflem2  35818  poimirlem2  35823  poimirlem23  35844  poimirlem28  35849  poimirlem29  35850  poimirlem31  35852  poimirlem32  35853  eqfnun  35924  sdclem2  35944  sdclem1  35945  prdsbnd2  35997  ismtyval  36002  rrnequiv  36037  isexid2  36057  ismndo1  36075  exidreslem  36079  rngo2  36109  rngoueqz  36142  risci  36189  prtlem11  36922  prtlem15  36931  cvrat4  37499  lcfl6  39556  dvdsexpnn0  40378  harval3  41183  clcnvlem  41269  cnvrcl0  41271  cnvtrcl0  41272  iunrelexpmin1  41354  iunrelexpmin2  41358  fcoresf1b  44622  aovmpt4g  44751  elsetpreimafvbi  44901  iccpartiltu  44932  iccpartgt  44937  iccpartgel  44939  reuopreuprim  45036  fmtnofac1  45080  gbepos  45268  funcrngcsetc  45614  funcrngcsetcALT  45615  rhmsscrnghm  45642  funcringcsetc  45651  ellcoellss  45834  dignn0flhalflem2  46020  nn0sumshdiglemB  46024  1arympt1  46042  fullthinc  46385  tworepnotupword  46579