Theorem simp3r 1050

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  simpl3r  1077  simpr3r  1083  simp13r  1137  simp23r  1143  simp33r  1149  issod  4407  tfisi  4676  fvun1  5693  f1oiso2  5944  tfrlem5  6450  tfr1onlembxssdm  6479  tfrcllembxssdm  6492  ecopovtrn  6769  ecopovtrng  6772  dftap2  7425  addassnqg  7557  ltsonq  7573  ltanqg  7575  ltmnqg  7576  addassnq0  7637  mulasssrg  7933  distrsrg  7934  lttrsr  7937  ltsosr  7939  ltasrg  7945  mulextsr1lem  7955  mulextsr1  7956  axmulass  8048  axdistr  8049  reapmul1  8730  mulcanap  8800  mulcanap2  8801  divassap  8825  divdirap  8832  div11ap  8835  apmul1  8923  ltdiv1  9003  ltmuldiv  9009  ledivmul  9012  lemuldiv  9016  lediv2  9026  ltdiv23  9027  lediv23  9028  xaddass2  10054  xlt2add  10064  modqdi  10601  expaddzap  10792  expmulzap  10794  leisorel  11046  resqrtcl  11526  xrbdtri  11773  dvdsgcd  12519  rpexp12i  12663  pythagtriplem4  12777  pythagtriplem11  12783  pythagtriplem13  12785  pcpremul  12802  pceu  12804  pcqmul  12812  pcqdiv  12816  f1ocpbllem  13329  ercpbl  13350  erlecpbl  13351  cmn4  13828  ablsub4  13836  abladdsub4  13837  lidlsubcl  14436  psmetlecl  14993  xmetlecl  15026  xblcntrps  15072  xblcntr  15073