Theorem simprll 532

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 108	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrl 487	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  imain  5278  fcof1  5759  mpo0  5920  eroveu  6600  sbthlemi6  6935  sbthlemi8  6937  addcmpblnq  7316  mulcmpblnq  7317  ordpipqqs  7323  addcmpblnq0  7392  mulcmpblnq0  7393  nnnq0lem1  7395  prarloclemcalc  7451  addlocpr  7485  distrlem4prl  7533  distrlem4pru  7534  ltpopr  7544  addcmpblnr  7688  mulcmpblnrlemg  7689  mulcmpblnr  7690  prsrlem1  7691  ltsrprg  7696  apreap  8493  apreim  8509  divdivdivap  8617  divmuleqap  8621  divadddivap  8631  divsubdivap  8632  ledivdiv  8793  lediv12a  8797  exbtwnz  10194  seq3caopr  10426  leexp2r  10517  zfz1iso  10763  recvguniq  10946  rsqrmo  10978  summodclem2  11332  prodmodc  11528  qredeu  12038  pw2dvdseu  12109  pcadd  12280  mhmpropd  12676  issubmd  12683  grprcan  12727  epttop  12843  txdis1cn  13031  metequiv2  13249  mulc1cncf  13329  cncfmptc  13335  cncfmptid  13336  addccncf  13339  negcncf  13341  dedekindicclemicc  13363  2sqlem5  13708  2sqlem9  13713