Theorem simp3r 1015

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 109	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant3 1009	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 969

This theorem is referenced by:  simpl3r  1042  simpr3r  1048  simp13r  1102  simp23r  1108  simp33r  1114  issod  4291  tfisi  4558  fvun1  5546  f1oiso2  5789  tfrlem5  6273  tfr1onlembxssdm  6302  tfrcllembxssdm  6315  ecopovtrn  6589  ecopovtrng  6592  addassnqg  7314  ltsonq  7330  ltanqg  7332  ltmnqg  7333  addassnq0  7394  mulasssrg  7690  distrsrg  7691  lttrsr  7694  ltsosr  7696  ltasrg  7702  mulextsr1lem  7712  mulextsr1  7713  axmulass  7805  axdistr  7806  reapmul1  8484  mulcanap  8553  mulcanap2  8554  divassap  8577  divdirap  8584  div11ap  8587  apmul1  8675  ltdiv1  8754  ltmuldiv  8760  ledivmul  8763  lemuldiv  8767  lediv2  8777  ltdiv23  8778  lediv23  8779  xaddass2  9797  xlt2add  9807  modqdi  10317  expaddzap  10489  expmulzap  10491  leisorel  10736  resqrtcl  10957  xrbdtri  11203  dvdsgcd  11930  rpexp12i  12064  pythagtriplem4  12177  pythagtriplem11  12183  pythagtriplem13  12185  pcpremul  12202  pceu  12204  pcqmul  12212  pcqdiv  12216  psmetlecl  12875  xmetlecl  12908  xblcntrps  12954  xblcntr  12955