Theorem syl5ibr 245

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 243	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  246  biimprd  247  exdistrf  2448  pm2.61ne  3031  unineq  4216  elpreqprlem  4801  oteqex  5416  elopabr  5474  otel3xp  5632  eqrelrdv2  5702  breldmg  5815  elrnmpt1  5864  cnveqb  6096  cnveq0  6097  predpoirr  6233  predfrirr  6234  limelon  6326  f1ssf1  6743  ndmfv  6798  ffvresb  6992  isomin  7201  isofrlem  7204  oprabidw  7299  caovord3d  7473  eldifpw  7609  ssonuni  7620  onsucuni2  7669  ordzsl  7680  tfindsg  7695  findsg  7733  oteqimp  7836  frxp  7951  poxp  7953  fnwelem  7956  suppssOLD  7995  wfrlem14OLD  8137  tfrlem11  8203  oacl  8341  omcl  8342  oecl  8343  oa0r  8344  om0r  8345  om1r  8350  oe1m  8352  oaordi  8353  oawordri  8357  oaass  8368  oarec  8369  omwordri  8379  odi  8386  omass  8387  oewordri  8399  oeworde  8400  oeordsuc  8401  oelim2  8402  oeoa  8404  oeoelem  8405  oeoe  8406  nnm0r  8417  nnacl  8418  nnacom  8424  nnaordi  8425  nnaass  8429  nndi  8430  nnmass  8431  nnmsucr  8432  nnmcom  8433  omabs  8455  brecop  8573  eceqoveq  8585  elpm2r  8607  map0g  8646  undifixp  8696  fundmen  8791  mapxpen  8895  mapunen  8898  pssnn  8916  php  8957  phpOLD  8970  unxpdomlem2  8989  pssnnOLD  9001  f1vrnfibi  9065  elfir  9135  wemapso2lem  9272  wdompwdom  9298  inf3lem1  9347  inf3lem3  9349  cantnfval2  9388  cantnfp1lem3  9399  trpredlem1  9457  r1sdom  9516  r1tr  9518  carden2a  9708  fidomtri2  9736  prdom2  9746  infxpenlem  9753  acndom  9791  fodomacn  9796  wdomfil  9801  alephon  9809  alephordi  9814  alephle  9828  alephfplem3  9846  dfac2a  9869  kmlem9  9898  cflm  9990  cfslb  10006  cfslbn  10007  infpssrlem3  10045  infpssrlem4  10046  fin23lem21  10079  fin23lem30  10082  isf34lem7  10119  isf34lem6  10120  fin67  10135  isfin7-2  10136  fin1a2lem7  10146  fin1a2lem10  10149  iundom2g  10280  konigthlem  10308  alephreg  10322  gchdomtri  10369  wunr1om  10459  tskr1om  10507  inar1  10515  grur1a  10559  indpi  10647  genpprecl  10741  genpnmax  10747  addcmpblnr  10809  recexsrlem  10843  map2psrpr  10850  ax1rid  10901  axpre-mulgt0  10908  ltle  11047  nnmulcl  11980  nnsub  12000  nn0sub  12266  nneo  12387  uz11  12589  xrltle  12865  xltnegi  12932  xrsupsslem  13023  xrinfmsslem  13024  xrub  13028  supxrunb1  13035  supxrunb2  13036  om2uzuzi  13650  uzrdgxfr  13668  seqcl2  13722  seqfveq2  13726  seqshft2  13730  seqsplit  13737  seqcaopr3  13739  seqf1olem2a  13742  seqid2  13750  seqhomo  13751  ser1const  13760  m1expcl2  13785  expadd  13806  expmul  13809  faclbnd  13985  hashfzp1  14127  hashmap  14131  hashfacenOLD  14148  hashf1lem1OLD  14150  hashf1lem2  14151  hashf1  14152  seqcoll  14159  wrdsymb0  14233  len0nnbi  14235  eqs1  14298  swrdnd2  14349  wrd2ind  14417  pfxccatin12lem2c  14424  pfxccatin12lem2  14425  swrdccatin1d  14437  repswccat  14480  repswcshw  14506  cshwcshid  14521  rtrclreclem3  14752  rtrclreclem4  14753  dfrtrcl2  14754  relexpindlem  14755  relexpind  14756  rtrclind  14757  recan  15029  rexanre  15039  rlimcn3  15280  caurcvg2  15370  fsumiun  15514  efexp  15791  rpnnen2lem12  15915  dvdstr  15984  alzdvds  16010  zob  16049  sumeven  16077  sumodd  16078  bitsinv1  16130  smu01lem  16173  smupval  16176  smueqlem  16178  smumullem  16180  seq1st  16257  lcmfunsnlem2lem1  16324  lcmfunsnlem2lem2  16325  cncongr2  16354  prmdiveq  16468  odzdvds  16477  pythagtriplem2  16499  pcexp  16541  vdwlem13  16675  ramz  16707  prmolefac  16728  elrestr  17120  xpsff1o  17259  subsubc  17549  clatl  18207  frmdgsum  18482  sursubmefmnd  18516  injsubmefmnd  18517  smndex1mndlem  18529  dfgrp3e  18656  mulgneg2  18718  mulgnnass  18719  mhmmulg  18725  gsumwrev  18954  symgextf1lem  19009  symgfixelsi  19024  pmtrdifellem4  19068  sylow1lem1  19184  efgsfo  19326  efgred  19335  cyggexb  19481  gsumzres  19491  gsum2dlem2  19553  ringadd2  19795  mulgass2  19821  lmodprop2d  20166  lspsnne2  20361  lspsneu  20366  cnfldmulg  20611  cnfldexp  20612  zrhpsgnelbas  20780  assapropd  21057  mplcoe1  21219  mplcoe3  21220  mplcoe5  21222  mhpvarcl  21319  ply1sclf1  21441  mat1scmat  21669  restopn2  22309  cnpf2  22382  cmpfi  22540  txcn  22758  txlm  22780  xkoptsub  22786  xkopjcn  22788  ufildr  23063  cnflf  23134  fclsnei  23151  fclscmp  23162  ufilcmp  23164  cnfcf  23174  symgtgp  23238  isxms2  23582  met2ndc  23660  metustbl  23703  tngngp2  23797  clmmulg  24245  iscau4  24424  ovolunlem1a  24641  ovolicc2lem4  24665  volfiniun  24692  voliunlem1  24695  volsup  24701  dvnadd  25074  dvnres  25076  dvcobr  25091  ply1nzb  25268  plypf1  25354  dgrle  25385  coeaddlem  25391  dgrlt  25408  dvntaylp  25511  cxpmul2  25825  rlimcnp  26096  facgam  26196  wilthlem2  26199  isnsqf  26265  musum  26321  chtub  26341  chpval2  26347  gausslemma2dlem0i  26493  dchrisumlem1  26618  qabvexp  26755  ostthlem2  26757  axsegconlem1  27266  ax5seglem4  27281  ax5seglem5  27282  axlowdimlem15  27305  axcontlem2  27314  axcontlem4  27316  incistruhgr  27430  upgredg2vtx  27492  upgredgpr  27493  numedglnl  27495  uhgr2edg  27556  nbupgruvtxres  27755  cusgrfilem1  27803  wlkres  28018  wlkp1lem2  28022  pthdivtx  28076  pthdlem2lem  28114  wlkiswwlks2lem4  28216  wwlksnredwwlkn0  28240  wwlksnextwrd  28241  wwlksnfi  28250  wwlksnextprop  28256  clwlkclwwlklem2a  28341  clwlkclwwlkf1lem2  28348  erclwwlksym  28364  clwwlkf1  28392  eleclclwwlknlem2  28404  erclwwlknsym  28413  clwwlknonex2  28452  eupth2lem3lem6  28576  frgr3vlem1  28616  3vfriswmgrlem  28620  wlkl0  28710  sspval  29064  nmosetre  29105  nmobndseqi  29120  nmobndseqiALT  29121  orthcom  29449  shsva  29661  shmodsi  29730  h1datomi  29922  nmopsetretALT  30204  nmfnsetre  30218  lnopcnbd  30377  pjclem4  30540  pj3si  30548  ssmd1  30652  atom1d  30694  chjatom  30698  atcvat4i  30738  cdj3lem2a  30777  cdj3lem3a  30780  disjunsn  30912  unitdivcld  31830  xrge0iifiso  31864  dya2iocuni  32229  bnj168  32688  bnj535  32849  bnj590  32869  bnj594  32871  bnj938  32896  bnj1118  32943  bnj1128  32949  fnrelpredd  33040  deranglem  33107  subfacp1lem6  33126  subfacval2  33128  cvmlift2lem12  33255  satffun  33350  mrsubvrs  33463  msrrcl  33484  mclsax  33510  dfon2lem6  33743  rdgprc  33749  nodenselem8  33873  slerec  33992  bday1s  34004  ssltleft  34033  ssltright  34034  ifscgr  34325  btwncolinear1  34350  hfelhf  34462  opnrebl2  34489  nn0prpw  34491  ordcmp  34615  findreccl  34621  nndivlub  34626  bj-rest0  35243  bj-isrvec2  35450  topdifinffinlem  35497  iooelexlt  35512  rdgeqoa  35520  exrecfnlem  35529  wl-mo3t  35710  matunitlindflem2  35753  poimirlem2  35758  poimirlem23  35779  poimirlem28  35784  poimirlem29  35785  poimirlem31  35787  poimirlem32  35788  eqfnun  35859  sdclem2  35879  sdclem1  35880  prdsbnd2  35932  ismtyval  35937  rrnequiv  35972  isexid2  35992  ismndo1  36010  exidreslem  36014  rngo2  36044  rngoueqz  36077  risci  36124  prtlem11  36859  prtlem15  36868  cvrat4  37436  lcfl6  39493  dvdsexpnn0  40321  harval3  41105  clcnvlem  41184  cnvrcl0  41186  cnvtrcl0  41187  iunrelexpmin1  41269  iunrelexpmin2  41273  fcoresf1b  44515  aovmpt4g  44644  elsetpreimafvbi  44795  iccpartiltu  44826  iccpartgt  44831  iccpartgel  44833  reuopreuprim  44930  fmtnofac1  44974  gbepos  45162  funcrngcsetc  45508  funcrngcsetcALT  45509  rhmsscrnghm  45536  funcringcsetc  45545  ellcoellss  45728  dignn0flhalflem2  45914  nn0sumshdiglemB  45918  1arympt1  45936  fullthinc  46279