Theorem syl5ibr 249

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  syl5ibrcom  250  biimprd  251  exdistrf  2447  pm2.61ne  3019  unineq  4168  elpreqprlem  4751  oteqex  5357  elopabr  5415  otel3xp  5569  eqrelrdv2  5639  breldmg  5752  elrnmpt1  5801  cnveqb  6028  cnveq0  6029  predpoirr  6157  predfrirr  6158  limelon  6235  f1ssf1  6649  ndmfv  6704  ffvresb  6898  isomin  7103  isofrlem  7106  oprabidw  7201  caovord3d  7374  eldifpw  7509  ssonuni  7520  onsucuni2  7568  ordzsl  7579  tfindsg  7594  findsg  7630  oteqimp  7733  frxp  7846  poxp  7848  fnwelem  7851  suppssOLD  7890  wfrlem14  7997  tfrlem11  8053  oacl  8191  omcl  8192  oecl  8193  oa0r  8194  om0r  8195  om1r  8200  oe1m  8202  oaordi  8203  oawordri  8207  oaass  8218  oarec  8219  omwordri  8229  odi  8236  omass  8237  oewordri  8249  oeworde  8250  oeordsuc  8251  oelim2  8252  oeoa  8254  oeoelem  8255  oeoe  8256  nnm0r  8267  nnacl  8268  nnacom  8274  nnaordi  8275  nnaass  8279  nndi  8280  nnmass  8281  nnmsucr  8282  nnmcom  8283  omabs  8305  brecop  8421  eceqoveq  8433  elpm2r  8455  map0g  8494  undifixp  8544  fundmen  8630  mapxpen  8733  mapunen  8736  php  8751  pssnn  8767  unxpdomlem2  8802  pssnnOLD  8815  f1vrnfibi  8882  elfir  8952  wemapso2lem  9089  wdompwdom  9115  inf3lem1  9164  inf3lem3  9166  cantnfval2  9205  cantnfp1lem3  9216  r1sdom  9276  r1tr  9278  carden2a  9468  fidomtri2  9496  prdom2  9506  infxpenlem  9513  acndom  9551  fodomacn  9556  wdomfil  9561  alephon  9569  alephordi  9574  alephle  9588  alephfplem3  9606  dfac2a  9629  kmlem9  9658  cflm  9750  cfslb  9766  cfslbn  9767  infpssrlem3  9805  infpssrlem4  9806  fin23lem21  9839  fin23lem30  9842  isf34lem7  9879  isf34lem6  9880  fin67  9895  isfin7-2  9896  fin1a2lem7  9906  fin1a2lem10  9909  iundom2g  10040  konigthlem  10068  alephreg  10082  gchdomtri  10129  wunr1om  10219  tskr1om  10267  inar1  10275  grur1a  10319  indpi  10407  genpprecl  10501  genpnmax  10507  addcmpblnr  10569  recexsrlem  10603  map2psrpr  10610  ax1rid  10661  axpre-mulgt0  10668  ltle  10807  nnmulcl  11740  nnsub  11760  nn0sub  12026  nneo  12147  uz11  12349  xrltle  12625  xltnegi  12692  xrsupsslem  12783  xrinfmsslem  12784  xrub  12788  supxrunb1  12795  supxrunb2  12796  om2uzuzi  13408  uzrdgxfr  13426  seqcl2  13480  seqfveq2  13484  seqshft2  13488  seqsplit  13495  seqcaopr3  13497  seqf1olem2a  13500  seqid2  13508  seqhomo  13509  ser1const  13518  m1expcl2  13543  expadd  13563  expmul  13566  faclbnd  13742  hashfzp1  13884  hashmap  13888  hashfacenOLD  13905  hashf1lem1OLD  13907  hashf1lem2  13908  hashf1  13909  seqcoll  13916  wrdsymb0  13990  len0nnbi  13992  eqs1  14055  swrdnd2  14106  wrd2ind  14174  pfxccatin12lem2c  14181  pfxccatin12lem2  14182  swrdccatin1d  14194  repswccat  14237  repswcshw  14263  cshwcshid  14278  rtrclreclem3  14509  rtrclreclem4  14510  dfrtrcl2  14511  relexpindlem  14512  relexpind  14513  rtrclind  14514  recan  14786  rexanre  14796  rlimcn3  15037  caurcvg2  15127  fsumiun  15269  efexp  15546  rpnnen2lem12  15670  dvdstr  15739  alzdvds  15765  zob  15804  sumeven  15832  sumodd  15833  bitsinv1  15885  smu01lem  15928  smupval  15931  smueqlem  15933  smumullem  15935  seq1st  16012  lcmfunsnlem2lem1  16079  lcmfunsnlem2lem2  16080  cncongr2  16109  prmdiveq  16223  odzdvds  16232  pythagtriplem2  16254  pcexp  16296  vdwlem13  16429  ramz  16461  prmolefac  16482  elrestr  16805  xpsff1o  16943  subsubc  17228  clatl  17842  frmdgsum  18143  sursubmefmnd  18177  injsubmefmnd  18178  smndex1mndlem  18190  dfgrp3e  18317  mulgneg2  18379  mulgnnass  18380  mhmmulg  18386  gsumwrev  18612  symgextf1lem  18666  symgfixelsi  18681  pmtrdifellem4  18725  sylow1lem1  18841  efgsfo  18983  efgred  18992  cyggexb  19138  gsumzres  19148  gsum2dlem2  19210  ringadd2  19447  mulgass2  19473  lmodprop2d  19815  lspsnne2  20009  lspsneu  20014  cnfldmulg  20249  cnfldexp  20250  zrhpsgnelbas  20410  assapropd  20685  mplcoe1  20848  mplcoe3  20849  mplcoe5  20851  mhpvarcl  20942  ply1sclf1  21064  mat1scmat  21290  restopn2  21928  cnpf2  22001  cmpfi  22159  txcn  22377  txlm  22399  xkoptsub  22405  xkopjcn  22407  ufildr  22682  cnflf  22753  fclsnei  22770  fclscmp  22781  ufilcmp  22783  cnfcf  22793  symgtgp  22857  isxms2  23201  met2ndc  23276  metustbl  23319  tngngp2  23405  clmmulg  23853  iscau4  24031  ovolunlem1a  24248  ovolicc2lem4  24272  volfiniun  24299  voliunlem1  24302  volsup  24308  dvnadd  24681  dvnres  24683  dvcobr  24698  ply1nzb  24875  plypf1  24961  dgrle  24992  coeaddlem  24998  dgrlt  25015  dvntaylp  25118  cxpmul2  25432  rlimcnp  25703  facgam  25803  wilthlem2  25806  isnsqf  25872  musum  25928  chtub  25948  chpval2  25954  gausslemma2dlem0i  26100  dchrisumlem1  26225  qabvexp  26362  ostthlem2  26364  axsegconlem1  26863  ax5seglem4  26878  ax5seglem5  26879  axlowdimlem15  26902  axcontlem2  26911  axcontlem4  26913  incistruhgr  27024  upgredg2vtx  27086  upgredgpr  27087  numedglnl  27089  uhgr2edg  27150  nbupgruvtxres  27349  cusgrfilem1  27397  wlkres  27612  wlkp1lem2  27616  pthdivtx  27670  pthdlem2lem  27708  wlkiswwlks2lem4  27810  wwlksnredwwlkn0  27834  wwlksnextwrd  27835  wwlksnfi  27844  wwlksnextprop  27850  clwlkclwwlklem2a  27935  clwlkclwwlkf1lem2  27942  erclwwlksym  27958  clwwlkf1  27986  eleclclwwlknlem2  27998  erclwwlknsym  28007  clwwlknonex2  28046  eupth2lem3lem6  28170  frgr3vlem1  28210  3vfriswmgrlem  28214  wlkl0  28304  sspval  28658  nmosetre  28699  nmobndseqi  28714  nmobndseqiALT  28715  orthcom  29043  shsva  29255  shmodsi  29324  h1datomi  29516  nmopsetretALT  29798  nmfnsetre  29812  lnopcnbd  29971  pjclem4  30134  pj3si  30142  ssmd1  30246  atom1d  30288  chjatom  30292  atcvat4i  30332  cdj3lem2a  30371  cdj3lem3a  30374  disjunsn  30507  unitdivcld  31423  xrge0iifiso  31457  dya2iocuni  31820  bnj168  32279  bnj535  32441  bnj590  32461  bnj594  32463  bnj938  32488  bnj1118  32535  bnj1128  32541  fnrelpredd  32632  deranglem  32699  subfacp1lem6  32718  subfacval2  32720  cvmlift2lem12  32847  satffun  32942  mrsubvrs  33055  msrrcl  33076  mclsax  33102  dfon2lem6  33336  rdgprc  33342  trpredlem1  33369  nodenselem8  33535  slerec  33654  bday1s  33666  ssltleft  33691  ssltright  33692  ifscgr  33984  btwncolinear1  34009  hfelhf  34121  opnrebl2  34148  nn0prpw  34150  ordcmp  34274  findreccl  34280  nndivlub  34285  bj-rest0  34885  bj-isrvec2  35091  topdifinffinlem  35141  iooelexlt  35156  rdgeqoa  35164  exrecfnlem  35173  wl-mo3t  35354  matunitlindflem2  35397  poimirlem2  35402  poimirlem23  35423  poimirlem28  35428  poimirlem29  35429  poimirlem31  35431  poimirlem32  35432  eqfnun  35503  sdclem2  35523  sdclem1  35524  prdsbnd2  35576  ismtyval  35581  rrnequiv  35616  isexid2  35636  ismndo1  35654  exidreslem  35658  rngo2  35688  rngoueqz  35721  risci  35768  prtlem11  36503  prtlem15  36512  cvrat4  37080  lcfl6  39137  dvdsexpnn0  39918  harval3  40697  clcnvlem  40776  cnvrcl0  40778  cnvtrcl0  40779  iunrelexpmin1  40862  iunrelexpmin2  40866  aovmpt4g  44226  elsetpreimafvbi  44377  iccpartiltu  44408  iccpartgt  44413  iccpartgel  44415  reuopreuprim  44512  fmtnofac1  44556  gbepos  44744  funcrngcsetc  45090  funcrngcsetcALT  45091  rhmsscrnghm  45118  funcringcsetc  45127  ellcoellss  45310  dignn0flhalflem2  45496  nn0sumshdiglemB  45500  1arympt1  45518