Theorem simp1rl 1237

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

Assertion

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

Proof of Theorem simp1rl

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  f1imass  7134  smo11  8186  zsupss  12676  lsmcv  20401  lspsolvlem  20402  mat2pmatghm  21877  mat2pmatmul  21878  plyadd  25376  plymul  25377  coeeu  25384  aannenlem1  25486  logexprlim  26371  ax5seglem6  27300  ax5seg  27304  mdetpmtr1  31769  mdetpmtr2  31770  wsuclem  33815  btwnconn1lem2  34386  btwnconn1lem3  34387  btwnconn1lem4  34388  btwnconn1lem12  34396  lshpsmreu  37119  2llnmat  37534  lvolex3N  37548  lnjatN  37790  pclfinclN  37960  lhpat3  38056  cdlemd6  38213  cdlemfnid  38574  cdlemk19ylem  38940  dihlsscpre  39244  dih1dimb2  39251  dihglblem6  39350  pellex  40654  mullimc  43128  mullimcf  43135  limcperiod  43140  cncfshift  43386  cncfperiod  43391