Theorem simprr1 1109

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

Assertion

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

Proof of Theorem simprr1

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

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

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 1039

This theorem is referenced by:  sqrmo  13992  icodiamlt  14174  psgnunilem2  17915  haust1  21156  cnhaus  21158  isreg2  21181  llynlly  21280  restnlly  21285  llyrest  21288  llyidm  21291  nllyidm  21292  cldllycmp  21298  txlly  21439  txnlly  21440  pthaus  21441  txhaus  21450  txkgen  21455  xkohaus  21456  xkococnlem  21462  hauspwpwf1  21791  itg2add  23526  ulmdvlem3  24156  ax5seglem6  25814  fusgrfis  26222  umgr2wlkon  26846  numclwlk1lem2f  27225  numclwwlk5  27246  connpconn  31217  cvmliftmolem2  31264  cvmlift2lem10  31294  cvmlift3lem2  31302  cvmlift3lem8  31308  nosupno  31849  scutbdaybnd  31921  broutsideof3  32233  unblimceq0  32498  paddasslem10  35115  lhpexle2lem  35295  lhpexle3lem  35297  cdlemj3  36111  cdlemkid4  36222  mpaaeu  37720  stoweidlem35  40252  stoweidlem56  40273  stoweidlem59  40276