Theorem simprll 537

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprll	⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Proof of Theorem simprll

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrl 490	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  imain  5341  fcof1  5833  mpo0  5996  eroveu  6694  sbthlemi6  7037  sbthlemi8  7039  addcmpblnq  7453  mulcmpblnq  7454  ordpipqqs  7460  addcmpblnq0  7529  mulcmpblnq0  7530  nnnq0lem1  7532  prarloclemcalc  7588  addlocpr  7622  distrlem4prl  7670  distrlem4pru  7671  ltpopr  7681  addcmpblnr  7825  mulcmpblnrlemg  7826  mulcmpblnr  7827  prsrlem1  7828  ltsrprg  7833  apreap  8633  apreim  8649  aptap  8696  divdivdivap  8759  divmuleqap  8763  divadddivap  8773  divsubdivap  8774  ledivdiv  8936  lediv12a  8940  exbtwnz  10359  seq3caopr  10606  seqcaoprg  10607  leexp2r  10704  zfz1iso  10952  recvguniq  11179  rsqrmo  11211  summodclem2  11566  prodmodc  11762  qredeu  12292  pw2dvdseu  12363  pcadd  12536  mhmpropd  13170  issubmd  13178  grprcan  13241  isnsg3  13415  ghmpreima  13474  rngpropd  13589  ringpropd  13672  lmodvsmmulgdi  13957  lmodprop2d  13982  lss1d  14017  epttop  14412  txdis1cn  14600  metequiv2  14818  mulc1cncf  14911  cncfmptc  14918  cncfmptid  14919  addccncf  14922  negcncf  14927  dedekindicclemicc  14954  mpodvdsmulf1o  15312  2sqlem5  15446  2sqlem9  15451