Theorem simp3r 967

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 108	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant3 961	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simpl3r  994  simpr3r  1000  simp13r  1054  simp23r  1060  simp33r  1066  issod  4074  tfisi  4328  fvun1  5260  f1oiso2  5486  tfrlem5  5953  ecopovtrn  6226  ecopovtrng  6229  addassnqg  6572  ltsonq  6588  ltanqg  6590  ltmnqg  6591  addassnq0  6652  mulasssrg  6935  distrsrg  6936  lttrsr  6939  ltsosr  6941  ltasrg  6947  mulextsr1lem  6956  mulextsr1  6957  axmulass  7039  axdistr  7040  reapmul1  7695  mulcanap  7755  mulcanap2  7756  divassap  7778  divdirap  7785  div11ap  7788  apmul1  7876  ltdiv1  7946  ltmuldiv  7952  ledivmul  7955  lemuldiv  7959  lediv2  7969  ltdiv23  7970  lediv23  7971  modqdi  9394  expaddzap  9520  expmulzap  9522  resqrtcl  9915  dvdsgcd  10401  rpexp12i  10534