Theorem simp1rr 1239

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

Assertion

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

Proof of Theorem simp1rr

Step	Hyp	Ref	Expression
1		simprr 772	. 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  nrmr0reg  23778  plyadd  26276  plymul  26277  coeeu  26284  ax5seglem6  28967  archiabl  33178  mdetpmtr1  33769  sseqval  34353  wsuclem  35789  btwnconn1lem1  36051  btwnconn1lem2  36052  btwnconn1lem12  36062  lshpsmreu  39065  1cvratlt  39431  llnle  39475  lvolex3N  39495  lnjatN  39737  lncvrat  39739  lncmp  39740  cdlemd6  40160  cdlemk19ylem  40887  pellex  42791  tfsconcatrn  43304  limcperiod  45549  itschlc0xyqsol1  48500  itschlc0xyqsol  48501