Theorem pm3.26 317

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 223	. 2 ⊢ ((φ ⋀ ψ) ↔ ¬ (φ → ¬ ψ))
2		pm3.26im 137	. 2 ⊢ (¬ (φ → ¬ ψ) → φ)
3	1, 2	sylbi 197	1 ⊢ ((φ ⋀ ψ) → φ)

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

This theorem is referenced by:  pm3.26i 318  pm3.26d 319  pm3.41 325  ancrb 328  pm4.45im 330  anim12i 331  pm4.44 343  adantrd 391  anidm 433  ancom 437  abai 482  anabs1 495  pm3.48 560  ibib 593  ordi 599  pm4.39 633  pm4.38 634  pm4.71 638  intnanr 696  intnanrd 698  biantrud 731  bianfd 743  pm5.75 754  dedlemb 768  nic-ax 969  nic-axALT 970  19.26 1103  19.40 1130  sbequ2 1216  mopick2 1476  moexex 1478  2exeu 1486  2eu2 1490  r19.40 1808  reu3 1977  csbnestglem 2087  csbnest1g 2089  ssab2 2182  uneqin 2308  difprsn 2529  unissel 2594  ssmin 2619  iununi 2686  class2set 2808  moabex 2844  mosubopt 2881  posn 2928  ordsseleq 3004  onin 3006  suctr 3055  ordsson 3145  opelxp 3297  ralxp 3301  xpss 3316  opabssxp 3320  dmcosseq 3452  relssres 3482  dminss 3547  cores 3602  fun11uni 3670  dffo4 3934  ffnfv 3942  isotr 4011  isotrALT 4012  isofrlem 4015  f1oiso 4018  fnoprabg 4072  eloprabi 4180  curry2val 4198  tfrlem8 4219  tz7.48lem 4256  omordi 4333  omord 4335  omlimcl 4345  oneo 4348  oen0 4349  oeordi 4350  oewordri 4355  oeordsuc 4357  eceqopreq 4454  th3qlem1 4455  pw2en 4587  ac6sfilem3 4590  ssenen 4651  unblem2 4687  dfom3 4776  r1ord 4801  r1val1 4804  rankr1 4820  rankuni 4844  rankxplim3 4860  karden 4872  hta 4874  aceq3 4879  kmlem8 4918  kmlem16 4926  brdom7disj 4950  brdom6disj 4951  unidom 4954  cardalephex 5036  axunnd 5102  axacndlem1 5113  axacndlem3 5115  enqeceq 5201  distrpq 5221  genpnnp 5262  addclprlem2 5273  distrlem4pr 5284  prlem936 5309  reclem3pr 5312  suplem2pr 5316  enreceq 5331  mulcmpblnr 5337  pncan3 5531  0re 5594  leltne 5675  xrleltne 5712  ltsubpos 5807  posdif 5808  subge0 5828  recextlem1 5838  recid2 5882  divcan5 5920  divdivdiv 5924  lemul2aOLD 5984  lemul12aOLD 5987  mulgt1 5989  lt2mul2div 6016  lt2mul2divOLD 6017  ltdiv2 6032  ledivdiv 6035  lediv2 6036  ltdiv23 6037  lediv23 6038  recp1lt1 6046  recreclt 6047  ledivp1 6050  1nn 6079  nnleltp1 6100  avgle 6190  rpneg 6211  nnrecl 6240  qreccl 6412  flwordi 6436  flbi2 6440  ceile 6450  quoremz 6451  quoremnn0ALT 6452  quoremnn0 6453  intfracq 6455  fldiv2 6457  modge0 6462  elioo3g 6506  elfz2 6600  elfzlem 6601  elfz2nn0 6625  fzaddel 6630  fzrev2 6643  fsequb 6654  seq1rn2 6686  ser1add2i 6703  ser1addi 6704  seqzp1 6743  seqzrn2 6751  expeq0 6780  expgt0 6783  expgt1 6786  mulexp 6788  exprecOLD 6790  subsq 6839  bernneq 6849  bernneqOLD 6850  digit1 6856  creur 6943  replim 6962  cjexp 7018  absexp 7070  absmax 7100  cvganz 7127  facavg 7158  fsumsplit 7223  fsumadd 7225  fsumcom 7231  fsumrev 7232  fsumdivcALT 7239  fsumcmp0 7244  fsumcmpndx2 7245  serzmulc1 7260  bcxmas 7279  clm3i 7282  clm4lei 7284  climge0 7315  climaddlem3 7319  climaddc1 7321  climmullem8 7330  climmulc2 7332  climsubc2 7334  iserzmulc1 7339  climcmpc1 7342  climsqueeze 7343  climsqueeze2 7344  caucvglem2 7361  caucvglem4 7363  caucvglem5 7364  caucvglem6 7365  iserzgt0 7415  infcvglem3 7427  explecnv 7438  georeclim 7445  geoisumr 7448  cvgratlem1 7455  cncfval 7469  ivthlem7 7492  efaddlem10 7552  efaddlem23 7565  efaddlem25 7567  efexp 7577  acdc2lem2 7701  acdc5lem2 7704  infmap2lem1 7791  infmap2lem2 7792  gch-kn 7799  basgen2 7851  indistop 7860  cctop 7862  clscld 7893  elcls 7914  ntrcls0 7917  neii1 7931  neissex 7948  islp2 7957  ismsg 8010  meteq0 8022  blin 8062  blss 8063  opnfss 8068  lpbl 8090  metcnplem 8097  metcnpi3 8103  metcnpi4 8104  metcni2 8106  tgioolem 8125  dscmet 8129  lmbr 8139  lmnn 8146  lmuni 8162  lmsslem 8163  metelcls 8176  bcthlem8 8217  bcthlem10 8219  bcthlem17 8226  bcthlem26 8235  isgrp 8254  grpidinvlem2 8262  grpidinv 8265  grprlidrid 8270  grpinveu 8281  grpinv 8286  grpdivdiv 8305  grpmuldivass 8306  grppnpcan2 8310  gxneg 8322  gxsuc 8328  gxid 8329  gxadd 8331  gxnn0mul 8333  gxmul 8334  gxmodid 8335  abldivdiv4 8350  ringideu 8387  ringsn 8405  vcid 8417  vcdi 8418  vcdir 8419  nvzs 8512  nvmf 8513  nvmdi 8517  nvmtri2 8547  imsmetlem 8570  vacnlem6 8587  nmoub3i 8690  nmlno0lem 8708  nmblolbii 8714  ipdi 8759  ipassr 8762  ipsubdi 8765  ip2eqi 8773  ubthlem8 8794  ubthlem9 8795  ubthlem10 8796  ubthlem11 8797  pstr 8914  laspwcl 8930  efif1lem3 9004  shftefif1olem 9013  grothpw 9054  hvaddsub4 9221  norm1 9397  norm1exi 9398  hhsscms 9426  chocunii 9448  occllem6 9454  projlem26 9487  pjtheui 9511  chabs1 9715  normcan 9775  pjspansn 9776  h1datomi 9780  pjoml5 9832  osumlem7 9862  5oalem1 9877  5oalem2 9878  5oalem5 9881  3oalem2 9886  pjid 9918  pjds3i 9936  nmopub2tALT 10113  cnvunop 10122  unoplin 10124  counop 10125  nmfnleub2 10130  hmoplin 10146  nmlnop0iALT 10199  nmbdoplbi 10228  nmcopexlem5 10234  nmcoplbi 10237  nmbdfnlbi 10257  nmcfnexlem5 10263  nmcfnlbi 10266  riesz3i 10274  riesz4i 10275  cnlnadjeui 10289  adjlnop 10298  branmfn 10317  branmfnOLD 10318  kbass5 10333  leopsq 10342  nmopleid 10352  hmopidmpji 10360  pjclem4 10408  pj3si 10416  stge0 10432  cvpss 10493  ssmd2 10520  mdslj1i 10527  mdslj2i 10528  mdslmd1lem1 10533  mdslmd1lem2 10534  atcvat3i 10605  atcvat4i 10606  mdsymlem2 10613  mdsymlem3 10614  mdsymlem5 10616  cdj1i 10642  inttr 10787  restidsing 10805  jidd 10840  midd 10841  definc 10869  domncnt 10872  ranncnt 10873  toplat 10884  smgrpmgm 10912  grpmnd 10933  uridm 10956  zerab 10957  isdivrng 10968  zrdivrng 10969  truni3 11001  cbci 11003  oibbi1 11004  oibbi2 11005  hmphre 11036  hmeogrp 11044  stoig 11064  subtopsin2 11067  fgsb 11082  fgsb2 11086  rcfpfillem3 11091  trnij 11160  dmrngcmp 11205  homib 11251  icmpmon 11271  immon 11273  idfisf 11295  subctct 11308  simplll 11362  simplrl 11364  simprll 11366  simprrl 11368  r19.2zb 11393  ordiso 11426  ordtypelem7 11433  hartog 11436  infenomsub 11450  opnregcld 11467  cldregopn 11468  neiin 11470  hausnei2 11471  cncls 11473  subcld 11480  cnsubsp 11483  compsublem 11487  cptclsscpt 11489  cncomp 11494  alexsublem2 11497  connsub 11502  subtopmetlem 11505  subtopmet 11506  isfne 11541  isref 11549  fnessref 11564  islocfin 11567  finlocfin 11570  neibastop2lem2 11581  neibastop2 11584  neibastop3 11585  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  opnfbas 11629  extbas1 11641  supfil 11645  fixufil 11661  ufinffr 11663  ufilen 11664  neiplim 11681  limfilcf 11683  cnpfillim 11686  isflimf 11709  isfclus 11718  flimfcls 11725  fclsfnflim 11726  flimfnfcls 11727  fcluscomplem 11732  fcluscomp 11733  filnetlem1 11763  filnetlem4 11766  gafo 11773  isga2 11774  gaid 11776  gagrpid 11780  gapmlem 11783  difxp 11798  fimax 11837  sdclem1 11875  sdc 11877  fsum00 11883  fsumlt1 11894  blssp 11908  metsstop 11909  mettrifi2 11913  iccshftr 11922  iccshftl 11924  iccdil 11926  icccntr 11928  cnres 11950  cnresima 11952  paste 11954  tx1cn 11976  txsubsp 11983  ismtyhmeolem 12006  heiborlem10 12020  heiborlem25 12035  heiborlem26 12036  heiborlem28 12038  heiborlem29 12039  heiborlem36 12046  rrnmet 12072  phtpyid 12091  phtpycom 12092  phtpycolem3 12095

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 145  df-an 223

Copyright terms: Public domain