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  5403  fcof1  5913  mpo0  6080  eroveu  6781  sbthlemi6  7137  sbthlemi8  7139  addcmpblnq  7562  mulcmpblnq  7563  ordpipqqs  7569  addcmpblnq0  7638  mulcmpblnq0  7639  nnnq0lem1  7641  prarloclemcalc  7697  addlocpr  7731  distrlem4prl  7779  distrlem4pru  7780  ltpopr  7790  addcmpblnr  7934  mulcmpblnrlemg  7935  mulcmpblnr  7936  prsrlem1  7937  ltsrprg  7942  apreap  8742  apreim  8758  aptap  8805  divdivdivap  8868  divmuleqap  8872  divadddivap  8882  divsubdivap  8883  ledivdiv  9045  lediv12a  9049  exbtwnz  10478  seq3caopr  10725  seqcaoprg  10726  leexp2r  10823  zfz1iso  11071  ccatsymb  11145  wrd2ind  11263  swrdccat  11275  recvguniq  11514  rsqrmo  11546  summodclem2  11901  prodmodc  12097  qredeu  12627  pw2dvdseu  12698  pcadd  12871  mhmpropd  13507  issubmd  13515  grprcan  13578  isnsg3  13752  ghmpreima  13811  rngpropd  13926  ringpropd  14009  lmodvsmmulgdi  14295  lmodprop2d  14320  lss1d  14355  epttop  14772  txdis1cn  14960  metequiv2  15178  mulc1cncf  15271  cncfmptc  15278  cncfmptid  15279  addccncf  15282  negcncf  15287  dedekindicclemicc  15314  mpodvdsmulf1o  15672  2sqlem5  15806  2sqlem9  15811