Theorem simprll 539

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  5412  fcof1  5924  mpo0  6091  eroveu  6795  sbthlemi6  7161  sbthlemi8  7163  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  addcmpblnq0  7663  mulcmpblnq0  7664  nnnq0lem1  7666  prarloclemcalc  7722  addlocpr  7756  distrlem4prl  7804  distrlem4pru  7805  ltpopr  7815  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  prsrlem1  7962  ltsrprg  7967  apreap  8767  apreim  8783  aptap  8830  divdivdivap  8893  divmuleqap  8897  divadddivap  8907  divsubdivap  8908  ledivdiv  9070  lediv12a  9074  exbtwnz  10511  seq3caopr  10758  seqcaoprg  10759  leexp2r  10856  zfz1iso  11106  ccatsymb  11180  wrd2ind  11305  swrdccat  11317  recvguniq  11557  rsqrmo  11589  summodclem2  11945  prodmodc  12141  qredeu  12671  pw2dvdseu  12742  pcadd  12915  mhmpropd  13551  issubmd  13559  grprcan  13622  isnsg3  13796  ghmpreima  13855  rngpropd  13971  ringpropd  14054  lmodvsmmulgdi  14340  lmodprop2d  14365  lss1d  14400  epttop  14817  txdis1cn  15005  metequiv2  15223  mulc1cncf  15316  cncfmptc  15323  cncfmptid  15324  addccncf  15327  negcncf  15332  dedekindicclemicc  15359  mpodvdsmulf1o  15717  2sqlem5  15851  2sqlem9  15856