Theorem simprr3 1109

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simprr3	⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)

Proof of Theorem simprr3

Step	Hyp	Ref	Expression
1		simpr3 1067	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒)
2	1	adantl 482	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038

This theorem is referenced by:  el2xptp0  7160  icodiamlt  14103  psgnunilem2  17831  srgbinom  18461  psgndiflemA  19861  haust1  21061  cnhaus  21063  isreg2  21086  llynlly  21185  restnlly  21190  llyrest  21193  llyidm  21196  nllyidm  21197  cldllycmp  21203  txlly  21344  txnlly  21345  pthaus  21346  txhaus  21355  txkgen  21360  xkohaus  21361  xkococnlem  21367  cmetcaulem  22989  itg2add  23427  ulmdvlem3  24055  ax5seglem6  25709  fusgrfis  26104  wwlksnextfun  26656  umgr2wlkon  26709  connpconn  30917  cvmlift3lem2  31002  cvmlift3lem8  31008  nosino  31567  ifscgr  31785  broutsideof3  31867  unblimceq0  32132  paddasslem10  34581  lhpexle2lem  34761  lhpexle3lem  34763  mpaaeu  37187  stoweidlem35  39546  stoweidlem56  39567  stoweidlem59  39570