Theorem simp3r 1016

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

Assertion

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

Proof of Theorem simp3r

Step	Hyp	Ref	Expression
1		simpr 109	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant3 1010	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 968

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simpl3r  1043  simpr3r  1049  simp13r  1103  simp23r  1109  simp33r  1115  issod  4297  tfisi  4564  fvun1  5552  f1oiso2  5795  tfrlem5  6282  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  ecopovtrn  6598  ecopovtrng  6601  addassnqg  7323  ltsonq  7339  ltanqg  7341  ltmnqg  7342  addassnq0  7403  mulasssrg  7699  distrsrg  7700  lttrsr  7703  ltsosr  7705  ltasrg  7711  mulextsr1lem  7721  mulextsr1  7722  axmulass  7814  axdistr  7815  reapmul1  8493  mulcanap  8562  mulcanap2  8563  divassap  8586  divdirap  8593  div11ap  8596  apmul1  8684  ltdiv1  8763  ltmuldiv  8769  ledivmul  8772  lemuldiv  8776  lediv2  8786  ltdiv23  8787  lediv23  8788  xaddass2  9806  xlt2add  9816  modqdi  10327  expaddzap  10499  expmulzap  10501  leisorel  10750  resqrtcl  10971  xrbdtri  11217  dvdsgcd  11945  rpexp12i  12087  pythagtriplem4  12200  pythagtriplem11  12206  pythagtriplem13  12208  pcpremul  12225  pceu  12227  pcqmul  12235  pcqdiv  12239  psmetlecl  12974  xmetlecl  13007  xblcntrps  13053  xblcntr  13054