Theorem simprr1 1234

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 1148	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antll 739	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  poxp2  8118  sqrmo  15261  icodiamlt  15448  psgnunilem2  19518  haust1  23392  cnhaus  23394  isreg2  23417  llynlly  23517  restnlly  23522  llyrest  23525  llyidm  23528  nllyidm  23529  cldllycmp  23535  txlly  23676  txnlly  23677  pthaus  23678  txhaus  23687  txkgen  23692  xkohaus  23693  xkococnlem  23699  hauspwpwf1  24027  itg2add  25801  ulmdvlem3  26442  nosupno  27744  noinfno  27759  etaslts  27863  cutbdaybnd  27865  cutbdaybnd2  27866  addsproplem6  28044  negsproplem6  28103  mulsproplem13  28198  mulsproplem14  28199  mulsprop  28200  bdayfinbndlem1  28537  ax5seglem6  29081  fusgrfis  29477  umgr2wlkon  30096  numclwwlk5  30536  connpconn  35549  cvmliftmolem2  35596  cvmlift2lem10  35626  cvmlift3lem2  35634  cvmlift3lem8  35640  broutsideof3  36440  unblimceq0  36909  paddasslem10  40417  lhpexle2lem  40597  lhpexle3lem  40599  cdlemj3  41411  cdlemkid4  41522  mpaaeu  43691  stoweidlem35  46573  stoweidlem56  46594  stoweidlem59  46597  2arwcat  50185