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  6603  ecopovtrn  6911  ecopovtrng  6914  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  10289  xlt2add  10299  expaddzaplem  11040  expaddzap  11041  expmulzap  11043  expdivap  11048  leisorel  11311  swrdspsleq  11461  pfxeq  11490  ccatopth2  11511  bdtrilem  12030  xrbdtri  12067  fldivndvdslt  12729  prmexpb  12955  pcpremul  13101  pcdiv  13110  pcqmul  13111  pcqdiv  13115  4sqlem12  13210  f1ocpbllem  13690  ercpbl  13711  erlecpbl  13712  cmn4  14198  ablsub4  14207  abladdsub4  14208  mvrf1fi  15231  cnptoprest  15498  ssblps  15684  ssbl  15685  tgqioo  15814  plyadd  16010  plymul  16011  rplogbchbase  16219  dichmul0or  16998