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  4411  tfisi  4680  fvun1  5705  f1oiso2  5960  tfrlem5  6471  tfr1onlembxssdm  6500  tfrcllembxssdm  6513  ecopovtrn  6792  ecopovtrng  6795  dftap2  7453  addassnqg  7585  ltsonq  7601  ltanqg  7603  ltmnqg  7604  addassnq0  7665  mulasssrg  7961  distrsrg  7962  lttrsr  7965  ltsosr  7967  ltasrg  7973  mulextsr1lem  7983  mulextsr1  7984  axmulass  8076  axdistr  8077  reapmul1  8758  mulcanap  8828  mulcanap2  8829  divassap  8853  divdirap  8860  div11ap  8863  apmul1  8951  ltdiv1  9031  ltmuldiv  9037  ledivmul  9040  lemuldiv  9044  lediv2  9054  ltdiv23  9055  lediv23  9056  xaddass2  10083  xlt2add  10093  modqdi  10631  expaddzap  10822  expmulzap  10824  leisorel  11077  resqrtcl  11561  xrbdtri  11808  dvdsgcd  12554  rpexp12i  12698  pythagtriplem4  12812  pythagtriplem11  12818  pythagtriplem13  12820  pcpremul  12837  pceu  12839  pcqmul  12847  pcqdiv  12851  f1ocpbllem  13364  ercpbl  13385  erlecpbl  13386  cmn4  13863  ablsub4  13871  abladdsub4  13872  lidlsubcl  14472  psmetlecl  15029  xmetlecl  15062  xblcntrps  15108  xblcntr  15109