Theorem simp3r 1021

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

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

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 975

This theorem is referenced by:  simpl3r  1048  simpr3r  1054  simp13r  1108  simp23r  1114  simp33r  1120  issod  4302  tfisi  4569  fvun1  5560  f1oiso2  5804  tfrlem5  6291  tfr1onlembxssdm  6320  tfrcllembxssdm  6333  ecopovtrn  6608  ecopovtrng  6611  addassnqg  7337  ltsonq  7353  ltanqg  7355  ltmnqg  7356  addassnq0  7417  mulasssrg  7713  distrsrg  7714  lttrsr  7717  ltsosr  7719  ltasrg  7725  mulextsr1lem  7735  mulextsr1  7736  axmulass  7828  axdistr  7829  reapmul1  8507  mulcanap  8576  mulcanap2  8577  divassap  8600  divdirap  8607  div11ap  8610  apmul1  8698  ltdiv1  8777  ltmuldiv  8783  ledivmul  8786  lemuldiv  8790  lediv2  8800  ltdiv23  8801  lediv23  8802  xaddass2  9820  xlt2add  9830  modqdi  10341  expaddzap  10513  expmulzap  10515  leisorel  10765  resqrtcl  10986  xrbdtri  11232  dvdsgcd  11960  rpexp12i  12102  pythagtriplem4  12215  pythagtriplem11  12221  pythagtriplem13  12223  pcpremul  12240  pceu  12242  pcqmul  12250  pcqdiv  12254  psmetlecl  13093  xmetlecl  13126  xblcntrps  13172  xblcntr  13173