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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr3i  200  3ori  1341  19.30dc  1680  nf4r  1723  cbvexv1  1805  cbvexh  1808  equveli  1812  sbequilem  1891  sb5rf  1905  nfsbxy  2002  nfsbxyt  2003  sbcomxyyz  2032  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  mo2n  2114  mo23  2128  2exeu  2179  bm1.1  2223  necon1idc  2473  sbhypf  2872  vtocl2  2878  vtocl3  2879  reu6  3015  rmo2ilem  3142  rabssrabd  3335  uneqin  3482  abn0r  3546  inelcm  3585  vdif0im  3590  difrab0eqim  3591  r19.3rm  3616  r19.9rmv  3619  difprsn1  3854  intminss  3995  disjnim  4120  bm1.3ii  4254  intexabim  4288  copsex2g  4386  opelopabt  4404  eusv2nf  4602  reusv3i  4605  onintrab2im  4665  ordtri2orexmid  4670  setindel  4685  onsucuni2  4711  ordtri2or2exmid  4718  zfregfr  4721  tfi  4729  mosubopt  4840  eqrelrel  4876  xpiindim  4917  opeliunxp2  4920  opelrn  5016  issref  5170  xpmlem  5208  rnxpid  5222  ssxpbm  5223  relcoi2  5318  unixpm  5323  cnviinm  5329  iotanul  5353  iotaexab  5356  funimaexglem  5464  fvelrnb  5750  fvmptssdm  5790  fnfvrnss  5868  fressnfv  5902  fconstfvm  5933  f1mpt  5977  ovprc  6121  fvmpopr2d  6225  fo1stresm  6395  fo2ndresm  6396  spc2ed  6469  opeliunxp2f  6509  reldmtpos  6524  tfrlem5  6585  tfrlem9  6590  tfri2  6637  frecfcllem  6675  frecsuclem  6677  fvmptmap  6966  ixpiinm  7006  ixp0  7013  mptelixpg  7016  ener  7066  domtr  7072  unen  7105  xpf1o  7144  mapen  7146  ss1o0el1o  7220  cardval3ex  7531  pr2cv2  7543  distrnqg  7755  nqnq0pi  7806  nqnq0a  7822  nqnq0m  7823  distrnq0  7827  nqprloc  7913  ltexprlemopl  7969  ltexprlemopu  7971  recexre  8909  nn1suc  9326  msqznn  9751  nn0ind  9765  fnn0ind  9767  ublbneg  10023  qreccl  10052  fzo1fzo0n0  10606  elfzom1elp1fzo  10631  fzo0end  10652  fzind2  10669  flqeqceilz  10770  nnsinds  10897  nn0sinds  10898  ser0f  10986  hashfacen  11300  iswrddm0  11344  swrdlsw  11457  pfxn0  11476  swrdswrdlem  11492  pfxccatin12lem3  11520  pfxccat3  11522  pfxccat3a  11526  swrdccat3blem  11527  redivap  11655  imdivap  11662  cvg1nlemres  11767  sqrt0  11786  summodclem3  12166  fsump1i  12219  prodf1  12328  cos1bnd  12545  odd2np1  12659  opoe  12681  omoe  12682  opeo  12683  omeo  12684  dfgcd2  12810  gcdmultiplez  12817  dvdssq  12827  algfx  12849  odzval  13043  mul4sq  13196  ballotfilemsdom  13307  ballotfilemth  13333  setsfun0  13440  rmodislmod  14772  isridl  14925  neipsm  15346  txbas  15450  elcncf1di  15771  plyco  15951  reeff1o  15965  sincosq1lem  16018  sincosq2sgn  16020  sincosq4sgn  16022  lgsne0  16323  2lgslem1  16376  mul2sq  16401  lpvtx  16486  umgrislfupgrenlem  16537  umgrislfupgrdom  16538  uspgr2wlkeq  16772  wlklenvclwlk  16780  bdbm1.3ii  17083  wexmiddiffilem  17209  wexmiddifxylem  17211  als-no-surprise  17314