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 769	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant1 1133	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  f1imass  7216  smo11  8315  zsupss  12871  lsmcv  20661  lspsolvlem  20662  mat2pmatghm  22116  mat2pmatmul  22117  plyadd  25615  plymul  25616  coeeu  25623  aannenlem1  25725  logexprlim  26610  ax5seglem6  27946  ax5seg  27950  mdetpmtr1  32493  mdetpmtr2  32494  wsuclem  34486  btwnconn1lem2  34749  btwnconn1lem3  34750  btwnconn1lem4  34751  btwnconn1lem12  34759  lshpsmreu  37644  2llnmat  38060  lvolex3N  38074  lnjatN  38316  pclfinclN  38486  lhpat3  38582  cdlemd6  38739  cdlemfnid  39100  cdlemk19ylem  39466  dihlsscpre  39770  dih1dimb2  39777  dihglblem6  39876  pellex  41216  tfsconcatrn  41735  mullimc  43977  mullimcf  43984  limcperiod  43989  cncfshift  44235  cncfperiod  44240