Theorem simprr1 1222

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

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

Proof of Theorem simprr1

Step	Hyp	Ref	Expression
1		simp1 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antll 729	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp2  8122  sqrmo  15217  icodiamlt  15404  psgnunilem2  19425  haust1  23239  cnhaus  23241  isreg2  23264  llynlly  23364  restnlly  23369  llyrest  23372  llyidm  23375  nllyidm  23376  cldllycmp  23382  txlly  23523  txnlly  23524  pthaus  23525  txhaus  23534  txkgen  23539  xkohaus  23540  xkococnlem  23546  hauspwpwf1  23874  itg2add  25660  ulmdvlem3  26311  nosupno  27615  noinfno  27630  etasslt  27725  scutbdaybnd  27727  scutbdaybnd2  27728  addsproplem6  27881  negsproplem6  27939  mulsproplem13  28031  mulsproplem14  28032  mulsprop  28033  ax5seglem6  28861  fusgrfis  29257  umgr2wlkon  29880  numclwwlk5  30317  connpconn  35222  cvmliftmolem2  35269  cvmlift2lem10  35299  cvmlift3lem2  35307  cvmlift3lem8  35313  broutsideof3  36114  unblimceq0  36495  paddasslem10  39823  lhpexle2lem  40003  lhpexle3lem  40005  cdlemj3  40817  cdlemkid4  40928  mpaaeu  43139  stoweidlem35  46033  stoweidlem56  46054  stoweidlem59  46057  2arwcat  49589