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  2469  pm2.61ne  3102  unineq  4254  elpreqprlem  4796  oteqex  5390  elopabr  5447  otel3xp  5599  eqrelrdv2  5668  breldmg  5778  elrnmpt1  5830  cnveqb  6053  cnveq0  6054  predpoirr  6176  predfrirr  6177  limelon  6254  f1ssf1  6646  ndmfv  6700  ffvresb  6888  isomin  7090  isofrlem  7093  oprabidw  7187  caovord3d  7358  eldifpw  7490  ssonuni  7501  onsucuni2  7549  ordzsl  7560  tfindsg  7575  findsg  7609  oteqimp  7708  frxp  7820  poxp  7822  fnwelem  7825  suppss  7860  wfrlem14  7968  tfrlem11  8024  oacl  8160  omcl  8161  oecl  8162  oa0r  8163  om0r  8164  om1r  8169  oe1m  8171  oaordi  8172  oawordri  8176  oaass  8187  oarec  8188  omwordri  8198  odi  8205  omass  8206  oewordri  8218  oeworde  8219  oeordsuc  8220  oelim2  8221  oeoa  8223  oeoelem  8224  oeoe  8225  nnm0r  8236  nnacl  8237  nnacom  8243  nnaordi  8244  nnaass  8248  nndi  8249  nnmass  8250  nnmsucr  8251  nnmcom  8252  omabs  8274  brecop  8390  eceqoveq  8402  elpm2r  8424  map0g  8448  undifixp  8498  fundmen  8583  mapxpen  8683  mapunen  8686  php  8701  unxpdomlem2  8723  pssnn  8736  f1vrnfibi  8809  elfir  8879  wemapso2lem  9016  wdompwdom  9042  inf3lem1  9091  inf3lem3  9093  cantnfval2  9132  cantnfp1lem3  9143  r1sdom  9203  r1tr  9205  carden2a  9395  fidomtri2  9423  prdom2  9432  infxpenlem  9439  acndom  9477  fodomacn  9482  wdomfil  9487  alephon  9495  alephordi  9500  alephle  9514  alephfplem3  9532  dfac2a  9555  kmlem9  9584  cflm  9672  cfslb  9688  cfslbn  9689  infpssrlem3  9727  infpssrlem4  9728  fin23lem21  9761  fin23lem30  9764  isf34lem7  9801  isf34lem6  9802  fin67  9817  isfin7-2  9818  fin1a2lem7  9828  fin1a2lem10  9831  iundom2g  9962  konigthlem  9990  alephreg  10004  gchdomtri  10051  wunr1om  10141  tskr1om  10189  inar1  10197  grur1a  10241  indpi  10329  genpprecl  10423  genpnmax  10429  addcmpblnr  10491  recexsrlem  10525  map2psrpr  10532  ax1rid  10583  axpre-mulgt0  10590  ltle  10729  nnmulcl  11662  nnsub  11682  nn0sub  11948  nneo  12067  uz11  12268  xrltle  12543  xltnegi  12610  xrsupsslem  12701  xrinfmsslem  12702  xrub  12706  supxrunb1  12713  supxrunb2  12714  om2uzuzi  13318  uzrdgxfr  13336  seqcl2  13389  seqfveq2  13393  seqshft2  13397  seqsplit  13404  seqcaopr3  13406  seqf1olem2a  13409  seqid2  13417  seqhomo  13418  ser1const  13427  m1expcl2  13452  expadd  13472  expmul  13475  faclbnd  13651  hashfzp1  13793  hashmap  13797  hashfacen  13813  hashf1lem1  13814  hashf1lem2  13815  hashf1  13816  seqcoll  13823  wrdsymb0  13901  len0nnbi  13903  eqs1  13966  swrdnd2  14017  wrd2ind  14085  pfxccatin12lem2c  14092  pfxccatin12lem2  14093  swrdccatin1d  14105  repswccat  14148  repswcshw  14174  cshwcshid  14189  rtrclreclem3  14419  rtrclreclem4  14420  dfrtrcl2  14421  relexpindlem  14422  relexpind  14423  rtrclind  14424  recan  14696  rexanre  14706  rlimcn2  14947  caurcvg2  15034  fsumiun  15176  pwm1geoserOLD  15225  efexp  15454  rpnnen2lem12  15578  dvdstr  15646  alzdvds  15670  zob  15708  sumeven  15738  sumodd  15739  bitsinv1  15791  smu01lem  15834  smupval  15837  smueqlem  15839  smumullem  15841  seq1st  15915  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  cncongr2  16012  prmdiveq  16123  odzdvds  16132  pythagtriplem2  16154  pcexp  16196  vdwlem13  16329  ramz  16361  prmolefac  16382  elrestr  16702  xpsff1o  16840  subsubc  17123  clatl  17726  frmdgsum  18027  sursubmefmnd  18061  injsubmefmnd  18062  smndex1mndlem  18074  dfgrp3e  18199  mulgneg2  18261  mulgnnass  18262  mhmmulg  18268  gsumwrev  18494  symgextf1lem  18548  symgfixelsi  18563  pmtrdifellem4  18607  sylow1lem1  18723  efgsfo  18865  efgred  18874  cyggexb  19019  gsumzres  19029  gsum2dlem2  19091  ringadd2  19325  mulgass2  19351  lmodprop2d  19696  lspsnne2  19890  lspsneu  19895  assapropd  20101  mplcoe1  20246  mplcoe3  20247  mplcoe5  20249  ply1sclf1  20457  cnfldmulg  20577  cnfldexp  20578  zrhpsgnelbas  20738  mat1scmat  21148  restopn2  21785  cnpf2  21858  cmpfi  22016  txcn  22234  txlm  22256  xkoptsub  22262  xkopjcn  22264  ufildr  22539  cnflf  22610  fclsnei  22627  fclscmp  22638  ufilcmp  22640  cnfcf  22650  symgtgp  22714  isxms2  23058  met2ndc  23133  metustbl  23176  tngngp2  23261  clmmulg  23705  iscau4  23882  ovolunlem1a  24097  ovolicc2lem4  24121  volfiniun  24148  voliunlem1  24151  volsup  24157  dvnadd  24526  dvnres  24528  dvcobr  24543  ply1nzb  24716  plypf1  24802  dgrle  24833  coeaddlem  24839  dgrlt  24856  dvntaylp  24959  cxpmul2  25272  rlimcnp  25543  facgam  25643  wilthlem2  25646  isnsqf  25712  musum  25768  chtub  25788  chpval2  25794  gausslemma2dlem0i  25940  dchrisumlem1  26065  qabvexp  26202  ostthlem2  26204  axsegconlem1  26703  ax5seglem4  26718  ax5seglem5  26719  axlowdimlem15  26742  axcontlem2  26751  axcontlem4  26753  incistruhgr  26864  upgredg2vtx  26926  upgredgpr  26927  numedglnl  26929  uhgr2edg  26990  nbupgruvtxres  27189  cusgrfilem1  27237  wlkres  27452  wlkp1lem2  27456  pthdivtx  27510  pthdlem2lem  27548  wlkiswwlks2lem4  27650  wwlksnredwwlkn0  27674  wwlksnextwrd  27675  wwlksnfi  27684  wwlksnextprop  27691  clwlkclwwlklem2a  27776  clwlkclwwlkf1lem2  27783  erclwwlksym  27799  clwwlkf1  27828  eleclclwwlknlem2  27840  erclwwlknsym  27849  clwwlknonex2  27888  eupth2lem3lem6  28012  frgr3vlem1  28052  3vfriswmgrlem  28056  wlkl0  28146  sspval  28500  nmosetre  28541  nmobndseqi  28556  nmobndseqiALT  28557  orthcom  28885  shsva  29097  shmodsi  29166  h1datomi  29358  nmopsetretALT  29640  nmfnsetre  29654  lnopcnbd  29813  pjclem4  29976  pj3si  29984  ssmd1  30088  atom1d  30130  chjatom  30134  atcvat4i  30174  cdj3lem2a  30213  cdj3lem3a  30216  disjunsn  30344  unitdivcld  31144  xrge0iifiso  31178  dya2iocuni  31541  bnj168  32000  bnj535  32162  bnj590  32182  bnj594  32184  bnj938  32209  bnj1118  32256  bnj1128  32262  deranglem  32413  subfacp1lem6  32432  subfacval2  32434  cvmlift2lem12  32561  satffun  32656  mrsubvrs  32769  msrrcl  32790  mclsax  32816  dfon2lem6  33033  rdgprc  33039  trpredlem1  33066  nodenselem8  33195  slerec  33277  ifscgr  33505  btwncolinear1  33530  hfelhf  33642  opnrebl2  33669  nn0prpw  33671  ordcmp  33795  findreccl  33801  nndivlub  33806  bj-rest0  34387  bj-isrvec2  34584  topdifinffinlem  34631  iooelexlt  34646  rdgeqoa  34654  exrecfnlem  34663  wl-mo3t  34827  matunitlindflem2  34904  poimirlem2  34909  poimirlem23  34930  poimirlem28  34935  poimirlem29  34936  poimirlem31  34938  poimirlem32  34939  eqfnun  35012  sdclem2  35032  sdclem1  35033  prdsbnd2  35088  ismtyval  35093  rrnequiv  35128  isexid2  35148  ismndo1  35166  exidreslem  35170  rngo2  35200  rngoueqz  35233  risci  35280  prtlem11  36017  prtlem15  36026  cvrat4  36594  lcfl6  38651  harval3  39924  clcnvlem  40003  cnvrcl0  40005  cnvtrcl0  40006  iunrelexpmin1  40073  iunrelexpmin2  40077  aovmpt4g  43420  elsetpreimafvbi  43571  iccpartiltu  43602  iccpartgt  43607  iccpartgel  43609  reuopreuprim  43708  fmtnofac1  43752  gbepos  43943  funcrngcsetc  44289  funcrngcsetcALT  44290  rhmsscrnghm  44317  funcringcsetc  44326  ellcoellss  44510  dignn0flhalflem2  44696  nn0sumshdiglemB  44700