Theorem simp3r 1010

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

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

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 964

This theorem is referenced by:  simpl3r  1037  simpr3r  1043  simp13r  1097  simp23r  1103  simp33r  1109  issod  4236  tfisi  4496  fvun1  5480  f1oiso2  5721  tfrlem5  6204  tfr1onlembxssdm  6233  tfrcllembxssdm  6246  ecopovtrn  6519  ecopovtrng  6522  addassnqg  7183  ltsonq  7199  ltanqg  7201  ltmnqg  7202  addassnq0  7263  mulasssrg  7559  distrsrg  7560  lttrsr  7563  ltsosr  7565  ltasrg  7571  mulextsr1lem  7581  mulextsr1  7582  axmulass  7674  axdistr  7675  reapmul1  8350  mulcanap  8419  mulcanap2  8420  divassap  8443  divdirap  8450  div11ap  8453  apmul1  8541  ltdiv1  8619  ltmuldiv  8625  ledivmul  8628  lemuldiv  8632  lediv2  8642  ltdiv23  8643  lediv23  8644  xaddass2  9646  xlt2add  9656  modqdi  10158  expaddzap  10330  expmulzap  10332  leisorel  10573  resqrtcl  10794  xrbdtri  11038  dvdsgcd  11689  rpexp12i  11822  psmetlecl  12492  xmetlecl  12525  xblcntrps  12571  xblcntr  12572