Theorem simp3r 1028

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

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

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 982

This theorem is referenced by:  simpl3r  1055  simpr3r  1061  simp13r  1115  simp23r  1121  simp33r  1127  issod  4351  tfisi  4620  fvun1  5624  f1oiso2  5871  tfrlem5  6369  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  ecopovtrn  6688  ecopovtrng  6691  dftap2  7313  addassnqg  7444  ltsonq  7460  ltanqg  7462  ltmnqg  7463  addassnq0  7524  mulasssrg  7820  distrsrg  7821  lttrsr  7824  ltsosr  7826  ltasrg  7832  mulextsr1lem  7842  mulextsr1  7843  axmulass  7935  axdistr  7936  reapmul1  8616  mulcanap  8686  mulcanap2  8687  divassap  8711  divdirap  8718  div11ap  8721  apmul1  8809  ltdiv1  8889  ltmuldiv  8895  ledivmul  8898  lemuldiv  8902  lediv2  8912  ltdiv23  8913  lediv23  8914  xaddass2  9939  xlt2add  9949  modqdi  10466  expaddzap  10657  expmulzap  10659  leisorel  10911  resqrtcl  11176  xrbdtri  11422  dvdsgcd  12152  rpexp12i  12296  pythagtriplem4  12409  pythagtriplem11  12415  pythagtriplem13  12417  pcpremul  12434  pceu  12436  pcqmul  12444  pcqdiv  12448  f1ocpbllem  12896  ercpbl  12917  erlecpbl  12918  cmn4  13378  ablsub4  13386  abladdsub4  13387  lidlsubcl  13986  psmetlecl  14513  xmetlecl  14546  xblcntrps  14592  xblcntr  14593