Theorem syl5ibr 248

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 225	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	syl5ib 246	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  syl5ibrcom  249  biimprd  250  exdistrf  2465  pm2.61ne  3102  unineq  4253  elpreqprlem  4789  oteqex  5382  elopabr  5439  otel3xp  5593  eqrelrdv2  5662  breldmg  5772  elrnmpt1  5824  cnveqb  6047  cnveq0  6048  predpoirr  6170  predfrirr  6171  limelon  6248  f1ssf1  6640  ndmfv  6694  ffvresb  6882  isomin  7084  isofrlem  7087  oprabidw  7181  caovord3d  7352  eldifpw  7484  ssonuni  7495  onsucuni2  7543  ordzsl  7554  tfindsg  7569  findsg  7603  oteqimp  7702  frxp  7814  poxp  7816  fnwelem  7819  suppss  7854  wfrlem14  7962  tfrlem11  8018  oacl  8154  omcl  8155  oecl  8156  oa0r  8157  om0r  8158  om1r  8163  oe1m  8165  oaordi  8166  oawordri  8170  oaass  8181  oarec  8182  omwordri  8192  odi  8199  omass  8200  oewordri  8212  oeworde  8213  oeordsuc  8214  oelim2  8215  oeoa  8217  oeoelem  8218  oeoe  8219  nnm0r  8230  nnacl  8231  nnacom  8237  nnaordi  8238  nnaass  8242  nndi  8243  nnmass  8244  nnmsucr  8245  nnmcom  8246  omabs  8268  brecop  8384  eceqoveq  8396  elpm2r  8418  map0g  8442  undifixp  8492  fundmen  8577  mapxpen  8677  mapunen  8680  php  8695  unxpdomlem2  8717  pssnn  8730  f1vrnfibi  8803  elfir  8873  wemapso2lem  9010  wdompwdom  9036  inf3lem1  9085  inf3lem3  9087  cantnfval2  9126  cantnfp1lem3  9137  r1sdom  9197  r1tr  9199  carden2a  9389  fidomtri2  9417  prdom2  9426  infxpenlem  9433  acndom  9471  fodomacn  9476  wdomfil  9481  alephon  9489  alephordi  9494  alephle  9508  alephfplem3  9526  dfac2a  9549  kmlem9  9578  cflm  9666  cfslb  9682  cfslbn  9683  infpssrlem3  9721  infpssrlem4  9722  fin23lem21  9755  fin23lem30  9758  isf34lem7  9795  isf34lem6  9796  fin67  9811  isfin7-2  9812  fin1a2lem7  9822  fin1a2lem10  9825  iundom2g  9956  konigthlem  9984  alephreg  9998  gchdomtri  10045  wunr1om  10135  tskr1om  10183  inar1  10191  grur1a  10235  indpi  10323  genpprecl  10417  genpnmax  10423  addcmpblnr  10485  recexsrlem  10519  map2psrpr  10526  ax1rid  10577  axpre-mulgt0  10584  ltle  10723  nnmulcl  11655  nnsub  11675  nn0sub  11941  nneo  12060  uz11  12261  xrltle  12536  xltnegi  12603  xrsupsslem  12694  xrinfmsslem  12695  xrub  12699  supxrunb1  12706  supxrunb2  12707  om2uzuzi  13311  uzrdgxfr  13329  seqcl2  13382  seqfveq2  13386  seqshft2  13390  seqsplit  13397  seqcaopr3  13399  seqf1olem2a  13402  seqid2  13410  seqhomo  13411  ser1const  13420  m1expcl2  13445  expadd  13465  expmul  13468  faclbnd  13644  hashfzp1  13786  hashmap  13790  hashfacen  13806  hashf1lem1  13807  hashf1lem2  13808  hashf1  13809  seqcoll  13816  wrdsymb0  13895  len0nnbi  13897  eqs1  13960  swrdnd2  14011  wrd2ind  14079  pfxccatin12lem2c  14086  pfxccatin12lem2  14087  swrdccatin1d  14099  repswccat  14142  repswcshw  14168  cshwcshid  14183  rtrclreclem3  14413  rtrclreclem4  14414  dfrtrcl2  14415  relexpindlem  14416  relexpind  14417  rtrclind  14418  recan  14690  rexanre  14700  rlimcn2  14941  caurcvg2  15028  fsumiun  15170  pwm1geoserOLD  15219  efexp  15448  rpnnen2lem12  15572  dvdstr  15640  alzdvds  15664  zob  15702  sumeven  15732  sumodd  15733  bitsinv1  15785  smu01lem  15828  smupval  15831  smueqlem  15833  smumullem  15835  seq1st  15909  lcmfunsnlem2lem1  15976  lcmfunsnlem2lem2  15977  cncongr2  16006  prmdiveq  16117  odzdvds  16126  pythagtriplem2  16148  pcexp  16190  vdwlem13  16323  ramz  16355  prmolefac  16376  elrestr  16696  xpsff1o  16834  subsubc  17117  clatl  17720  frmdgsum  18021  sursubmefmnd  18055  injsubmefmnd  18056  smndex1mndlem  18068  dfgrp3e  18193  mulgneg2  18255  mulgnnass  18256  mhmmulg  18262  gsumwrev  18488  symgextf1lem  18542  symgfixelsi  18557  pmtrdifellem4  18601  sylow1lem1  18717  efgsfo  18859  efgred  18868  cyggexb  19013  gsumzres  19023  gsum2dlem2  19085  ringadd2  19319  mulgass2  19345  lmodprop2d  19690  lspsnne2  19884  lspsneu  19889  assapropd  20095  mplcoe1  20240  mplcoe3  20241  mplcoe5  20243  ply1sclf1  20451  cnfldmulg  20571  cnfldexp  20572  zrhpsgnelbas  20732  mat1scmat  21142  restopn2  21779  cnpf2  21852  cmpfi  22010  txcn  22228  txlm  22250  xkoptsub  22256  xkopjcn  22258  ufildr  22533  cnflf  22604  fclsnei  22621  fclscmp  22632  ufilcmp  22634  cnfcf  22644  symgtgp  22708  isxms2  23052  met2ndc  23127  metustbl  23170  tngngp2  23255  clmmulg  23699  iscau4  23876  ovolunlem1a  24091  ovolicc2lem4  24115  volfiniun  24142  voliunlem1  24145  volsup  24151  dvnadd  24520  dvnres  24522  dvcobr  24537  ply1nzb  24710  plypf1  24796  dgrle  24827  coeaddlem  24833  dgrlt  24850  dvntaylp  24953  cxpmul2  25266  rlimcnp  25537  facgam  25637  wilthlem2  25640  isnsqf  25706  musum  25762  chtub  25782  chpval2  25788  gausslemma2dlem0i  25934  dchrisumlem1  26059  qabvexp  26196  ostthlem2  26198  axsegconlem1  26697  ax5seglem4  26712  ax5seglem5  26713  axlowdimlem15  26736  axcontlem2  26745  axcontlem4  26747  incistruhgr  26858  upgredg2vtx  26920  upgredgpr  26921  numedglnl  26923  uhgr2edg  26984  nbupgruvtxres  27183  cusgrfilem1  27231  wlkres  27446  wlkp1lem2  27450  pthdivtx  27504  pthdlem2lem  27542  wlkiswwlks2lem4  27644  wwlksnredwwlkn0  27668  wwlksnextwrd  27669  wwlksnfi  27678  wwlksnextprop  27685  clwlkclwwlklem2a  27770  clwlkclwwlkf1lem2  27777  erclwwlksym  27793  clwwlkf1  27822  eleclclwwlknlem2  27834  erclwwlknsym  27843  clwwlknonex2  27882  eupth2lem3lem6  28006  frgr3vlem1  28046  3vfriswmgrlem  28050  wlkl0  28140  sspval  28494  nmosetre  28535  nmobndseqi  28550  nmobndseqiALT  28551  orthcom  28879  shsva  29091  shmodsi  29160  h1datomi  29352  nmopsetretALT  29634  nmfnsetre  29648  lnopcnbd  29807  pjclem4  29970  pj3si  29978  ssmd1  30082  atom1d  30124  chjatom  30128  atcvat4i  30168  cdj3lem2a  30207  cdj3lem3a  30210  disjunsn  30338  unitdivcld  31139  xrge0iifiso  31173  dya2iocuni  31536  bnj168  31995  bnj535  32157  bnj590  32177  bnj594  32179  bnj938  32204  bnj1118  32251  bnj1128  32257  deranglem  32408  subfacp1lem6  32427  subfacval2  32429  cvmlift2lem12  32556  satffun  32651  mrsubvrs  32764  msrrcl  32785  mclsax  32811  dfon2lem6  33028  rdgprc  33034  trpredlem1  33061  nodenselem8  33190  slerec  33272  ifscgr  33500  btwncolinear1  33525  hfelhf  33637  opnrebl2  33664  nn0prpw  33666  ordcmp  33790  findreccl  33796  nndivlub  33801  bj-rest0  34378  bj-isrvec2  34575  topdifinffinlem  34622  iooelexlt  34637  rdgeqoa  34645  exrecfnlem  34654  wl-mo3t  34806  matunitlindflem2  34883  poimirlem2  34888  poimirlem23  34909  poimirlem28  34914  poimirlem29  34915  poimirlem31  34917  poimirlem32  34918  eqfnun  34991  sdclem2  35011  sdclem1  35012  prdsbnd2  35067  ismtyval  35072  rrnequiv  35107  isexid2  35127  ismndo1  35145  exidreslem  35149  rngo2  35179  rngoueqz  35212  risci  35259  prtlem11  35996  prtlem15  36005  cvrat4  36573  lcfl6  38630  harval3  39897  clcnvlem  39976  cnvrcl0  39978  cnvtrcl0  39979  iunrelexpmin1  40046  iunrelexpmin2  40050  aovmpt4g  43394  elsetpreimafvbi  43545  iccpartiltu  43576  iccpartgt  43581  iccpartgel  43583  reuopreuprim  43682  fmtnofac1  43726  gbepos  43917  funcrngcsetc  44263  funcrngcsetcALT  44264  rhmsscrnghm  44291  funcringcsetc  44300  ellcoellss  44484  dignn0flhalflem2  44670  nn0sumshdiglemB  44674