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  5341  fcof1  5831  mpo0  5993  eroveu  6686  sbthlemi6  7029  sbthlemi8  7031  addcmpblnq  7436  mulcmpblnq  7437  ordpipqqs  7443  addcmpblnq0  7512  mulcmpblnq0  7513  nnnq0lem1  7515  prarloclemcalc  7571  addlocpr  7605  distrlem4prl  7653  distrlem4pru  7654  ltpopr  7664  addcmpblnr  7808  mulcmpblnrlemg  7809  mulcmpblnr  7810  prsrlem1  7811  ltsrprg  7816  apreap  8616  apreim  8632  aptap  8679  divdivdivap  8742  divmuleqap  8746  divadddivap  8756  divsubdivap  8757  ledivdiv  8919  lediv12a  8923  exbtwnz  10342  seq3caopr  10589  seqcaoprg  10590  leexp2r  10687  zfz1iso  10935  recvguniq  11162  rsqrmo  11194  summodclem2  11549  prodmodc  11745  qredeu  12275  pw2dvdseu  12346  pcadd  12519  mhmpropd  13108  issubmd  13116  grprcan  13179  isnsg3  13347  ghmpreima  13406  rngpropd  13521  ringpropd  13604  lmodvsmmulgdi  13889  lmodprop2d  13914  lss1d  13949  epttop  14336  txdis1cn  14524  metequiv2  14742  mulc1cncf  14835  cncfmptc  14842  cncfmptid  14843  addccncf  14846  negcncf  14851  dedekindicclemicc  14878  mpodvdsmulf1o  15236  2sqlem5  15370  2sqlem9  15375