Theorem sylbir 135

Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
sylbir.1	⊢ (𝜓 ↔ 𝜑)
sylbir.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
sylbir	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbir

Step	Hyp	Ref	Expression
1		sylbir.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	biimpri 133	. 2 ⊢ (𝜑 → 𝜓)
3		sylbir.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3i  200  3ori  1336  19.30dc  1675  nf4r  1719  cbvexv1  1800  cbvexh  1803  equveli  1807  sbequilem  1886  sb5rf  1900  nfsbxy  1995  nfsbxyt  1996  sbcomxyyz  2025  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  mo2n  2107  mo23  2121  2exeu  2172  bm1.1  2216  necon1idc  2455  sbhypf  2853  vtocl2  2859  vtocl3  2860  reu6  2995  rmo2ilem  3122  uneqin  3458  abn0r  3519  inelcm  3555  vdif0im  3560  difrab0eqim  3561  r19.3rm  3583  r19.9rmv  3586  difprsn1  3812  intminss  3953  disjnim  4078  bm1.3ii  4210  intexabim  4242  copsex2g  4338  opelopabt  4356  eusv2nf  4553  reusv3i  4556  onintrab2im  4616  ordtri2orexmid  4621  setindel  4636  onsucuni2  4662  ordtri2or2exmid  4669  zfregfr  4672  tfi  4680  mosubopt  4791  eqrelrel  4827  xpiindim  4867  opeliunxp2  4870  opelrn  4966  issref  5119  xpmlem  5157  rnxpid  5171  ssxpbm  5172  relcoi2  5267  unixpm  5272  cnviinm  5278  iotanul  5302  iotaexab  5305  funimaexglem  5413  fvelrnb  5693  fvmptssdm  5731  fnfvrnss  5807  fressnfv  5841  fconstfvm  5872  f1mpt  5912  ovprc  6054  fvmpopr2d  6158  fo1stresm  6324  fo2ndresm  6325  spc2ed  6398  opeliunxp2f  6404  reldmtpos  6419  tfrlem5  6480  tfrlem9  6485  tfri2  6532  frecfcllem  6570  frecsuclem  6572  fvmptmap  6854  ixpiinm  6893  ixp0  6900  mptelixpg  6903  ener  6953  domtr  6959  unen  6991  xpf1o  7030  mapen  7032  ss1o0el1o  7105  cardval3ex  7389  pr2cv2  7401  distrnqg  7607  nqnq0pi  7658  nqnq0a  7674  nqnq0m  7675  distrnq0  7679  nqprloc  7765  ltexprlemopl  7821  ltexprlemopu  7823  recexre  8758  nn1suc  9162  msqznn  9580  nn0ind  9594  fnn0ind  9596  ublbneg  9847  qreccl  9876  fzo1fzo0n0  10423  elfzom1elp1fzo  10448  fzo0end  10469  fzind2  10486  flqeqceilz  10581  nnsinds  10708  nn0sinds  10709  ser0f  10797  hashfacen  11101  iswrddm0  11141  swrdlsw  11254  pfxn0  11273  swrdswrdlem  11289  pfxccatin12lem3  11317  pfxccat3  11319  pfxccat3a  11323  swrdccat3blem  11324  redivap  11452  imdivap  11459  cvg1nlemres  11563  sqrt0  11582  summodclem3  11959  fsump1i  12012  prodf1  12121  cos1bnd  12338  odd2np1  12452  opoe  12474  omoe  12475  opeo  12476  omeo  12477  dfgcd2  12603  gcdmultiplez  12610  dvdssq  12620  algfx  12642  odzval  12832  mul4sq  12985  setsfun0  13136  rmodislmod  14384  isridl  14537  neipsm  14897  txbas  15001  elcncf1di  15322  plyco  15502  reeff1o  15516  sincosq1lem  15568  sincosq2sgn  15570  sincosq4sgn  15572  lgsne0  15786  2lgslem1  15839  mul2sq  15864  lpvtx  15949  umgrislfupgrenlem  16000  umgrislfupgrdom  16001  uspgr2wlkeq  16235  wlklenvclwlk  16243  bdbm1.3ii  16537