Theorem simp3l 932

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

Assertion

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

Proof of Theorem simp3l

Step	Hyp	Ref	Expression
1		simpl 102	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant3 927	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  simpl3l  959  simpr3l  965  simp13l  1019  simp23l  1025  simp33l  1031  issod  4056  tfisi  4310  tfrlem5  5930  tfrlemibxssdm  5941  ecopovtrn  6203  ecopovtrng  6206  addassnqg  6480  ltsonq  6496  ltanqg  6498  ltmnqg  6499  addassnq0  6560  mulasssrg  6843  distrsrg  6844  lttrsr  6847  ltsosr  6849  ltasrg  6855  mulextsr1lem  6864  mulextsr1  6865  axmulass  6947  axdistr  6948  lemul1  7584  reapmul1lem  7585  reapmul1  7586  mulcanap  7646  mulcanap2  7647  divassap  7669  divdirap  7674  div11ap  7677  divcanap5  7690  apmul1  7764  ltdiv1  7834  ltmuldiv  7840  ledivmul  7843  lemuldiv  7847  ltdiv2  7853  lediv2  7857  ltdiv23  7858  lediv23  7859  expaddzap  9299  expmulzap  9301  resqrtcl  9627