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  1311  19.30dc  1641  nf4r  1685  cbvexv1  1766  cbvexh  1769  equveli  1773  sbequilem  1852  sb5rf  1866  nfsbxy  1961  nfsbxyt  1962  sbcomxyyz  1991  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  mo2n  2073  mo23  2086  2exeu  2137  bm1.1  2181  necon1idc  2420  sbhypf  2813  vtocl2  2819  vtocl3  2820  reu6  2953  rmo2ilem  3079  uneqin  3415  abn0r  3476  inelcm  3512  vdif0im  3517  difrab0eqim  3518  r19.3rm  3540  r19.9rmv  3543  difprsn1  3762  intminss  3900  disjnim  4025  bm1.3ii  4155  intexabim  4186  copsex2g  4280  opelopabt  4297  eusv2nf  4492  reusv3i  4495  onintrab2im  4555  ordtri2orexmid  4560  setindel  4575  onsucuni2  4601  ordtri2or2exmid  4608  zfregfr  4611  tfi  4619  mosubopt  4729  eqrelrel  4765  xpiindim  4804  opeliunxp2  4807  opelrn  4901  issref  5053  xpmlem  5091  rnxpid  5105  ssxpbm  5106  relcoi2  5201  unixpm  5206  cnviinm  5212  iotanul  5235  iotaexab  5238  funimaexglem  5342  fvelrnb  5611  fvmptssdm  5649  fnfvrnss  5725  fressnfv  5752  fconstfvm  5783  f1mpt  5821  ovprc  5961  fvmpopr2d  6063  fo1stresm  6228  fo2ndresm  6229  spc2ed  6300  opeliunxp2f  6305  reldmtpos  6320  tfrlem5  6381  tfrlem9  6386  tfri2  6433  frecfcllem  6471  frecsuclem  6473  fvmptmap  6753  ixpiinm  6792  ixp0  6799  mptelixpg  6802  ener  6847  domtr  6853  unen  6884  xpf1o  6914  mapen  6916  ss1o0el1o  6983  cardval3ex  7265  distrnqg  7473  nqnq0pi  7524  nqnq0a  7540  nqnq0m  7541  distrnq0  7545  nqprloc  7631  ltexprlemopl  7687  ltexprlemopu  7689  recexre  8624  nn1suc  9028  msqznn  9445  nn0ind  9459  fnn0ind  9461  ublbneg  9706  qreccl  9735  fzo1fzo0n0  10278  elfzom1elp1fzo  10297  fzo0end  10318  fzind2  10334  flqeqceilz  10429  nnsinds  10556  nn0sinds  10557  ser0f  10645  hashfacen  10947  iswrddm0  10978  redivap  11058  imdivap  11065  cvg1nlemres  11169  sqrt0  11188  summodclem3  11564  fsump1i  11617  prodf1  11726  cos1bnd  11943  odd2np1  12057  opoe  12079  omoe  12080  opeo  12081  omeo  12082  dfgcd2  12208  gcdmultiplez  12215  dvdssq  12225  algfx  12247  odzval  12437  mul4sq  12590  setsfun0  12741  rmodislmod  13985  isridl  14138  neipsm  14498  txbas  14602  elcncf1di  14923  plyco  15103  reeff1o  15117  sincosq1lem  15169  sincosq2sgn  15171  sincosq4sgn  15173  lgsne0  15387  2lgslem1  15440  mul2sq  15465  bdbm1.3ii  15645