Theorem simp1rl 1238

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

Assertion

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

Proof of Theorem simp1rl

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

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  f1imass  7301  smo11  8420  zsupss  13002  lsmcv  21166  lspsolvlem  21167  mat2pmatghm  22757  mat2pmatmul  22758  plyadd  26276  plymul  26277  coeeu  26284  aannenlem1  26388  logexprlim  27287  ax5seglem6  28967  ax5seg  28971  mdetpmtr1  33769  mdetpmtr2  33770  wsuclem  35789  btwnconn1lem2  36052  btwnconn1lem3  36053  btwnconn1lem4  36054  btwnconn1lem12  36062  lshpsmreu  39065  2llnmat  39481  lvolex3N  39495  lnjatN  39737  pclfinclN  39907  lhpat3  40003  cdlemd6  40160  cdlemfnid  40521  cdlemk19ylem  40887  dihlsscpre  41191  dih1dimb2  41198  dihglblem6  41297  pellex  42791  tfsconcatrn  43304  mullimc  45537  mullimcf  45544  limcperiod  45549  cncfshift  45795  cncfperiod  45800