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  7334  addassnqg  7466  ltsonq  7482  ltanqg  7484  ltmnqg  7485  addassnq0  7546  mulasssrg  7842  distrsrg  7843  lttrsr  7846  ltsosr  7848  ltasrg  7854  mulextsr1lem  7864  mulextsr1  7865  axmulass  7957  axdistr  7958  reapmul1  8639  mulcanap  8709  mulcanap2  8710  divassap  8734  divdirap  8741  div11ap  8744  apmul1  8832  ltdiv1  8912  ltmuldiv  8918  ledivmul  8921  lemuldiv  8925  lediv2  8935  ltdiv23  8936  lediv23  8937  xaddass2  9962  xlt2add  9972  modqdi  10501  expaddzap  10692  expmulzap  10694  leisorel  10946  resqrtcl  11211  xrbdtri  11458  dvdsgcd  12204  rpexp12i  12348  pythagtriplem4  12462  pythagtriplem11  12468  pythagtriplem13  12470  pcpremul  12487  pceu  12489  pcqmul  12497  pcqdiv  12501  f1ocpbllem  13012  ercpbl  13033  erlecpbl  13034  cmn4  13511  ablsub4  13519  abladdsub4  13520  lidlsubcl  14119  psmetlecl  14654  xmetlecl  14687  xblcntrps  14733  xblcntr  14734