Theorem simp2r 1055

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 1050	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl2r  1082  simpr2r  1088  simp12r  1142  simp22r  1148  simp32r  1154  issod  4466  funprg  5434  fsnunf  5918  f1oiso2  6036  tfrlemibxssdm  6602  ecopovtrn  6910  ecopovtrng  6913  dftap2  7624  addassnqg  7756  ltsonq  7772  ltanqg  7774  ltmnqg  7775  addassnq0  7836  recexprlem1ssl  8007  mulasssrg  8132  distrsrg  8133  lttrsr  8136  ltsosr  8138  ltasrg  8144  mulextsr1lem  8154  mulextsr1  8155  axmulass  8247  axdistr  8248  dmdcanap  9061  lediv2  9230  ltdiv23  9231  lediv23  9232  xaddass2  10290  xlt2add  10300  expaddzaplem  11041  expaddzap  11042  expmulzap  11044  expdivap  11049  leisorel  11312  swrdspsleq  11462  pfxeq  11491  ccatopth2  11512  bdtrilem  12031  xrbdtri  12068  fldivndvdslt  12730  prmexpb  12956  pcpremul  13102  pcdiv  13111  pcqmul  13112  pcqdiv  13116  4sqlem12  13211  f1ocpbllem  13691  ercpbl  13712  erlecpbl  13713  cmn4  14199  ablsub4  14208  abladdsub4  14209  mvrf1fi  15215  cnptoprest  15477  ssblps  15663  ssbl  15664  tgqioo  15793  plyadd  15989  plymul  15990  rplogbchbase  16198  dichmul0or  16977