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  7530  pr2cv2  7542  distrnqg  7754  nqnq0pi  7805  nqnq0a  7821  nqnq0m  7822  distrnq0  7826  nqprloc  7912  ltexprlemopl  7968  ltexprlemopu  7970  recexre  8906  nn1suc  9323  msqznn  9746  nn0ind  9760  fnn0ind  9762  ublbneg  10013  qreccl  10042  fzo1fzo0n0  10595  elfzom1elp1fzo  10620  fzo0end  10641  fzind2  10658  flqeqceilz  10755  nnsinds  10882  nn0sinds  10883  ser0f  10971  hashfacen  11284  iswrddm0  11328  swrdlsw  11441  pfxn0  11460  swrdswrdlem  11476  pfxccatin12lem3  11504  pfxccat3  11506  pfxccat3a  11510  swrdccat3blem  11511  redivap  11639  imdivap  11646  cvg1nlemres  11751  sqrt0  11770  summodclem3  12147  fsump1i  12200  prodf1  12309  cos1bnd  12526  odd2np1  12640  opoe  12662  omoe  12663  opeo  12664  omeo  12665  dfgcd2  12791  gcdmultiplez  12798  dvdssq  12808  algfx  12830  odzval  13020  mul4sq  13173  ballotfilemsdom  13255  ballotfilemth  13281  setsfun0  13388  rmodislmod  14688  isridl  14841  neipsm  15255  txbas  15359  elcncf1di  15680  plyco  15860  reeff1o  15874  sincosq1lem  15926  sincosq2sgn  15928  sincosq4sgn  15930  lgsne0  16157  2lgslem1  16210  mul2sq  16235  lpvtx  16320  umgrislfupgrenlem  16371  umgrislfupgrdom  16372  uspgr2wlkeq  16606  wlklenvclwlk  16614  bdbm1.3ii  16917  wexmiddiffilem  17043  wexmiddifxylem  17045  als-no-surprise  17147