Theorem pm3.26 256

Description: Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112.

Assertion

Ref	Expression
pm3.26	|- ((ph /\ ps) -> ph)

Proof of Theorem pm3.26

Step	Hyp	Ref	Expression
1		df-an 198	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2		pm3.26im 120	. 2 |- (-. (ph -> -. ps) -> ph)
3	1, 2	sylbi 174	1 |- ((ph /\ ps) -> ph)

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196

This theorem is referenced by:  pm3.26i 257  pm3.26d 258  ancrb 265  pm4.45im 267  anim12i 268  adantrd 308  anidm 331  ancom 333  abai 366  anabs1 374  pm3.48 430  ibib 448  ordi 452  pm4.71 481  intnanr 517  biantrud 545  bianfd 554  dedlemb 570  19.26 749  19.40 773  sbequ2 864  mopick2 1057  moexex 1058  2exeu 1066  2eu2 1068  r19.40 1301  ssab 1555  class2set 1747  moabex 1868  mosubop 1911  iununi 2037  ordelord 2221  ordsseleq 2227  onin 2229  ordsson 2242  ralxp 2456  xpss 2465  opabssxp 2468  xp0r 2474  dmcosseq 2572  relssres 2596  dminss 2648  imainss 2649  cores 2659  fun11uni 2707  ffnfv 2892  isotr 2935  isotrALT 2936  isofrlem 2939  f1oiso 2942  tz7.48lem 2993  tz7.48-2 2995  fnoprab 3038  oaass 3163  omordi 3164  oen0 3165  nndi 3180  nnmord 3189  ecopoprtrn 3247  eceqopreq 3249  th3qlem1 3250  pw2en 3348  ssenen 3399  unblem1 3431  unblem2 3432  dfom3 3477  r1ord 3499  r1val1 3502  rankr1 3518  karden 3551  aceq3 3556  kmlem13 3592  kmlem16 3595  hta 3619  cardalephex 3691  axrepnd 3740  axunnd 3742  axacndlem1 3753  axacndlem3 3755  enqeceq 3841  distrpq 3861  ltexpq 3874  prn0 3887  prpssnq 3888  genpnnp 3902  addclprlem2 3913  distrlem4pr 3924  prlem936 3949  reclem3pr 3952  suplem2pr 3956  enreceq 3971  mulcmpblnr 3977  axrecex 4079  divdivdivt 4265  divdiv23t 4271  leltnet 4287  ltsubpost 4364  1nn 4432  nnind 4434  nnleltp1t 4448  nndiv 4453  nnreclt 4522  creur 4532  znnsubt 4595  qrecclt 4646  seqrn 4673  expaddt 4698  replimt 4798  ruclem28 4912  infdif 4948  infmap2lem1 4951  infmap2lem2 4952  gch-kn 4957  hvsubaddeqt 5019  hi2eqt 5059  shex 5115  shaddclt 5123  chocuni 5179  occllem6 5185  projlem26 5218  pjthu 5241  pjoml 5271  chabs1t 5432  spansncol 5473  h1datom 5483  osumlem7 5536  5oalem1 5544  5oalem2 5545  5oalem5 5548  3oalem2 5553  pjclem4 5653  pj3s 5659  stge0t 5673  cvpsst 5717  spansncv2t 5725  dmdbr2 5733  ssmd2 5735  atn0 5743  chcv1t 5751  atcv0eq 5767  atexch 5769  atcvat3 5774  atcvat4 5775  mdsymlem2 5777  mdsymlem3 5778  mdsymlem5 5780

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org