Theorem syl5ibr 235

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  syl5ibrcom  236  biimprd  237  exdistrf  2321  pm2.61ne  2867  unineq  3836  elpreqprlem  4333  oteqex  4889  elopabr  4937  otel3xp  5077  eqrelrdv2  5142  breldmg  5252  elrnmpt1  5295  cnveqb  5508  cnveq0  5509  predpoirr  5625  predfrirr  5626  ordtri3OLD  5677  limelon  5705  ndmfv  6128  ffvresb  6301  isomin  6487  isofrlem  6490  caovord3d  6742  eldifpw  6868  ssonuni  6878  onsucuni2  6926  ordzsl  6937  tfindsg  6952  findsg  6985  oteqimp  7078  frxp  7174  poxp  7176  fnwelem  7179  suppss  7212  wfrlem14  7315  tfrlem11  7371  oacl  7502  omcl  7503  oecl  7504  oa0r  7505  om0r  7506  om1r  7510  oe1m  7512  oaordi  7513  oawordri  7517  oaass  7528  oarec  7529  omwordri  7539  odi  7546  omass  7547  oewordri  7559  oeworde  7560  oeordsuc  7561  oelim2  7562  oeoa  7564  oeoelem  7565  oeoe  7566  nnm0r  7577  nnacl  7578  nnacom  7584  nnaordi  7585  nnaass  7589  nndi  7590  nnmass  7591  nnmsucr  7592  nnmcom  7593  omabs  7614  brecop  7727  eceqoveq  7740  elpm2r  7761  map0g  7783  undifixp  7830  fundmen  7916  mapxpen  8011  mapunen  8014  php  8029  unxpdomlem2  8050  pssnn  8063  f1vrnfibi  8134  elfir  8204  wemapso2lem  8340  wdompwdom  8366  inf3lem1  8408  inf3lem3  8410  cantnfval2  8449  cantnfp1lem3  8460  r1sdom  8520  r1tr  8522  carden2a  8675  fidomtri2  8703  prdom2  8712  infxpenlem  8719  acndom  8757  fodomacn  8762  wdomfil  8767  alephon  8775  alephordi  8780  alephle  8794  alephfplem3  8812  dfac2a  8835  kmlem9  8863  cflm  8955  cfslb  8971  cfslbn  8972  infpssrlem3  9010  infpssrlem4  9011  fin23lem21  9044  fin23lem30  9047  isf34lem7  9084  isf34lem6  9085  fin67  9100  isfin7-2  9101  fin1a2lem7  9111  fin1a2lem10  9114  iundom2g  9241  konigthlem  9269  alephreg  9283  gchdomtri  9330  wunr1om  9420  tskr1om  9468  inar1  9476  grur1a  9520  indpi  9608  genpprecl  9702  genpnmax  9708  addcmpblnr  9769  recexsrlem  9803  map2psrpr  9810  ax1rid  9861  axpre-mulgt0  9868  ltle  10005  nnmulcl  10920  nnsub  10936  nn0sub  11220  nneo  11337  uz11  11586  xrltle  11858  xltnegi  11921  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  supxrunb1  12021  supxrunb2  12022  om2uzuzi  12610  uzrdgxfr  12628  seqcl2  12681  seqfveq2  12685  seqshft2  12689  seqsplit  12696  seqcaopr3  12698  seqf1olem2a  12701  seqid2  12709  seqhomo  12710  ser1const  12719  m1expcl2  12744  expadd  12764  expmul  12767  faclbnd  12939  hashfzp1  13078  hashmap  13082  hashfacen  13095  hashf1lem1  13096  hashf1lem2  13097  hashf1  13098  seqcoll  13105  wrdsymb0  13194  swrdnd2  13285  wrd2ind  13329  swrdccatin12lem2  13340  swrdccatin1d  13350  repswccat  13383  repswcshw  13409  cshwcshid  13424  rtrclreclem3  13648  rtrclreclem4  13649  dfrtrcl2  13650  relexpindlem  13651  relexpind  13652  rtrclind  13653  recan  13924  rexanre  13934  rlimcn2  14169  caurcvg2  14256  fsumiun  14394  pwm1geoser  14439  efexp  14670  rpnnen2lem12  14793  dvdstr  14856  alzdvds  14880  zob  14921  sumeven  14948  sumodd  14949  bitsinv1  15002  smu01lem  15045  smupval  15048  smueqlem  15050  smumullem  15052  seq1st  15122  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  cncongr2  15220  prmdiveq  15329  odzdvds  15338  pythagtriplem2  15360  pcexp  15402  vdwlem13  15535  ramz  15567  prmolefac  15588  elrestr  15912  xpsff1o  16051  subsubc  16336  clatl  16939  frmdgsum  17222  dfgrp3e  17338  mulgneg2  17398  mulgnnass  17399  mulgnnassOLD  17400  mhmmulg  17406  gsumwrev  17619  symgbas  17623  symgextf1lem  17663  symgfixelsi  17678  pmtrdifellem4  17722  sylow1lem1  17836  efgsfo  17975  efgred  17984  cyggexb  18123  gsumzres  18133  gsum2dlem2  18193  ringadd2  18398  mulgass2  18424  lmodprop2d  18748  lspsnne2  18939  lspsneu  18944  assapropd  19148  mplcoe1  19286  mplcoe3  19287  mplcoe5  19289  ply1sclf1  19480  cnfldmulg  19597  cnfldexp  19598  zrhpsgnelbas  19759  mat1scmat  20164  restopn2  20791  cnpf2  20864  cmpfi  21021  txcn  21239  txlm  21261  xkoptsub  21267  xkopjcn  21269  ufildr  21545  cnflf  21616  fclsnei  21633  fclscmp  21644  ufilcmp  21646  cnfcf  21656  symgtgp  21715  isxms2  22063  met2ndc  22138  metustbl  22181  tngngp2  22266  clmmulg  22709  iscau4  22885  ovolunlem1a  23071  ovolicc2lem4  23095  volfiniun  23122  voliunlem1  23125  volsup  23131  dvnadd  23498  dvnres  23500  dvcobr  23515  ply1nzb  23686  plypf1  23772  dgrle  23803  coeaddlem  23809  dgrlt  23826  dvntaylp  23929  cxpmul2  24235  rlimcnp  24492  facgam  24592  wilthlem2  24595  isnsqf  24661  musum  24717  chtub  24737  chpval2  24743  gausslemma2dlem0i  24889  dchrisumlem1  24978  qabvexp  25115  ostthlem2  25117  axsegconlem1  25597  ax5seglem4  25612  ax5seglem5  25613  axlowdimlem15  25636  axcontlem2  25645  axcontlem4  25647  incistruhgr  25746  upgredg2vtx  25814  upgredgpr  25815  ushgrauhgra  25832  usgra2edg  25911  cusgrafilem1  26007  sizeusglecusglem1  26012  sizeusglecusg  26014  trliswlk  26069  2trllemF  26079  constr3lem6  26177  1conngra  26203  wlkiswwlk2lem4  26222  wwlknredwwlkn0  26255  wwlkextwrd  26256  wwlkextproplem1  26269  wwlkextprop  26272  clwlkisclwwlklem2a  26313  clwwlkf1  26324  erclwwlksym  26342  eleclclwwlknlem2  26346  erclwwlknsym  26354  el2wlkonot  26396  el2spthonot  26397  hashnbgravdg  26440  eupatrl  26495  frgra3vlem1  26527  3vfriswmgralem  26531  frconngra  26548  frgrawopreglem3  26573  frg2wot1  26584  2spotiundisj  26589  usg2spot2nb  26592  usgreg2spot  26594  extwwlkfablem2  26605  numclwwlkovf2ex  26613  extwwlkfab  26617  sspval  26962  nmosetre  27003  nmobndseqi  27018  nmobndseqiALT  27019  orthcom  27349  shsva  27563  shmodsi  27632  h1datomi  27824  nmopsetretALT  28106  nmfnsetre  28120  lnopcnbd  28279  pjclem4  28442  pj3si  28450  ssmd1  28554  atom1d  28596  chjatom  28600  atcvat4i  28640  cdj3lem2a  28679  cdj3lem3a  28682  disjunsn  28789  unitdivcld  29275  xrge0iifiso  29309  dya2iocuni  29672  bnj168  30052  bnj535  30214  bnj590  30234  bnj594  30236  bnj938  30261  bnj1118  30306  bnj1128  30312  deranglem  30402  subfacp1lem6  30421  subfacval2  30423  cvmlift2lem12  30550  mrsubvrs  30673  msrrcl  30694  mclsax  30720  dfon2lem6  30937  rdgprc  30944  trpredlem1  30971  frrlem5e  31032  nodenselem8  31087  ifscgr  31321  btwncolinear1  31346  hfelhf  31458  opnrebl2  31486  nn0prpw  31488  ordcmp  31616  findreccl  31622  nndivlub  31627  bj-rest0  32227  topdifinffinlem  32371  iooelexlt  32386  rdgeqoa  32394  wl-mo3t  32537  matunitlindflem2  32576  poimirlem2  32581  poimirlem23  32602  poimirlem28  32607  poimirlem29  32608  poimirlem31  32610  poimirlem32  32611  eqfnun  32686  sdclem2  32708  sdclem1  32709  prdsbnd2  32764  ismtyval  32769  rrnequiv  32804  isexid2  32824  ismndo1  32842  exidreslem  32846  rngo2  32876  rngoueqz  32909  risci  32956  prtlem11  33169  prtlem15  33178  cvrat4  33747  lcfl6  35807  clcnvlem  36949  cnvrcl0  36951  cnvtrcl0  36952  iunrelexpmin1  37019  iunrelexpmin2  37023  aovmpt4g  39930  iccpartiltu  39960  iccpartgt  39965  iccpartgel  39967  fmtnofac1  40020  gbepos  40180  pfxccatin12lem2  40287  f1ssf1  40328  uhgr2edg  40435  nbupgruvtxres  40634  cusgrfilem1  40671  1wlkres  40879  1wlkp1lem2  40883  pthdivtx  40935  pthdlem2lem  40973  1wlkiswwlks2lem4  41069  wwlksnredwwlkn0  41102  wwlksnextwrd  41103  wwlksnextprop  41118  wwlksnonfi  41127  clwlkclwwlklem2a  41207  clwwlksf1  41224  erclwwlkssym  41242  eleclclwwlksnlem2  41246  erclwwlksnsym  41254  eupth2lem3lem6  41401  frgr3vlem1  41443  3vfriswmgrlem  41447  frgr2wwlk1  41494  av-numclwwlkovf2ex  41517  av-extwwlkfab  41520  funcrngcsetc  41790  funcrngcsetcALT  41791  rhmsscrnghm  41818  funcringcsetc  41827  ellcoellss  42018  dignn0flhalflem2  42208  nn0sumshdiglemB  42212