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  1300  19.30dc  1627  nf4r  1671  cbvexv1  1752  cbvexh  1755  equveli  1759  sbequilem  1838  sb5rf  1852  nfsbxy  1942  nfsbxyt  1943  sbcomxyyz  1972  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  mo2n  2054  mo23  2067  2exeu  2118  bm1.1  2162  necon1idc  2400  sbhypf  2787  vtocl2  2793  vtocl3  2794  reu6  2927  rmo2ilem  3053  uneqin  3387  abn0r  3448  inelcm  3484  vdif0im  3489  difrab0eqim  3490  r19.3rm  3512  r19.9rmv  3515  difprsn1  3732  intminss  3870  disjnim  3995  bm1.3ii  4125  intexabim  4153  copsex2g  4247  opelopabt  4263  eusv2nf  4457  reusv3i  4460  onintrab2im  4518  ordtri2orexmid  4523  setindel  4538  onsucuni2  4564  ordtri2or2exmid  4571  zfregfr  4574  tfi  4582  mosubopt  4692  eqrelrel  4728  xpiindim  4765  opeliunxp2  4768  opelrn  4862  issref  5012  xpmlem  5050  rnxpid  5064  ssxpbm  5065  relcoi2  5160  unixpm  5165  cnviinm  5171  iotanul  5194  funimaexglem  5300  fvelrnb  5564  fvmptssdm  5601  fnfvrnss  5677  fressnfv  5704  fconstfvm  5735  f1mpt  5772  ovprc  5910  fo1stresm  6162  fo2ndresm  6163  spc2ed  6234  opeliunxp2f  6239  reldmtpos  6254  tfrlem5  6315  tfrlem9  6320  tfri2  6367  frecfcllem  6405  frecsuclem  6407  fvmptmap  6685  ixpiinm  6724  ixp0  6731  mptelixpg  6734  ener  6779  domtr  6785  unen  6816  xpf1o  6844  mapen  6846  ss1o0el1o  6912  cardval3ex  7184  distrnqg  7386  nqnq0pi  7437  nqnq0a  7453  nqnq0m  7454  distrnq0  7458  nqprloc  7544  ltexprlemopl  7600  ltexprlemopu  7602  recexre  8535  nn1suc  8938  msqznn  9353  nn0ind  9367  fnn0ind  9369  ublbneg  9613  qreccl  9642  fzo1fzo0n0  10183  elfzom1elp1fzo  10202  fzo0end  10223  fzind2  10239  flqeqceilz  10318  nnsinds  10443  nn0sinds  10444  ser0f  10515  hashfacen  10816  redivap  10883  imdivap  10890  cvg1nlemres  10994  sqrt0  11013  summodclem3  11388  fsump1i  11441  prodf1  11550  cos1bnd  11767  odd2np1  11878  opoe  11900  omoe  11901  opeo  11902  omeo  11903  dfgcd2  12015  gcdmultiplez  12022  dvdssq  12032  algfx  12052  odzval  12241  mul4sq  12392  setsfun0  12498  rmodislmod  13441  neipsm  13657  txbas  13761  elcncf1di  14069  reeff1o  14197  sincosq1lem  14249  sincosq2sgn  14251  sincosq4sgn  14253  lgsne0  14442  mul2sq  14466  bdbm1.3ii  14646