Theorem simprr1 1220

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  sqrmo  14963  icodiamlt  15147  psgnunilem2  19103  haust1  22503  cnhaus  22505  isreg2  22528  llynlly  22628  restnlly  22633  llyrest  22636  llyidm  22639  nllyidm  22640  cldllycmp  22646  txlly  22787  txnlly  22788  pthaus  22789  txhaus  22798  txkgen  22803  xkohaus  22804  xkococnlem  22810  hauspwpwf1  23138  itg2add  24924  ulmdvlem3  25561  ax5seglem6  27302  fusgrfis  27697  umgr2wlkon  28315  numclwwlk5  28752  connpconn  33197  cvmliftmolem2  33244  cvmlift2lem10  33274  cvmlift3lem2  33282  cvmlift3lem8  33288  poxp2  33790  nosupno  33906  noinfno  33921  etasslt  34007  scutbdaybnd  34009  scutbdaybnd2  34010  broutsideof3  34428  unblimceq0  34687  paddasslem10  37843  lhpexle2lem  38023  lhpexle3lem  38025  cdlemj3  38837  cdlemkid4  38948  mpaaeu  40975  stoweidlem35  43576  stoweidlem56  43597  stoweidlem59  43600