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  6426  mulcmpblnq0  6427  prml  6460  addlocpr  6519  prmuloc  6547  mullocpr  6552  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemloc  6581  ltexprlemrl  6584  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  aptiprleml  6611  ltmprr  6614  cauappcvgprlemopl  6618  cauappcvgprlemopu  6620  cauappcvgprlemloc  6624  caucvgprlemopl  6640  caucvgprlemopu  6642  caucvgprlemloc  6646  addcmpblnr  6667  mulcmpblnrlemg  6668  mulcmpblnr  6669  ltsrprg  6675  mulgt0sr  6704  axmulcl  6752  cnegexlem1  6983  negeu  6999  add20  7264  apreap  7371  cru  7386  apsym  7390  apcotr  7391  apadd1  7392  apneg  7395  mulext1  7396  mulge0  7403  mulap0  7417  divdivdivap  7471  prodgt0  7599  ltmul12a  7607  lt2mul2div  7626  ledivdiv  7637  lediv12a  7641  qapne  8350  ixxss12  8545  elfz0ubfz0  8752  expivallem  8910  mulexpzap  8949  leexp1a  8963  cjap  9134