Theorem simprr1 1223

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

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

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 1089

This theorem is referenced by:  poxp2  8093  sqrmo  15213  icodiamlt  15400  psgnunilem2  19470  haust1  23317  cnhaus  23319  isreg2  23342  llynlly  23442  restnlly  23447  llyrest  23450  llyidm  23453  nllyidm  23454  cldllycmp  23460  txlly  23601  txnlly  23602  pthaus  23603  txhaus  23612  txkgen  23617  xkohaus  23618  xkococnlem  23624  hauspwpwf1  23952  itg2add  25726  ulmdvlem3  26367  nosupno  27667  noinfno  27682  etaslts  27785  cutbdaybnd  27787  cutbdaybnd2  27788  addsproplem6  27966  negsproplem6  28025  mulsproplem13  28120  mulsproplem14  28121  mulsprop  28122  bdayfinbndlem1  28459  ax5seglem6  29003  fusgrfis  29399  umgr2wlkon  30018  numclwwlk5  30458  connpconn  35417  cvmliftmolem2  35464  cvmlift2lem10  35494  cvmlift3lem2  35502  cvmlift3lem8  35508  broutsideof3  36308  unblimceq0  36767  paddasslem10  40275  lhpexle2lem  40455  lhpexle3lem  40457  cdlemj3  41269  cdlemkid4  41380  mpaaeu  43578  stoweidlem35  46463  stoweidlem56  46484  stoweidlem59  46487  2arwcat  50075