Theorem simp3r 1027

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

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

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 981

This theorem is referenced by:  simpl3r  1054  simpr3r  1060  simp13r  1114  simp23r  1120  simp33r  1126  issod  4333  tfisi  4600  fvun1  5597  f1oiso2  5843  tfrlem5  6332  tfr1onlembxssdm  6361  tfrcllembxssdm  6374  ecopovtrn  6649  ecopovtrng  6652  dftap2  7267  addassnqg  7398  ltsonq  7414  ltanqg  7416  ltmnqg  7417  addassnq0  7478  mulasssrg  7774  distrsrg  7775  lttrsr  7778  ltsosr  7780  ltasrg  7786  mulextsr1lem  7796  mulextsr1  7797  axmulass  7889  axdistr  7890  reapmul1  8569  mulcanap  8639  mulcanap2  8640  divassap  8664  divdirap  8671  div11ap  8674  apmul1  8762  ltdiv1  8842  ltmuldiv  8848  ledivmul  8851  lemuldiv  8855  lediv2  8865  ltdiv23  8866  lediv23  8867  xaddass2  9887  xlt2add  9897  modqdi  10409  expaddzap  10581  expmulzap  10583  leisorel  10834  resqrtcl  11055  xrbdtri  11301  dvdsgcd  12030  rpexp12i  12172  pythagtriplem4  12285  pythagtriplem11  12291  pythagtriplem13  12293  pcpremul  12310  pceu  12312  pcqmul  12320  pcqdiv  12324  f1ocpbllem  12752  ercpbl  12772  erlecpbl  12773  cmn4  13204  ablsub4  13212  abladdsub4  13213  lidlsubcl  13763  psmetlecl  14217  xmetlecl  14250  xblcntrps  14296  xblcntr  14297