Theorem simplrl 487

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplrl	⊢ (((φ ∧ (ψ ∧ χ)) ∧ θ) → ψ)

Proof of Theorem simplrl

Step	Hyp	Ref	Expression
1		simpl 102	. 2 ⊢ ((ψ ∧ χ) → ψ)
2	1	ad2antlr 458	1 ⊢ (((φ ∧ (ψ ∧ χ)) ∧ θ) → ψ)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  rmob  2844  f1imass  5356  riota5f  5435  tfrexlem  5889  fopwdom  6246  addcmpblnq  6351  mulcmpblnq  6352  ordpipqqs  6358  addcmpblnq0  6425  mulcmpblnq0  6426  prml  6459  addlocpr  6518  prmuloc  6546  mullocpr  6551  ltexprlemopl  6574  ltexprlemopu  6576  ltexprlemloc  6580  ltexprlemrl  6583  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  aptiprleml  6610  ltmprr  6613  cauappcvgprlemopl  6617  cauappcvgprlemopu  6619  cauappcvgprlemloc  6623  addcmpblnr  6647  mulcmpblnrlemg  6648  mulcmpblnr  6649  ltsrprg  6655  mulgt0sr  6684  axmulcl  6732  cnegexlem1  6963  negeu  6979  add20  7244  apreap  7351  cru  7366  apsym  7370  apcotr  7371  apadd1  7372  apneg  7375  mulext1  7376  mulge0  7383  mulap0  7397  divdivdivap  7451  prodgt0  7579  ltmul12a  7587  lt2mul2div  7606  ledivdiv  7617  lediv12a  7621  qapne  8330  ixxss12  8525  elfz0ubfz0  8732  expivallem  8890  mulexpzap  8929  leexp1a  8943  cjap  9114