Theorem simp1rl 1236

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

Assertion

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

Proof of Theorem simp1rl

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  f1imass  7131  smo11  8179  zsupss  12659  lsmcv  20384  lspsolvlem  20385  mat2pmatghm  21860  mat2pmatmul  21861  plyadd  25359  plymul  25360  coeeu  25367  aannenlem1  25469  logexprlim  26354  ax5seglem6  27283  ax5seg  27287  mdetpmtr1  31752  mdetpmtr2  31753  wsuclem  33798  btwnconn1lem2  34369  btwnconn1lem3  34370  btwnconn1lem4  34371  btwnconn1lem12  34379  lshpsmreu  37102  2llnmat  37517  lvolex3N  37531  lnjatN  37773  pclfinclN  37943  lhpat3  38039  cdlemd6  38196  cdlemfnid  38557  cdlemk19ylem  38923  dihlsscpre  39227  dih1dimb2  39234  dihglblem6  39333  pellex  40637  mullimc  43111  mullimcf  43118  limcperiod  43123  cncfshift  43369  cncfperiod  43374