Theorem simp2r 1027

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

Assertion

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

Proof of Theorem simp2r

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant2 1022	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:  simpl2r  1054  simpr2r  1060  simp12r  1114  simp22r  1120  simp32r  1126  issod  4371  funprg  5330  fsnunf  5794  f1oiso2  5906  tfrlemibxssdm  6423  ecopovtrn  6729  ecopovtrng  6732  dftap2  7376  addassnqg  7508  ltsonq  7524  ltanqg  7526  ltmnqg  7527  addassnq0  7588  recexprlem1ssl  7759  mulasssrg  7884  distrsrg  7885  lttrsr  7888  ltsosr  7890  ltasrg  7896  mulextsr1lem  7906  mulextsr1  7907  axmulass  7999  axdistr  8000  dmdcanap  8808  lediv2  8977  ltdiv23  8978  lediv23  8979  xaddass2  10005  xlt2add  10015  expaddzaplem  10740  expaddzap  10741  expmulzap  10743  expdivap  10748  leisorel  10995  swrdspsleq  11134  pfxeq  11161  bdtrilem  11600  xrbdtri  11637  fldivndvdslt  12298  prmexpb  12523  pcpremul  12666  pcdiv  12675  pcqmul  12676  pcqdiv  12680  4sqlem12  12775  f1ocpbllem  13192  ercpbl  13213  erlecpbl  13214  cmn4  13691  ablsub4  13699  abladdsub4  13700  cnptoprest  14761  ssblps  14947  ssbl  14948  tgqioo  15077  plyadd  15273  plymul  15274  rplogbchbase  15472