Theorem simp1r 1025

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1r	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Proof of Theorem simp1r

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2ant1 1021	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  simpl1r  1052  simpr1r  1058  simp11r  1112  simp21r  1118  simp31r  1124  vtoclgft  2825  en2lp  4607  funprg  5330  nnsucsssuc  6588  ecopovtrn  6729  ecopovtrng  6732  addassnqg  7508  distrnqg  7513  ltsonq  7524  ltanqg  7526  ltmnqg  7527  distrnq0  7585  addassnq0  7588  prarloclem5  7626  recexprlem1ssl  7759  recexprlem1ssu  7760  mulasssrg  7884  distrsrg  7885  lttrsr  7888  ltsosr  7890  ltasrg  7896  mulextsr1lem  7906  mulextsr1  7907  axmulass  7999  axdistr  8000  dmdcanap  8808  lt2msq1  8971  lediv2  8977  xaddass2  10005  xlt2add  10015  modqdi  10550  expaddzaplem  10740  expaddzap  10741  expmulzap  10743  swrdspsleq  11134  pfxeq  11161  bdtrilem  11600  xrbdtri  11637  bitsfzo  12316  prmexpb  12523  4sqlem18  12781  mgmsscl  13243  subgabl  13718  cnptoprest  14761  ssblps  14947  ssbl  14948  rplogbchbase  15472  rplogbreexp  15475  relogbcxpbap  15487  lgssq  15567