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 )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl2anb  291  dcor  941  bm1.1  2214  eqtr3  2249  elnelne1  2504  elnelne2  2505  morex  2988  reuss2  3485  reupick  3489  rabsneu  3742  invdisjrab  4080  opabss  4151  triun  4198  poirr  4402  wepo  4454  wetrep  4455  rexxfrd  4558  reg3exmidlemwe  4675  nnsuc  4712  fnfco  5508  fun11iun  5601  fnressn  5835  fvpr1g  5855  fvtp1g  5857  fvtp3g  5859  fvtp3  5862  f1mpt  5907  caovlem2d  6210  offval  6238  dfoprab3  6349  1stconst  6381  2ndconst  6382  poxp  6392  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  fiintim  7116  pr1or2  7390  addclpi  7537  addnidpig  7546  reapmul1  8765  nnnn0addcl  9422  un0addcl  9425  un0mulcl  9426  zltnle  9515  nn0ge0div  9557  uzind3  9583  uzind4  9812  ltsubrp  9915  ltaddrp  9916  xrlttr  10020  xrltso  10021  xltnegi  10060  xaddnemnf  10082  xaddnepnf  10083  xaddcom  10086  xnegdi  10093  xsubge0  10106  fzind2  10475  qltnle  10493  qbtwnxr  10507  exp3vallem  10792  expp1  10798  expnegap0  10799  expcllem  10802  mulexpzap  10831  expaddzap  10835  expmulzap  10837  hashunlem  11057  cats1un  11292  reuccatpfxs1  11318  shftf  11381  sqrtdiv  11593  mulcn2  11863  summodclem2  11933  fsum3  11938  cvgratz  12083  prodmodclem2  12128  zproddc  12130  prodsnf  12143  dvdsflip  12402  dvdsfac  12411  bitsfzolem  12505  lcmgcdlem  12639  rpexp1i  12716  hashdvds  12783  hashgcdlem  12800  phisum  12803  pcqcl  12869  pcid  12887  ssnnctlemct  13057  issubmd  13547  grpinvnzcl  13645  mulgneg  13717  mulgnn0z  13726  01eq0ring  14193  lmss  14960  xmetrtri  15090  blssioo  15267  divcnap  15279  dedekindicc  15347  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvrecap  15427  dveflem  15440  lgsval3  15737  lgsdir2  15752  2sqlem6  15839  umgredg  15984  umgrpredgv  15986  umgredgne  15989  umgredgnlp  15991  usgredgppren  16036  edgssv2en  16038  uspgredg2vlem  16059  usgredg2vlem1  16061  uhgr0vsize0en  16074  bj-bdfindes  16480  bj-findes  16512  2omap  16530