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  5440  fcof1  5958  mpo0  6125  eroveu  6862  sbthlemi6  7234  sbthlemi8  7236  suppeqfsuppbi  7250  addcmpblnq  7687  mulcmpblnq  7688  ordpipqqs  7694  addcmpblnq0  7763  mulcmpblnq0  7764  nnnq0lem1  7766  prarloclemcalc  7822  addlocpr  7856  distrlem4prl  7904  distrlem4pru  7905  ltpopr  7915  addcmpblnr  8059  mulcmpblnrlemg  8060  mulcmpblnr  8061  prsrlem1  8062  ltsrprg  8067  apreap  8866  apreim  8882  aptap  8929  divdivdivap  8992  divmuleqap  8996  divadddivap  9006  divsubdivap  9007  ledivdiv  9169  lediv12a  9173  exbtwnz  10617  seq3caopr  10864  seqcaoprg  10865  leexp2r  10962  zfz1iso  11221  ccatsymb  11298  wrd2ind  11423  swrdccat  11435  recvguniq  11688  rsqrmo  11720  summodclem2  12076  prodmodc  12272  qredeu  12802  pw2dvdseu  12873  pcadd  13046  mhmpropd  13700  issubmd  13708  grprcan  13771  isnsg3  13945  ghmpreima  14004  rngpropd  14120  ringpropd  14203  lmodvsmmulgdi  14520  lmodprop2d  14545  lss1d  14580  epttop  15004  txdis1cn  15192  metequiv2  15410  mulc1cncf  15503  cncfmptc  15510  cncfmptid  15511  addccncf  15514  negcncf  15519  dedekindicclemicc  15546  mpodvdsmulf1o  15907  2sqlem5  16041  2sqlem9  16046