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  2458  pm2.61ne  3072  unineq  4204  elpreqprlem  4756  oteqex  5355  elopabr  5412  otel3xp  5563  eqrelrdv2  5632  breldmg  5742  elrnmpt1  5794  cnveqb  6020  cnveq0  6021  predpoirr  6144  predfrirr  6145  limelon  6222  f1ssf1  6621  ndmfv  6675  ffvresb  6865  isomin  7069  isofrlem  7072  oprabidw  7166  caovord3d  7338  eldifpw  7470  ssonuni  7481  onsucuni2  7529  ordzsl  7540  tfindsg  7555  findsg  7590  oteqimp  7690  frxp  7803  poxp  7805  fnwelem  7808  suppss  7843  wfrlem14  7951  tfrlem11  8007  oacl  8143  omcl  8144  oecl  8145  oa0r  8146  om0r  8147  om1r  8152  oe1m  8154  oaordi  8155  oawordri  8159  oaass  8170  oarec  8171  omwordri  8181  odi  8188  omass  8189  oewordri  8201  oeworde  8202  oeordsuc  8203  oelim2  8204  oeoa  8206  oeoelem  8207  oeoe  8208  nnm0r  8219  nnacl  8220  nnacom  8226  nnaordi  8227  nnaass  8231  nndi  8232  nnmass  8233  nnmsucr  8234  nnmcom  8235  omabs  8257  brecop  8373  eceqoveq  8385  elpm2r  8407  map0g  8431  undifixp  8481  fundmen  8566  mapxpen  8667  mapunen  8670  php  8685  unxpdomlem2  8707  pssnn  8720  f1vrnfibi  8793  elfir  8863  wemapso2lem  9000  wdompwdom  9026  inf3lem1  9075  inf3lem3  9077  cantnfval2  9116  cantnfp1lem3  9127  r1sdom  9187  r1tr  9189  carden2a  9379  fidomtri2  9407  prdom2  9417  infxpenlem  9424  acndom  9462  fodomacn  9467  wdomfil  9472  alephon  9480  alephordi  9485  alephle  9499  alephfplem3  9517  dfac2a  9540  kmlem9  9569  cflm  9661  cfslb  9677  cfslbn  9678  infpssrlem3  9716  infpssrlem4  9717  fin23lem21  9750  fin23lem30  9753  isf34lem7  9790  isf34lem6  9791  fin67  9806  isfin7-2  9807  fin1a2lem7  9817  fin1a2lem10  9820  iundom2g  9951  konigthlem  9979  alephreg  9993  gchdomtri  10040  wunr1om  10130  tskr1om  10178  inar1  10186  grur1a  10230  indpi  10318  genpprecl  10412  genpnmax  10418  addcmpblnr  10480  recexsrlem  10514  map2psrpr  10521  ax1rid  10572  axpre-mulgt0  10579  ltle  10718  nnmulcl  11649  nnsub  11669  nn0sub  11935  nneo  12054  uz11  12255  xrltle  12530  xltnegi  12597  xrsupsslem  12688  xrinfmsslem  12689  xrub  12693  supxrunb1  12700  supxrunb2  12701  om2uzuzi  13312  uzrdgxfr  13330  seqcl2  13384  seqfveq2  13388  seqshft2  13392  seqsplit  13399  seqcaopr3  13401  seqf1olem2a  13404  seqid2  13412  seqhomo  13413  ser1const  13422  m1expcl2  13447  expadd  13467  expmul  13470  faclbnd  13646  hashfzp1  13788  hashmap  13792  hashfacen  13808  hashf1lem1  13809  hashf1lem2  13810  hashf1  13811  seqcoll  13818  wrdsymb0  13892  len0nnbi  13894  eqs1  13957  swrdnd2  14008  wrd2ind  14076  pfxccatin12lem2c  14083  pfxccatin12lem2  14084  swrdccatin1d  14096  repswccat  14139  repswcshw  14165  cshwcshid  14180  rtrclreclem3  14411  rtrclreclem4  14412  dfrtrcl2  14413  relexpindlem  14414  relexpind  14415  rtrclind  14416  recan  14688  rexanre  14698  rlimcn2  14939  caurcvg2  15026  fsumiun  15168  pwm1geoserOLD  15217  efexp  15446  rpnnen2lem12  15570  dvdstr  15638  alzdvds  15662  zob  15700  sumeven  15728  sumodd  15729  bitsinv1  15781  smu01lem  15824  smupval  15827  smueqlem  15829  smumullem  15831  seq1st  15905  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  cncongr2  16002  prmdiveq  16113  odzdvds  16122  pythagtriplem2  16144  pcexp  16186  vdwlem13  16319  ramz  16351  prmolefac  16372  elrestr  16694  xpsff1o  16832  subsubc  17115  clatl  17718  frmdgsum  18019  sursubmefmnd  18053  injsubmefmnd  18054  smndex1mndlem  18066  dfgrp3e  18191  mulgneg2  18253  mulgnnass  18254  mhmmulg  18260  gsumwrev  18486  symgextf1lem  18540  symgfixelsi  18555  pmtrdifellem4  18599  sylow1lem1  18715  efgsfo  18857  efgred  18866  cyggexb  19012  gsumzres  19022  gsum2dlem2  19084  ringadd2  19321  mulgass2  19347  lmodprop2d  19689  lspsnne2  19883  lspsneu  19888  cnfldmulg  20123  cnfldexp  20124  zrhpsgnelbas  20283  assapropd  20558  mplcoe1  20705  mplcoe3  20706  mplcoe5  20708  mhpvarcl  20798  ply1sclf1  20918  mat1scmat  21144  restopn2  21782  cnpf2  21855  cmpfi  22013  txcn  22231  txlm  22253  xkoptsub  22259  xkopjcn  22261  ufildr  22536  cnflf  22607  fclsnei  22624  fclscmp  22635  ufilcmp  22637  cnfcf  22647  symgtgp  22711  isxms2  23055  met2ndc  23130  metustbl  23173  tngngp2  23258  clmmulg  23706  iscau4  23883  ovolunlem1a  24100  ovolicc2lem4  24124  volfiniun  24151  voliunlem1  24154  volsup  24160  dvnadd  24532  dvnres  24534  dvcobr  24549  ply1nzb  24723  plypf1  24809  dgrle  24840  coeaddlem  24846  dgrlt  24863  dvntaylp  24966  cxpmul2  25280  rlimcnp  25551  facgam  25651  wilthlem2  25654  isnsqf  25720  musum  25776  chtub  25796  chpval2  25802  gausslemma2dlem0i  25948  dchrisumlem1  26073  qabvexp  26210  ostthlem2  26212  axsegconlem1  26711  ax5seglem4  26726  ax5seglem5  26727  axlowdimlem15  26750  axcontlem2  26759  axcontlem4  26761  incistruhgr  26872  upgredg2vtx  26934  upgredgpr  26935  numedglnl  26937  uhgr2edg  26998  nbupgruvtxres  27197  cusgrfilem1  27245  wlkres  27460  wlkp1lem2  27464  pthdivtx  27518  pthdlem2lem  27556  wlkiswwlks2lem4  27658  wwlksnredwwlkn0  27682  wwlksnextwrd  27683  wwlksnfi  27692  wwlksnextprop  27698  clwlkclwwlklem2a  27783  clwlkclwwlkf1lem2  27790  erclwwlksym  27806  clwwlkf1  27834  eleclclwwlknlem2  27846  erclwwlknsym  27855  clwwlknonex2  27894  eupth2lem3lem6  28018  frgr3vlem1  28058  3vfriswmgrlem  28062  wlkl0  28152  sspval  28506  nmosetre  28547  nmobndseqi  28562  nmobndseqiALT  28563  orthcom  28891  shsva  29103  shmodsi  29172  h1datomi  29364  nmopsetretALT  29646  nmfnsetre  29660  lnopcnbd  29819  pjclem4  29982  pj3si  29990  ssmd1  30094  atom1d  30136  chjatom  30140  atcvat4i  30180  cdj3lem2a  30219  cdj3lem3a  30222  disjunsn  30357  unitdivcld  31254  xrge0iifiso  31288  dya2iocuni  31651  bnj168  32110  bnj535  32272  bnj590  32292  bnj594  32294  bnj938  32319  bnj1118  32366  bnj1128  32372  fnrelpredd  32472  deranglem  32526  subfacp1lem6  32545  subfacval2  32547  cvmlift2lem12  32674  satffun  32769  mrsubvrs  32882  msrrcl  32903  mclsax  32929  dfon2lem6  33146  rdgprc  33152  trpredlem1  33179  nodenselem8  33308  slerec  33390  ifscgr  33618  btwncolinear1  33643  hfelhf  33755  opnrebl2  33782  nn0prpw  33784  ordcmp  33908  findreccl  33914  nndivlub  33919  bj-rest0  34508  bj-isrvec2  34714  topdifinffinlem  34764  iooelexlt  34779  rdgeqoa  34787  exrecfnlem  34796  wl-mo3t  34977  matunitlindflem2  35054  poimirlem2  35059  poimirlem23  35080  poimirlem28  35085  poimirlem29  35086  poimirlem31  35088  poimirlem32  35089  eqfnun  35160  sdclem2  35180  sdclem1  35181  prdsbnd2  35233  ismtyval  35238  rrnequiv  35273  isexid2  35293  ismndo1  35311  exidreslem  35315  rngo2  35345  rngoueqz  35378  risci  35425  prtlem11  36162  prtlem15  36171  cvrat4  36739  lcfl6  38796  harval3  40244  clcnvlem  40323  cnvrcl0  40325  cnvtrcl0  40326  iunrelexpmin1  40409  iunrelexpmin2  40413  aovmpt4g  43757  elsetpreimafvbi  43908  iccpartiltu  43939  iccpartgt  43944  iccpartgel  43946  reuopreuprim  44043  fmtnofac1  44087  gbepos  44276  funcrngcsetc  44622  funcrngcsetcALT  44623  rhmsscrnghm  44650  funcringcsetc  44659  ellcoellss  44844  dignn0flhalflem2  45030  nn0sumshdiglemB  45034  1arympt1  45052