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  1334  19.30dc  1673  nf4r  1717  cbvexv1  1798  cbvexh  1801  equveli  1805  sbequilem  1884  sb5rf  1898  nfsbxy  1993  nfsbxyt  1994  sbcomxyyz  2023  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  mo2n  2105  mo23  2119  2exeu  2170  bm1.1  2214  necon1idc  2453  sbhypf  2850  vtocl2  2856  vtocl3  2857  reu6  2992  rmo2ilem  3119  uneqin  3455  abn0r  3516  inelcm  3552  vdif0im  3557  difrab0eqim  3558  r19.3rm  3580  r19.9rmv  3583  difprsn1  3807  intminss  3948  disjnim  4073  bm1.3ii  4205  intexabim  4236  copsex2g  4332  opelopabt  4350  eusv2nf  4547  reusv3i  4550  onintrab2im  4610  ordtri2orexmid  4615  setindel  4630  onsucuni2  4656  ordtri2or2exmid  4663  zfregfr  4666  tfi  4674  mosubopt  4784  eqrelrel  4820  xpiindim  4859  opeliunxp2  4862  opelrn  4958  issref  5111  xpmlem  5149  rnxpid  5163  ssxpbm  5164  relcoi2  5259  unixpm  5264  cnviinm  5270  iotanul  5294  iotaexab  5297  funimaexglem  5404  fvelrnb  5683  fvmptssdm  5721  fnfvrnss  5797  fressnfv  5830  fconstfvm  5861  f1mpt  5901  ovprc  6043  fvmpopr2d  6147  fo1stresm  6313  fo2ndresm  6314  spc2ed  6385  opeliunxp2f  6390  reldmtpos  6405  tfrlem5  6466  tfrlem9  6471  tfri2  6518  frecfcllem  6556  frecsuclem  6558  fvmptmap  6840  ixpiinm  6879  ixp0  6886  mptelixpg  6889  ener  6939  domtr  6945  unen  6977  xpf1o  7013  mapen  7015  ss1o0el1o  7086  cardval3ex  7368  pr2cv2  7380  distrnqg  7585  nqnq0pi  7636  nqnq0a  7652  nqnq0m  7653  distrnq0  7657  nqprloc  7743  ltexprlemopl  7799  ltexprlemopu  7801  recexre  8736  nn1suc  9140  msqznn  9558  nn0ind  9572  fnn0ind  9574  ublbneg  9820  qreccl  9849  fzo1fzo0n0  10395  elfzom1elp1fzo  10420  fzo0end  10441  fzind2  10457  flqeqceilz  10552  nnsinds  10679  nn0sinds  10680  ser0f  10768  hashfacen  11071  iswrddm0  11108  swrdlsw  11216  pfxn0  11235  swrdswrdlem  11251  pfxccatin12lem3  11279  pfxccat3  11281  pfxccat3a  11285  swrdccat3blem  11286  redivap  11400  imdivap  11407  cvg1nlemres  11511  sqrt0  11530  summodclem3  11906  fsump1i  11959  prodf1  12068  cos1bnd  12285  odd2np1  12399  opoe  12421  omoe  12422  opeo  12423  omeo  12424  dfgcd2  12550  gcdmultiplez  12557  dvdssq  12567  algfx  12589  odzval  12779  mul4sq  12932  setsfun0  13083  rmodislmod  14330  isridl  14483  neipsm  14843  txbas  14947  elcncf1di  15268  plyco  15448  reeff1o  15462  sincosq1lem  15514  sincosq2sgn  15516  sincosq4sgn  15518  lgsne0  15732  2lgslem1  15785  mul2sq  15810  lpvtx  15894  umgrislfupgrenlem  15943  umgrislfupgrdom  15944  uspgr2wlkeq  16106  wlklenvclwlk  16114  bdbm1.3ii  16309