Theorem simp3r 1053

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

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

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 1007

This theorem is referenced by:  simpl3r  1080  simpr3r  1086  simp13r  1140  simp23r  1146  simp33r  1152  issod  4422  tfisi  4691  fvun1  5721  f1oiso2  5978  tfrlem5  6523  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  ecopovtrn  6844  ecopovtrng  6847  dftap2  7513  addassnqg  7645  ltsonq  7661  ltanqg  7663  ltmnqg  7664  addassnq0  7725  mulasssrg  8021  distrsrg  8022  lttrsr  8025  ltsosr  8027  ltasrg  8033  mulextsr1lem  8043  mulextsr1  8044  axmulass  8136  axdistr  8137  reapmul1  8818  mulcanap  8888  mulcanap2  8889  divassap  8913  divdirap  8920  div11ap  8923  apmul1  9011  ltdiv1  9091  ltmuldiv  9097  ledivmul  9100  lemuldiv  9104  lediv2  9114  ltdiv23  9115  lediv23  9116  xaddass2  10148  xlt2add  10158  modqdi  10698  expaddzap  10889  expmulzap  10891  leisorel  11145  resqrtcl  11650  xrbdtri  11897  dvdsgcd  12644  rpexp12i  12788  pythagtriplem4  12902  pythagtriplem11  12908  pythagtriplem13  12910  pcpremul  12927  pceu  12929  pcqmul  12937  pcqdiv  12941  f1ocpbllem  13454  ercpbl  13475  erlecpbl  13476  cmn4  13953  ablsub4  13961  abladdsub4  13962  lidlsubcl  14563  psmetlecl  15125  xmetlecl  15158  xblcntrps  15204  xblcntr  15205