Theorem sylan2b 287

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 120	. 2 |- ( ph -> ch )
3		sylan2b.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 286	1 |- ( ( ps /\ ph ) -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> 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:  syl2anb  291  dcor  948  bm1.1  2223  eqtr3  2258  elnelne1  2524  elnelne2  2525  morex  3010  reuss2  3513  reupick  3517  rabsneu  3784  invdisjrab  4124  opabss  4196  triun  4244  poirr  4454  wepo  4506  wetrep  4507  rexxfrd  4611  reg3exmidlemwe  4728  nnsuc  4765  fnfco  5567  fun11iun  5663  fnressn  5904  fvpr1g  5924  fvtp1g  5926  fvtp3g  5928  fvtp3  5931  f1mpt  5980  caovlem2d  6285  offval  6314  dfoprab3  6429  1stconst  6461  2ndconst  6462  poxp  6472  suppssrst  6505  suppssrgst  6506  tfrlemisucaccv  6600  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  fiintim  7242  2omap  7324  pr1or2  7546  addclpi  7700  addnidpig  7709  reapmul1  8931  nnnn0addcl  9604  un0addcl  9607  un0mulcl  9608  zltnle  9701  nn0ge0div  9744  uzind3  9770  uzind4  10004  ltsubrp  10108  ltaddrp  10109  xrlttr  10214  xrltso  10215  xltnegi  10254  xaddnemnf  10276  xaddnepnf  10277  xaddcom  10280  xnegdi  10287  xsubge0  10300  fzind2  10675  qltnle  10695  qbtwnxr  10709  exp3vallem  10998  expp1  11004  expnegap0  11005  expcllem  11008  mulexpzap  11037  expaddzap  11041  expmulzap  11043  hashunlem  11266  cats1un  11515  reuccatpfxs1  11541  shftf  11617  sqrtdiv  11830  mulcn2  12103  summodclem2  12174  fsum3  12179  cvgratz  12324  prodmodclem2  12369  zproddc  12371  prodsnf  12384  dvdsflip  12643  dvdsfac  12652  bitsfzolem  12746  lcmgcdlem  12880  rpexp1i  12958  hashdvds  13028  hashgcdlem  13045  phisum  13048  pcqcl  13114  pcid  13132  ballotfilemfc0  13290  ballotfilemfcc  13291  ssnnctlemct  13395  issubmd  13840  grpinvnzcl  13936  mulgneg  14002  mulgnn0z  14011  gsumunsnfd  14259  gsum2dfilem1  14271  gsum2dfilem2  14272  01eq0ring  14605  psrbaglefifi  15172  lmss  15472  xmetrtri  15602  blssioo  15779  divcnap  15791  dedekindicc  15859  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvrecap  15939  dveflem  15952  pellexlem3  16231  prmorcht  16282  lgsval3  16342  lgsdir2  16357  2sqlem6  16444  umgredg  16591  umgrpredgv  16593  umgredgne  16596  umgredgnlp  16598  usgredgppren  16643  edgssv2en  16645  uspgredg2vlem  16666  usgredg2vlem1  16668  uhgr0vsize0en  16681  wlkepvtx  16821  bj-bdfindes  17180  bj-findes  17212