Theorem simprll 543

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 494	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  imain  5463  fcof1  5989  mpo0  6158  eroveu  6900  sbthlemi6  7279  sbthlemi8  7281  suppeqfsuppbi  7295  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  addcmpblnq0  7810  mulcmpblnq0  7811  nnnq0lem1  7813  prarloclemcalc  7869  addlocpr  7903  distrlem4prl  7951  distrlem4pru  7952  ltpopr  7962  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  prsrlem1  8109  ltsrprg  8114  apreap  8916  apreim  8932  aptap  8979  divdivdivap  9044  divmuleqap  9048  divadddivap  9058  divsubdivap  9059  ledivdiv  9221  lediv12a  9225  exbtwnz  10687  seq3caopr  10934  seqcaoprg  10935  leexp2r  11032  hashf1lem1  11287  hashf1lem2  11288  zfz1iso  11295  ccatsymb  11372  wrd2ind  11497  swrdccat  11509  recvguniq  11763  rsqrmo  11795  summodclem2  12151  prodmodc  12347  qredeu  12877  pw2dvdseu  12948  pcadd  13121  mhmpropd  13775  issubmd  13783  grprcan  13844  isnsg3  14012  ghmpreima  14071  rngpropd  14256  ringpropd  14345  lmodvsmmulgdi  14662  lmodprop2d  14687  lss1d  14722  assamulgscmlem2  15044  epttop  15193  txdis1cn  15381  metequiv2  15599  mulc1cncf  15692  cncfmptc  15699  cncfmptid  15700  addccncf  15703  negcncf  15708  dedekindicclemicc  15735  mpodvdsmulf1o  16110  2sqlem5  16250  2sqlem9  16255