Theorem sylan2b 285

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2b.1	|- ( ph <-> ch )
sylan2b.2	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylan2b	|- ( ( ps /\ ph ) -> th )

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan2b.1	. . 3 |- ( ph <-> ch )
2	1	biimpi 119	. 2 |- ( ph -> ch )
3		sylan2b.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 284	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anb  289  dcor  930  bm1.1  2155  eqtr3  2190  elnelne1  2444  elnelne2  2445  morex  2914  reuss2  3407  reupick  3411  rabsneu  3656  opabss  4053  triun  4100  poirr  4292  wepo  4344  wetrep  4345  rexxfrd  4448  reg3exmidlemwe  4563  nnsuc  4600  fnfco  5372  fun11iun  5463  fnressn  5682  fvpr1g  5702  fvtp1g  5704  fvtp3g  5706  fvtp3  5709  f1mpt  5750  caovlem2d  6045  offval  6068  dfoprab3  6170  1stconst  6200  2ndconst  6201  poxp  6211  tfrlemisucaccv  6304  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  fiintim  6906  addclpi  7289  addnidpig  7298  reapmul1  8514  nnnn0addcl  9165  un0addcl  9168  un0mulcl  9169  zltnle  9258  nn0ge0div  9299  uzind3  9325  uzind4  9547  ltsubrp  9647  ltaddrp  9648  xrlttr  9752  xrltso  9753  xltnegi  9792  xaddnemnf  9814  xaddnepnf  9815  xaddcom  9818  xnegdi  9825  xsubge0  9838  fzind2  10195  qltnle  10202  qbtwnxr  10214  exp3vallem  10477  expp1  10483  expnegap0  10484  expcllem  10487  mulexpzap  10516  expaddzap  10520  expmulzap  10522  hashunlem  10739  shftf  10794  sqrtdiv  11006  mulcn2  11275  summodclem2  11345  fsum3  11350  cvgratz  11495  prodmodclem2  11540  zproddc  11542  prodsnf  11555  dvdsflip  11811  dvdsfac  11820  lcmgcdlem  12031  rpexp1i  12108  hashdvds  12175  hashgcdlem  12192  phisum  12194  pcqcl  12260  pcid  12277  ssnnctlemct  12401  issubmd  12696  grpinvnzcl  12771  lmss  13040  xmetrtri  13170  blssioo  13339  divcnap  13349  dedekindicc  13405  dvidlemap  13454  dvrecap  13471  dveflem  13481  lgsval3  13713  lgsdir2  13728  2sqlem6  13750  bj-bdfindes  13984  bj-findes  14016