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  7205  smo11  8294  zsupss  12856  lsmcv  21066  lspsolvlem  21067  mat2pmatghm  22633  mat2pmatmul  22634  plyadd  26138  plymul  26139  coeeu  26146  aannenlem1  26252  logexprlim  27152  ax5seglem6  28897  ax5seg  28901  mdetpmtr1  33792  mdetpmtr2  33793  wsuclem  35801  btwnconn1lem2  36064  btwnconn1lem3  36065  btwnconn1lem4  36066  btwnconn1lem12  36074  lshpsmreu  39090  2llnmat  39506  lvolex3N  39520  lnjatN  39762  pclfinclN  39932  lhpat3  40028  cdlemd6  40185  cdlemfnid  40546  cdlemk19ylem  40912  dihlsscpre  41216  dih1dimb2  41223  dihglblem6  41322  pellex  42811  tfsconcatrn  43318  mullimc  45601  mullimcf  45608  limcperiod  45613  cncfshift  45859  cncfperiod  45864