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	|- ( ps <-> ph )
sylbir.2	|- ( ps -> ch )

Assertion

Ref	Expression
sylbir	|- ( ph -> ch )

Proof of Theorem sylbir

Step	Hyp	Ref	Expression
1		sylbir.1	. . 3 |- ( ps <-> ph )
2	1	biimpri 133	. 2 |- ( ph -> ps )
3		sylbir.2	. 2 |- ( ps -> ch )
4	2, 3	syl 14	1 |- ( ph -> ch )

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  8908  nn1suc  9325  msqznn  9750  nn0ind  9764  fnn0ind  9766  ublbneg  10022  qreccl  10051  fzo1fzo0n0  10605  elfzom1elp1fzo  10630  fzo0end  10651  fzind2  10668  flqeqceilz  10768  nnsinds  10895  nn0sinds  10896  ser0f  10984  hashfacen  11298  iswrddm0  11342  swrdlsw  11455  pfxn0  11474  swrdswrdlem  11490  pfxccatin12lem3  11518  pfxccat3  11520  pfxccat3a  11524  swrdccat3blem  11525  redivap  11653  imdivap  11660  cvg1nlemres  11765  sqrt0  11784  summodclem3  12163  fsump1i  12216  prodf1  12325  cos1bnd  12542  odd2np1  12656  opoe  12678  omoe  12679  opeo  12680  omeo  12681  dfgcd2  12807  gcdmultiplez  12814  dvdssq  12824  algfx  12846  odzval  13040  mul4sq  13193  ballotfilemsdom  13304  ballotfilemth  13330  setsfun0  13437  rmodislmod  14737  isridl  14890  neipsm  15304  txbas  15408  elcncf1di  15729  plyco  15909  reeff1o  15923  sincosq1lem  15976  sincosq2sgn  15978  sincosq4sgn  15980  lgsne0  16255  2lgslem1  16308  mul2sq  16333  lpvtx  16418  umgrislfupgrenlem  16469  umgrislfupgrdom  16470  uspgr2wlkeq  16704  wlklenvclwlk  16712  bdbm1.3ii  17015  wexmiddiffilem  17141  wexmiddifxylem  17143  als-no-surprise  17245