Theorem simp1rr 1127

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

Assertion

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

Proof of Theorem simp1rr

Step	Hyp	Ref	Expression
1		simprr 796	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant1 1082	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  f1imass  6521  smo11  7461  zsupss  11777  lsmcv  19141  lspsolvlem  19142  mat2pmatghm  20535  mat2pmatmul  20536  nrmr0reg  21552  plyadd  23973  plymul  23974  coeeu  23981  ax5seglem6  25814  clwwnisshclwwsn  26930  archiabl  29752  mdetpmtr1  29889  sseqval  30450  wsuclem  31773  wsuclemOLD  31774  btwnconn1lem1  32194  btwnconn1lem2  32195  btwnconn1lem12  32205  lshpsmreu  34396  1cvratlt  34760  llnle  34804  lvolex3N  34824  lnjatN  35066  lncvrat  35068  lncmp  35069  cdlemd6  35490  cdlemk19ylem  36218  pellex  37399  limcperiod  39860