Theorem simplr 415

Description: Simplification of a conjunction.

Assertion

Ref	Expression
simplr	⊢ (((φ ⋀ ψ) ⋀ χ) → ψ)

Proof of Theorem simplr

Step	Hyp	Ref	Expression
1		id 59	. 2 ⊢ (ψ → ψ)
2	1	ad2antlr 407	1 ⊢ (((φ ⋀ ψ) ⋀ χ) → ψ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  ax11indalem 1370  ax11inda2ALT 1371  reuuniss2 2897  ordelord 2976  fvelimab 3771  odi 4216  omsmo 4263  onomeneq 4525  noinfep 4650  prpssnq 5106  cnegextlem2 5358  cnegextlem3 5359  divmuldivt 5782  divdivmult 5797  ltmul12it 5843  lemulge11t 5850  lediv12it 5898  lediv2it 5899  nndivt 5961  zltp1let 6183  iccsupr 6399  elfzelz 6483  fzrevt 6512  fzrev3t 6515  fsequb2 6525  expmult 6598  expnbndt 6655  seq1bnd 6910  caubnd 6926  fsumsplit 7020  fsumcom 7028  fsumdivc 7035  clm4le 7081  climcmpc1 7139  climsqueeze 7140  climsqueeze2 7141  cvgratlem2 7251  cvgratlem5 7254  opnssneib 7726  clslp 7745  cnpco 7766  iscncl 7767  dnsconst 7785  blval 7834  blcntr 7842  blelrn 7845  ssblex 7853  lpbl 7877  metcnplem 7883  metcnp 7884  tgioolem 7911  lmconst 7931  lmnn 7932  iscau3 7935  iscau4 7937  xplm 7972  cmsss 7994  bcthlem2 7997  grpidinvlem4 8048  grprid 8058  abl4 8101  nmcnilem 8333  sm1cnilem 8343  nvcnpi3 8418  nvcnpi4 8419  ubthlem5 8529  spwpr4OLD 8658  spwpr4aOLD 8659  hvmul0ort 8889  hhsscms 9145  spansncol 9486  osumlem6 9578  3oalem2 9603  eigpos 9757  hhlno 9821  unoplint 9839  hmoplint 9861  hmopcot 9943  lnopcon 9958  lnfncon 9985  cnlnadjlem6 10000  kbass4t 10047  nmopleidt 10067  dmdbr2 10225  dmdbr5 10230  mdslmd1lem1 10247  mdslmd1lem2 10248  superpos 10276  irredlem1 10312  qusp 10541  iintlem1 10603  imonclem 10712  ismonc 10713  icmpmon 10715  idmon 10716

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