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  4414  tfisi  4683  fvun1  5708  f1oiso2  5963  tfrlem5  6475  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  ecopovtrn  6796  ecopovtrng  6799  dftap2  7463  addassnqg  7595  ltsonq  7611  ltanqg  7613  ltmnqg  7614  addassnq0  7675  mulasssrg  7971  distrsrg  7972  lttrsr  7975  ltsosr  7977  ltasrg  7983  mulextsr1lem  7993  mulextsr1  7994  axmulass  8086  axdistr  8087  reapmul1  8768  mulcanap  8838  mulcanap2  8839  divassap  8863  divdirap  8870  div11ap  8873  apmul1  8961  ltdiv1  9041  ltmuldiv  9047  ledivmul  9050  lemuldiv  9054  lediv2  9064  ltdiv23  9065  lediv23  9066  xaddass2  10098  xlt2add  10108  modqdi  10647  expaddzap  10838  expmulzap  10840  leisorel  11094  resqrtcl  11583  xrbdtri  11830  dvdsgcd  12576  rpexp12i  12720  pythagtriplem4  12834  pythagtriplem11  12840  pythagtriplem13  12842  pcpremul  12859  pceu  12861  pcqmul  12869  pcqdiv  12873  f1ocpbllem  13386  ercpbl  13407  erlecpbl  13408  cmn4  13885  ablsub4  13893  abladdsub4  13894  lidlsubcl  14494  psmetlecl  15051  xmetlecl  15084  xblcntrps  15130  xblcntr  15131