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  4355  tfisi  4624  fvun1  5630  f1oiso2  5877  tfrlem5  6381  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  ecopovtrn  6700  ecopovtrng  6703  dftap2  7336  addassnqg  7468  ltsonq  7484  ltanqg  7486  ltmnqg  7487  addassnq0  7548  mulasssrg  7844  distrsrg  7845  lttrsr  7848  ltsosr  7850  ltasrg  7856  mulextsr1lem  7866  mulextsr1  7867  axmulass  7959  axdistr  7960  reapmul1  8641  mulcanap  8711  mulcanap2  8712  divassap  8736  divdirap  8743  div11ap  8746  apmul1  8834  ltdiv1  8914  ltmuldiv  8920  ledivmul  8923  lemuldiv  8927  lediv2  8937  ltdiv23  8938  lediv23  8939  xaddass2  9964  xlt2add  9974  modqdi  10503  expaddzap  10694  expmulzap  10696  leisorel  10948  resqrtcl  11213  xrbdtri  11460  dvdsgcd  12206  rpexp12i  12350  pythagtriplem4  12464  pythagtriplem11  12470  pythagtriplem13  12472  pcpremul  12489  pceu  12491  pcqmul  12499  pcqdiv  12503  f1ocpbllem  13014  ercpbl  13035  erlecpbl  13036  cmn4  13513  ablsub4  13521  abladdsub4  13522  lidlsubcl  14121  psmetlecl  14678  xmetlecl  14711  xblcntrps  14757  xblcntr  14758