Theorem syl5ibr 236

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  syl5ibrcom  237  biimprd  238  exdistrf  2333  pm2.61ne  2879  unineq  3877  elpreqprlem  4395  oteqex  4964  elopabr  5013  otel3xp  5153  eqrelrdv2  5219  breldmg  5330  elrnmpt1  5374  cnveqb  5590  cnveq0  5591  predpoirr  5708  predfrirr  5709  ordtri3OLD  5760  limelon  5788  f1ssf1  6168  ndmfv  6218  ffvresb  6394  isomin  6587  isofrlem  6590  caovord3d  6844  eldifpw  6976  ssonuni  6986  onsucuni2  7034  ordzsl  7045  tfindsg  7060  findsg  7093  oteqimp  7187  frxp  7287  poxp  7289  fnwelem  7292  suppss  7325  wfrlem14  7428  tfrlem11  7484  oacl  7615  omcl  7616  oecl  7617  oa0r  7618  om0r  7619  om1r  7623  oe1m  7625  oaordi  7626  oawordri  7630  oaass  7641  oarec  7642  omwordri  7652  odi  7659  omass  7660  oewordri  7672  oeworde  7673  oeordsuc  7674  oelim2  7675  oeoa  7677  oeoelem  7678  oeoe  7679  nnm0r  7690  nnacl  7691  nnacom  7697  nnaordi  7698  nnaass  7702  nndi  7703  nnmass  7704  nnmsucr  7705  nnmcom  7706  omabs  7727  brecop  7840  eceqoveq  7853  elpm2r  7875  map0g  7897  undifixp  7944  fundmen  8030  mapxpen  8126  mapunen  8129  php  8144  unxpdomlem2  8165  pssnn  8178  f1vrnfibi  8251  elfir  8321  wemapso2lem  8457  wdompwdom  8483  inf3lem1  8525  inf3lem3  8527  cantnfval2  8566  cantnfp1lem3  8577  r1sdom  8637  r1tr  8639  carden2a  8792  fidomtri2  8820  prdom2  8829  infxpenlem  8836  acndom  8874  fodomacn  8879  wdomfil  8884  alephon  8892  alephordi  8897  alephle  8911  alephfplem3  8929  dfac2a  8952  kmlem9  8980  cflm  9072  cfslb  9088  cfslbn  9089  infpssrlem3  9127  infpssrlem4  9128  fin23lem21  9161  fin23lem30  9164  isf34lem7  9201  isf34lem6  9202  fin67  9217  isfin7-2  9218  fin1a2lem7  9228  fin1a2lem10  9231  iundom2g  9362  konigthlem  9390  alephreg  9404  gchdomtri  9451  wunr1om  9541  tskr1om  9589  inar1  9597  grur1a  9641  indpi  9729  genpprecl  9823  genpnmax  9829  addcmpblnr  9890  recexsrlem  9924  map2psrpr  9931  ax1rid  9982  axpre-mulgt0  9989  ltle  10126  nnmulcl  11043  nnsub  11059  nn0sub  11343  nneo  11461  uz11  11710  xrltle  11982  xltnegi  12047  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  supxrunb1  12149  supxrunb2  12150  om2uzuzi  12748  uzrdgxfr  12766  seqcl2  12819  seqfveq2  12823  seqshft2  12827  seqsplit  12834  seqcaopr3  12836  seqf1olem2a  12839  seqid2  12847  seqhomo  12848  ser1const  12857  m1expcl2  12882  expadd  12902  expmul  12905  faclbnd  13077  hashfzp1  13218  hashmap  13222  hashfacen  13238  hashf1lem1  13239  hashf1lem2  13240  hashf1  13241  seqcoll  13248  wrdsymb0  13339  swrdnd2  13433  wrd2ind  13477  swrdccatin12lem2  13489  swrdccatin1d  13499  repswccat  13532  repswcshw  13558  cshwcshid  13573  rtrclreclem3  13800  rtrclreclem4  13801  dfrtrcl2  13802  relexpindlem  13803  relexpind  13804  rtrclind  13805  recan  14076  rexanre  14086  rlimcn2  14321  caurcvg2  14408  fsumiun  14553  pwm1geoser  14600  efexp  14831  rpnnen2lem12  14954  dvdstr  15018  alzdvds  15042  zob  15083  sumeven  15110  sumodd  15111  bitsinv1  15164  smu01lem  15207  smupval  15210  smueqlem  15212  smumullem  15214  seq1st  15284  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  cncongr2  15382  prmdiveq  15491  odzdvds  15500  pythagtriplem2  15522  pcexp  15564  vdwlem13  15697  ramz  15729  prmolefac  15750  elrestr  16089  xpsff1o  16228  subsubc  16513  clatl  17116  frmdgsum  17399  dfgrp3e  17515  mulgneg2  17575  mulgnnass  17576  mulgnnassOLD  17577  mhmmulg  17583  gsumwrev  17796  symgbas  17800  symgextf1lem  17840  symgfixelsi  17855  pmtrdifellem4  17899  sylow1lem1  18013  efgsfo  18152  efgred  18161  cyggexb  18300  gsumzres  18310  gsum2dlem2  18370  ringadd2  18575  mulgass2  18601  lmodprop2d  18925  lspsnne2  19118  lspsneu  19123  assapropd  19327  mplcoe1  19465  mplcoe3  19466  mplcoe5  19468  ply1sclf1  19659  cnfldmulg  19778  cnfldexp  19779  zrhpsgnelbas  19940  mat1scmat  20345  restopn2  20981  cnpf2  21054  cmpfi  21211  txcn  21429  txlm  21451  xkoptsub  21457  xkopjcn  21459  ufildr  21735  cnflf  21806  fclsnei  21823  fclscmp  21834  ufilcmp  21836  cnfcf  21846  symgtgp  21905  isxms2  22253  met2ndc  22328  metustbl  22371  tngngp2  22456  clmmulg  22901  iscau4  23077  ovolunlem1a  23264  ovolicc2lem4  23288  volfiniun  23315  voliunlem1  23318  volsup  23324  dvnadd  23692  dvnres  23694  dvcobr  23709  ply1nzb  23882  plypf1  23968  dgrle  23999  coeaddlem  24005  dgrlt  24022  dvntaylp  24125  cxpmul2  24435  rlimcnp  24692  facgam  24792  wilthlem2  24795  isnsqf  24861  musum  24917  chtub  24937  chpval2  24943  gausslemma2dlem0i  25089  dchrisumlem1  25178  qabvexp  25315  ostthlem2  25317  axsegconlem1  25797  ax5seglem4  25812  ax5seglem5  25813  axlowdimlem15  25836  axcontlem2  25845  axcontlem4  25847  incistruhgr  25974  upgredg2vtx  26036  upgredgpr  26037  numedglnl  26039  uhgr2edg  26100  nbupgruvtxres  26308  cusgrfilem1  26351  wlkres  26567  wlkp1lem2  26571  pthdivtx  26625  pthdlem2lem  26663  wlkiswwlks2lem4  26758  wwlksnredwwlkn0  26791  wwlksnextwrd  26792  wwlksnextprop  26807  wwlksnonfi  26816  clwlkclwwlklem2a  26899  clwwlksf1  26917  erclwwlkssym  26935  eleclclwwlksnlem2  26939  erclwwlksnsym  26947  eupth2lem3lem6  27093  frgr3vlem1  27137  3vfriswmgrlem  27141  numclwwlkovf2ex  27219  extwwlkfab  27223  sspval  27578  nmosetre  27619  nmobndseqi  27634  nmobndseqiALT  27635  orthcom  27965  shsva  28179  shmodsi  28248  h1datomi  28440  nmopsetretALT  28722  nmfnsetre  28736  lnopcnbd  28895  pjclem4  29058  pj3si  29066  ssmd1  29170  atom1d  29212  chjatom  29216  atcvat4i  29256  cdj3lem2a  29295  cdj3lem3a  29298  disjunsn  29407  unitdivcld  29947  xrge0iifiso  29981  dya2iocuni  30345  bnj168  30798  bnj535  30960  bnj590  30980  bnj594  30982  bnj938  31007  bnj1118  31052  bnj1128  31058  deranglem  31148  subfacp1lem6  31167  subfacval2  31169  cvmlift2lem12  31296  mrsubvrs  31419  msrrcl  31440  mclsax  31466  dfon2lem6  31693  rdgprc  31700  trpredlem1  31727  frrlem5e  31788  nodenselem8  31841  slerec  31923  ifscgr  32151  btwncolinear1  32176  hfelhf  32288  opnrebl2  32316  nn0prpw  32318  ordcmp  32446  findreccl  32452  nndivlub  32457  bj-rest0  33046  topdifinffinlem  33195  iooelexlt  33210  rdgeqoa  33218  wl-mo3t  33358  matunitlindflem2  33406  poimirlem2  33411  poimirlem23  33432  poimirlem28  33437  poimirlem29  33438  poimirlem31  33440  poimirlem32  33441  eqfnun  33516  sdclem2  33538  sdclem1  33539  prdsbnd2  33594  ismtyval  33599  rrnequiv  33634  isexid2  33654  ismndo1  33672  exidreslem  33676  rngo2  33706  rngoueqz  33739  risci  33786  prtlem11  34151  prtlem15  34160  cvrat4  34729  lcfl6  36789  clcnvlem  37930  cnvrcl0  37932  cnvtrcl0  37933  iunrelexpmin1  38000  iunrelexpmin2  38004  aovmpt4g  41281  iccpartiltu  41358  iccpartgt  41363  iccpartgel  41365  pfxccatin12lem2  41424  fmtnofac1  41482  gbepos  41646  funcrngcsetc  41998  funcrngcsetcALT  41999  rhmsscrnghm  42026  funcringcsetc  42035  ellcoellss  42224  dignn0flhalflem2  42410  nn0sumshdiglemB  42414