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  5299  fcof1  5784  mpo0  5945  eroveu  6626  sbthlemi6  6961  sbthlemi8  6963  addcmpblnq  7366  mulcmpblnq  7367  ordpipqqs  7373  addcmpblnq0  7442  mulcmpblnq0  7443  nnnq0lem1  7445  prarloclemcalc  7501  addlocpr  7535  distrlem4prl  7583  distrlem4pru  7584  ltpopr  7594  addcmpblnr  7738  mulcmpblnrlemg  7739  mulcmpblnr  7740  prsrlem1  7741  ltsrprg  7746  apreap  8544  apreim  8560  aptap  8607  divdivdivap  8670  divmuleqap  8674  divadddivap  8684  divsubdivap  8685  ledivdiv  8847  lediv12a  8851  exbtwnz  10251  seq3caopr  10483  leexp2r  10574  zfz1iso  10821  recvguniq  11004  rsqrmo  11036  summodclem2  11390  prodmodc  11586  qredeu  12097  pw2dvdseu  12168  pcadd  12339  mhmpropd  12857  issubmd  12865  grprcan  12910  isnsg3  13067  ringpropd  13217  lmodvsmmulgdi  13413  lmodprop2d  13438  epttop  13593  txdis1cn  13781  metequiv2  13999  mulc1cncf  14079  cncfmptc  14085  cncfmptid  14086  addccncf  14089  negcncf  14091  dedekindicclemicc  14113  2sqlem5  14469  2sqlem9  14474