Theorem simp1rl 1239

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

This theorem is referenced by:  f1imass  7206  smo11  8292  zsupss  12839  lsmcv  21082  lspsolvlem  21083  mat2pmatghm  22648  mat2pmatmul  22649  plyadd  26152  plymul  26153  coeeu  26160  aannenlem1  26266  logexprlim  27166  ax5seglem6  28916  ax5seg  28920  mdetpmtr1  33859  mdetpmtr2  33860  wsuclem  35890  btwnconn1lem2  36155  btwnconn1lem3  36156  btwnconn1lem4  36157  btwnconn1lem12  36165  lshpsmreu  39231  2llnmat  39646  lvolex3N  39660  lnjatN  39902  pclfinclN  40072  lhpat3  40168  cdlemd6  40325  cdlemfnid  40686  cdlemk19ylem  41052  dihlsscpre  41356  dih1dimb2  41363  dihglblem6  41462  pellex  42955  tfsconcatrn  43462  mullimc  45743  mullimcf  45750  limcperiod  45755  cncfshift  45999  cncfperiod  46004