Theorem simp1rl 1119

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp1rl	⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Proof of Theorem simp1rl

Step	Hyp	Ref	Expression
1		simprl 790	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant1 1075	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  f1imass  6422  smo11  7348  zsupss  11653  lsmcv  18962  lspsolvlem  18963  mat2pmatghm  20354  mat2pmatmul  20355  plyadd  23777  plymul  23778  coeeu  23785  aannenlem1  23887  logexprlim  24750  ax5seglem6  25614  ax5seg  25618  mdetpmtr1  29217  mdetpmtr2  29218  wsuclem  31017  wsuclemOLD  31018  btwnconn1lem2  31365  btwnconn1lem3  31366  btwnconn1lem4  31367  btwnconn1lem12  31375  lshpsmreu  33414  2llnmat  33828  lvolex3N  33842  lnjatN  34084  pclfinclN  34254  lhpat3  34350  cdlemd6  34508  cdlemfnid  34870  cdlemk19ylem  35236  dihlsscpre  35541  dih1dimb2  35548  dihglblem6  35647  pellex  36417  mullimc  38683  mullimcf  38690  limcperiod  38695  cncfshift  38759  cncfperiod  38764