Theorem simp3r 1026

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

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

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 980

This theorem is referenced by:  simpl3r  1053  simpr3r  1059  simp13r  1113  simp23r  1119  simp33r  1125  issod  4321  tfisi  4588  fvun1  5584  f1oiso2  5830  tfrlem5  6317  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  ecopovtrn  6634  ecopovtrng  6637  dftap2  7252  addassnqg  7383  ltsonq  7399  ltanqg  7401  ltmnqg  7402  addassnq0  7463  mulasssrg  7759  distrsrg  7760  lttrsr  7763  ltsosr  7765  ltasrg  7771  mulextsr1lem  7781  mulextsr1  7782  axmulass  7874  axdistr  7875  reapmul1  8554  mulcanap  8624  mulcanap2  8625  divassap  8649  divdirap  8656  div11ap  8659  apmul1  8747  ltdiv1  8827  ltmuldiv  8833  ledivmul  8836  lemuldiv  8840  lediv2  8850  ltdiv23  8851  lediv23  8852  xaddass2  9872  xlt2add  9882  modqdi  10394  expaddzap  10566  expmulzap  10568  leisorel  10819  resqrtcl  11040  xrbdtri  11286  dvdsgcd  12015  rpexp12i  12157  pythagtriplem4  12270  pythagtriplem11  12276  pythagtriplem13  12278  pcpremul  12295  pceu  12297  pcqmul  12305  pcqdiv  12309  f1ocpbllem  12736  ercpbl  12755  erlecpbl  12756  cmn4  13113  ablsub4  13121  abladdsub4  13122  psmetlecl  13919  xmetlecl  13952  xblcntrps  13998  xblcntr  13999