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  944  bm1.1  2217  eqtr3  2252  elnelne1  2516  elnelne2  2517  morex  3001  reuss2  3501  reupick  3505  rabsneu  3764  invdisjrab  4103  opabss  4174  triun  4221  poirr  4428  wepo  4480  wetrep  4481  rexxfrd  4584  reg3exmidlemwe  4701  nnsuc  4738  fnfco  5539  fun11iun  5635  fnressn  5870  fvpr1g  5890  fvtp1g  5892  fvtp3g  5894  fvtp3  5897  f1mpt  5944  caovlem2d  6247  offval  6274  dfoprab3  6385  1stconst  6417  2ndconst  6418  poxp  6428  suppssrst  6461  suppssrgst  6462  tfrlemisucaccv  6556  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  fiintim  7191  2omap  7269  pr1or2  7491  addclpi  7642  addnidpig  7651  reapmul1  8869  nnnn0addcl  9526  un0addcl  9529  un0mulcl  9530  zltnle  9623  nn0ge0div  9665  uzind3  9691  uzind4  9920  ltsubrp  10023  ltaddrp  10024  xrlttr  10128  xrltso  10129  xltnegi  10168  xaddnemnf  10190  xaddnepnf  10191  xaddcom  10194  xnegdi  10201  xsubge0  10214  fzind2  10585  qltnle  10603  qbtwnxr  10617  exp3vallem  10902  expp1  10908  expnegap0  10909  expcllem  10912  mulexpzap  10941  expaddzap  10945  expmulzap  10947  hashunlem  11168  cats1un  11413  reuccatpfxs1  11439  shftf  11515  sqrtdiv  11727  mulcn2  11997  summodclem2  12068  fsum3  12073  cvgratz  12218  prodmodclem2  12263  zproddc  12265  prodsnf  12278  dvdsflip  12537  dvdsfac  12546  bitsfzolem  12640  lcmgcdlem  12774  rpexp1i  12851  hashdvds  12918  hashgcdlem  12935  phisum  12938  pcqcl  13004  pcid  13022  ssnnctlemct  13197  issubmd  13687  grpinvnzcl  13785  mulgneg  13857  mulgnn0z  13866  01eq0ring  14334  lmss  15111  xmetrtri  15241  blssioo  15418  divcnap  15430  dedekindicc  15498  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvrecap  15578  dveflem  15591  pellexlem3  15847  lgsval3  15891  lgsdir2  15906  2sqlem6  15993  umgredg  16140  umgrpredgv  16142  umgredgne  16145  umgredgnlp  16147  usgredgppren  16192  edgssv2en  16194  uspgredg2vlem  16215  usgredg2vlem1  16217  uhgr0vsize0en  16230  wlkepvtx  16370  bj-bdfindes  16719  bj-findes  16751