Theorem pm3.26 319

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

Assertion

Ref	Expression
pm3.26	⊢ ((φ ⋀ ψ) → φ)

Proof of Theorem pm3.26

Step	Hyp	Ref	Expression
1		df-an 225	. 2 ⊢ ((φ ⋀ ψ) ↔ ¬ (φ → ¬ ψ))
2		pm3.26im 139	. 2 ⊢ (¬ (φ → ¬ ψ) → φ)
3	1, 2	sylbi 199	1 ⊢ ((φ ⋀ ψ) → φ)

Syntax hints:  ¬ wn 2   → wi 3   ⋀ wa 223

This theorem is referenced by:  pm3.26i 320  pm3.26d 321  pm3.41 327  ancrb 330  pm4.45im 332  anim12i 333  pm4.44 345  adantrd 391  anidm 432  ancom 435  abai 479  anabs1 492  pm3.48 556  ibib 589  ordi 595  pm4.39 629  pm4.38 630  pm4.71 634  intnanr 691  intnanrd 693  biantrud 725  bianfd 737  pm5.75 748  dedlemb 762  nicodraw 950  19.26 1065  19.40 1092  sbequ2 1177  mopick2 1434  moexex 1436  2exeu 1444  2eu2 1448  r19.40 1759  reu3 1927  csbnestglem 2031  csbnest1g 2033  ssab2 2126  uneqin 2252  difprsn 2461  unissel 2522  ssmin 2547  iununi 2611  class2set 2729  moabex 2761  mosubopt 2799  ordsseleq 2971  onin 2973  ordsson 2986  opelxp 3209  ralxp 3213  xpss 3225  opabssxp 3229  dmcosseq 3357  relssres 3384  dminss 3454  cores 3491  fun11uni 3557  dffo4 3811  ffnfv 3819  isotr 3888  isotrALT 3889  isofrlem 3892  f1oiso 3895  tfrlem8 3909  tz7.48lem 3946  fnoprabg 4003  eloprabi 4108  omordi 4187  omord 4189  omlimcl 4199  oneo 4202  oen0 4203  oeordi 4204  oewordri 4209  oeordsuc 4211  eceqopreq 4303  th3qlem1 4304  pw2en 4432  ssenen 4490  unblem2 4524  dfom3 4610  r1ord 4635  r1val1 4638  rankr1 4654  rankuni 4678  rankxplim3 4694  karden 4706  hta 4708  aceq3 4713  kmlem8 4752  kmlem16 4760  brdom7disj 4784  brdom6disj 4785  unidom 4788  cardalephex 4866  axunnd 4928  axacndlem1 4939  axacndlem3 4941  enqeceq 5027  distrpq 5047  genpnnp 5088  addclprlem2 5099  distrlem4pr 5110  prlem936 5135  reclem3pr 5138  suplem2pr 5142  enreceq 5157  mulcmpblnr 5163  pncan3t 5357  0re 5420  leltnet 5502  xrleltnet 5539  ltsubpost 5634  posdift 5635  subge0t 5655  recextlem1 5663  recid2t 5707  divcan5t 5745  divdivdivt 5749  divdivmult 5759  ltmul12it 5805  lemul12itOLD 5807  mulgt1t 5809  lt2mul2divt 5830  ltdiv2t 5843  ledivdivt 5846  lediv2t 5847  recp1lt1 5857  recrecltt 5858  ledivp1t 5861  1nn 5890  nnleltp1t 5909  avglet 5999  nnreclt 6027  flwordit 6191  ceilet 6201  qrecclt 6219  seq1rn2 6266  ser1add2 6283  ser1add 6284  elioo3g 6325  elfz2t 6412  elfzlem 6413  elfz2nn0t 6435  fzaddelt 6440  fzrev2t 6452  fsequb 6463  seqzp1 6488  seqzrn2 6496  expeq0t 6525  expgt0t 6528  expgt1t 6531  mulexpt 6533  recexpt 6534  subsqt 6581  bernneq 6591  creur 6681  replimt 6700  cjexpt 6760  absexpt 6811  cvganz 6869  facavgt 6900  fsumsplit 6966  fsumadd 6968  fsumcom 6974  fsumrev 6975  fsumdivcALT 6982  fsumcmp0 6987  fsumcmpndx2 6988  serzmulc1 7003  bcxmas 7022  clm3 7025  clm4le 7027  climge0 7057  climaddlem3 7060  climaddc1 7062  climmullem8 7071  climmulc2 7073  climsubc2 7075  iserzmulc1 7080  climcmpc1 7083  climsqueeze 7084  climsqueeze2 7085  caucvglem2 7102  caucvglem4 7104  caucvglem5 7105  caucvglem6 7106  iserzgt0 7154  infcvglem3 7166  georeclim 7183  geoisumr 7186  geoisum1c 7188  cvgratlem1 7193  cncfval 7207  ivthlem7 7230  ivthlem7OLD 7239  efaddlem10 7297  efaddlem23 7310  efaddlem25 7312  efexpt 7322  acdc2lem2 7439  acdc5lem2 7442  infmap2lem1 7529  infmap2lem2 7530  gch-kn 7537  basgen2t 7589  indistop 7598  fctop 7600  cctop 7602  clscld 7633  elcls 7654  ntrcls0 7657  neii1 7671  neissex 7688  islp2 7697  ismsg 7750  meteq0 7762  blin 7804  blss 7805  opnfss 7810  lpbl 7832  metcnplem 7838  metcnpi3 7844  metcnpi4 7845  metcni2 7847  tgioolem 7866  dscmet 7870  lmbr 7880  lmnn 7887  lmuni 7902  lmsslem 7903  metelcls 7916  bcthlem8 7956  bcthlem10 7958  bcthlem17 7965  bcthlem26 7974  isgrp 7991  grpidinvlem2 7999  grpidinv 8002  grpinveu 8014  grpinv 8019  grpdivdiv 8037  grpmuldivass 8038  grppnpcan2 8042  abldivdiv4 8061  ringsn 8115  vcid 8122  vcdi 8123  vcdir 8124  nvzs 8217  nvmf 8218  nvmdi 8222  nvmtri2 8252  imsmetlem 8274  nmoub3i 8381  nmlno0lem 8398  nmblolbii 8403  ipdi 8447  ipassr 8450  ipsubdi 8453  ip2eqi 8461  ubthlem8 8480  ubthlem9 8481  ubthlem10 8482  ubthlem11 8483  pstr 8594  efif1lem3 8666  shftefif1olem 8680  hvaddsub4t 8884  norm1t 9060  norm1ex 9061  hhsscms 9089  chocuni 9111  occllem6 9117  projlem26 9150  pjtheu 9173  chabs1t 9377  normcant 9439  pjspansnt 9440  h1datom 9444  pjoml5t 9496  osumlem7 9524  5oalem1 9539  5oalem2 9540  5oalem5 9543  3oalem2 9548  pjidt 9580  pjds3 9598  nmopub2tALT 9773  cnvunopt 9781  unoplint 9783  counopt 9784  nmfnleub2t 9789  hmoplint 9805  nmlnop0ALT 9858  nmbdoplb 9887  nmcopexlem5 9893  nmcoplb 9896  nmbdfnlb 9916  nmcfnexlem5 9922  nmcfnlb 9925  riesz3 9933  riesz4 9934  cnlnadjeu 9948  adjlnopt 9957  branmfnt 9976  kbass5t 9991  leopsqt 10000  nmopleidt 10010  hmopidmpj 10018  pjclem4 10065  pj3s 10073  stge0t 10089  cvpsst 10150  ssmd2 10176  mdslj1 10183  mdslj2 10184  mdslmd1lem1 10189  mdslmd1lem2 10190  atcvat3 10260  atcvat4 10261  mdsymlem2 10268  mdsymlem3 10269  mdsymlem5 10271  cdj1 10294  hmphre 10453  hmeogrp 10461  fgsb 10480  fgsb2 10485  trnij 10517  homib 10604  icmpmon 10623  immon 10625

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain