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  5361  fcof1  5859  mpo0  6022  eroveu  6720  sbthlemi6  7071  sbthlemi8  7073  addcmpblnq  7487  mulcmpblnq  7488  ordpipqqs  7494  addcmpblnq0  7563  mulcmpblnq0  7564  nnnq0lem1  7566  prarloclemcalc  7622  addlocpr  7656  distrlem4prl  7704  distrlem4pru  7705  ltpopr  7715  addcmpblnr  7859  mulcmpblnrlemg  7860  mulcmpblnr  7861  prsrlem1  7862  ltsrprg  7867  apreap  8667  apreim  8683  aptap  8730  divdivdivap  8793  divmuleqap  8797  divadddivap  8807  divsubdivap  8808  ledivdiv  8970  lediv12a  8974  exbtwnz  10400  seq3caopr  10647  seqcaoprg  10648  leexp2r  10745  zfz1iso  10993  ccatsymb  11066  recvguniq  11350  rsqrmo  11382  summodclem2  11737  prodmodc  11933  qredeu  12463  pw2dvdseu  12534  pcadd  12707  mhmpropd  13342  issubmd  13350  grprcan  13413  isnsg3  13587  ghmpreima  13646  rngpropd  13761  ringpropd  13844  lmodvsmmulgdi  14129  lmodprop2d  14154  lss1d  14189  epttop  14606  txdis1cn  14794  metequiv2  15012  mulc1cncf  15105  cncfmptc  15112  cncfmptid  15113  addccncf  15116  negcncf  15121  dedekindicclemicc  15148  mpodvdsmulf1o  15506  2sqlem5  15640  2sqlem9  15645